What is Proof?

Joel David Hamkins, Professor of Logic, Oxford University
This lecture is based on chapter 5 of my book, Lectures on the Philosophy of Mathematics, published with MIT Press, mitpress.mit.edu/books/lectur...
Lecture 5. Proof
What is proof? What is the relation between proof and truth? Is every mathematical truth true for a reason? After clarifying the distinction between syntax and semantics and discussing various views on the nature of proof, including proof-as-dialogue, we shall consider the nature of formal proof. We shall highlight the importance of soundness, completeness, and verifiability in any formal proof system, outlining the central ideas used in proving the completeness theorem. The compactness property distills the finiteness of proofs into an independent, purely semantic consequence. Computer-verified proof promises increasing significance; its role is well illustrated by the history of the four-color theorem. Nonclassical logics, such as intuitionistic logic, arise naturally from formal systems by weakening the logical rules.

[@joeldavidhamkins5484]

Errata At 7:32 I mention the phrase "not even wrong", which should evidently be attributed to Wolfgang Pauli (en.wikipedia.org/wiki/Not_even_wrong).

[@RenRealism]

I like your videos! Audio seems a bit off on this one though

[@calmander]

Best one so far!

[@giveaway4002]

You are really really great ... ❤️ For India.... Thanks for your video Professor

[@erincarmody8562]

Wonderful talk! I was thinking more about my question, and I was really thinking about how axioms are like primary colors. And you said that the axioms are the mathematical context. So, it is like the primary colors because it depends on what kind of color system you are in as to which colors are primary. Thanks!

[@joeldavidhamkins5484]

I find it interesting how your comment relates to the Wittgenstein quotation I had mentioned, concerning the fact that we can aim to reproduce a proof exactly, unlike the situation where we might seek (unsuccessfully) to reproduce a shade of color exactly or some handwriting.

[@StephenPaulKing]

Might sentience spring from an unverifiable proof by demonstration of one's own existence?

[@johntavers6878]

your voice sounds very deep in this video lol

[@ViceroyoftheDiptera]

It's been artificially lowered for some reason.

[@moussaadem7933]

Probably some kind of accident

[@evangorstein4345]

At @40:38, we use compactness in a proof of the completeness of the proof system. How did we know that the proof system is compact?

[@evangorstein4345]

Also, I'm struggling to understand validity and specifically, what it means for an axiom to be valid? If A is an axiom of theory T, then how could there be a model of T which is not a model of A? What does that mean?

[@joeldavidhamkins5484]

This is an important point. I had mentioned earlier (see 34:03) that there are proofs of the compactness theorem that do not rely on completeness. Indeed, the standard way to prove the compactness theorem in most parts of mathematical logic nowadays does not use completeness. In most contemporary model theory texts, for example, compactness is proved without introducing any proof theory at all (and therefore without completeness). I woulds say that the Henkin proof of completeness is seen better as a direct proof of compactness: every finitely-satisfiable theory can be extended to a finitely-satisfiable complete Henkin theory, and every such theory has a model by Henkin's argument. But also, one can prove compactness by means of ultrapowers or Boolean-valued models and many other arguments.

[@joeldavidhamkins5484]

I'm not sure of the context of your queston, but let me try to answer anyway. We say that a statement phi is valid, if phi is true in all models. A statement phi is valid relative to a theory T, if every model of T satisfies phi. If A is an axiom of T, then A is valid relative to T, but it might not be valid without assuming T.

[@evangorstein4345]

Got it. I guess my confusion is that since all the axioms of a proof system are always valid relative to the very same proof system, then that doesn't seem like something we need to check in order to establish the soundness of the proof system, as you say at @29:05?

[@joeldavidhamkins5484]

Ah, now I understand what you are asking. We have two kinds of axioms: the axioms of the theory T, but also the *logical* axioms, which are part of the proof system. In effect, the logical axioms are axioms that the proof systems will automatically add to every theory, for the purpose of using that proof system. For soundness, what we need to check is that these logical axioms are indeed valid, which is to say, that they are true in all structures, with no restriction on the theory T.

[@RBanerj]

Hi Joel, starting at around 37 minutes you describe a second-order proof system that you say is both sound and complete: take all second-order validities as axioms and modus ponens as your rule of inference. It appears to me that this proof system is actually not complete unless you allow infinitely long proofs: consider the entailment from second-order Peano arithmetic + the axiom schema {c≠0, c≠S0, c≠SS0, ...} to the sentence 0=S0. Since every finite subset of the assumptions is satisfied by the natural numbers, no proof from finitely many assumptions will suffice to derive 0=S0. So to prove the entailment would require an infinitary proof system. And actually, I'm not sure that the proof system you describe would be able to derive 0=S0 from the assumptions even allowing for infinitely long proofs. If all you have is modus ponens and finitely long sentences, how would you show the contradiction between second-order Peano arithmetic and the axiom schema {c≠0, c≠S0, c≠SS0, ...}?

[@joeldavidhamkins5484]

You are completely right. This is a residue of the failure of compactness in second-order logic. Nevertheless, one can construct a sound+complete proof system for second-order logic by allowing as rules of inference all (infinitary) valid consequences. That is, we take it as a rule Gamma entails phi, whenever this is in fact valid. This is obviously sound, and also complete.

[@Robinson8491]

Thanks

[@Maria-yx4se]

Voice become deeper lol

[@antoniolewis1016]

It's surprising how little discussion there has been about psychology and cognition and neurology here. Considering we are entering into questions of meaning and interpretation of these deep notions of reasoning and logic, and considering how much these notions of reasoning matter in clinical psychiatry and psychology and and in child neurodevelopment and in multiple mental illnesses ranging from autism to schizophrenia, it would be great to see some sort of connection between these two very distant fields of logic in mathematics and logic in psychiatry, bridged with logic in philosophy.