File this under Mathematics of argumentation, truth, validity, and propositions.
Minute 11:30 “We have certain proof-theoretic intuitions about valid ways of reasoning. And we have other model-theoretic intuitions about what can be true. And we want those to match up.”
I couldn’t be into this all the time, but it’s kind of reassuring to know that somebody cares about “Mapping structures into each other and showing that they’re the same, so we can feel better about things.”
Also, here’s 300 pages on the Curry-Howard isomorphism. For those who want a 300-page explanation of why lambda calculi (&c.) are equivalent to systems of formal logic.
Polynomials enter the picture as well. Hmm. Does that make a creepy connection between engineering applications and theological claims? Weird…
Minute 25. Different sizes of infinity — if it sounds screwy to you, you’re on the side of Intuitionist Mathematicians.
The Lindenbaum Lemma, used in the proof of different sizes of infinity (|ℝ| > |ℤ| … in fact ℵ = |ℤ| < ℶ = |ℝ| < ℷ = |ℱ| < ℸ), “counts up” a bunch of infinite sets. Which how can you do that since you don’t finish counting any of the little individual sets?
Alfred Tarski apparently came up with the Lindenbaum Lemma. (He also proved, along with Stefan Banach, that assuming the axiom of choice yields a contradiction (1 ball = 2 balls).) Arendt Heyting gets in on the game too.
Minute 40. Dangit! Intuitionist logic is crazy too. I thought its requirement for constructive proofs meant that it would be non-crazy. But intuitionism still says F → anything and that A && ~A → F.
Peirce’s law: ( (A → B) → A ) → B.
Johansen’s minimal logic is intuitionist logic sans F → anything. It’s paraconsistent, meaning that it doesn’t treat all contradictions as equals.
Remind me again why so many proofs I learnt in school used contradictions instead of intuitionist math? I guess we sent a rocket to the moon <link>, so the math can’t be that far off.
Minute 55. Correspondence between intuitionistic logic and modal S4.
Does it bother you that mathematicians and logicians haven’t figured out how to make logic logical a century after Russell & Whitehead? I mean seriously, you would think math is logical. But the logical foundations of math are illogical.
I thought all I had to do to understand the universe was learn a bunch of math. Mom! Tell them to be right!