MA5219 Logic and Foundation of Mathematics I: the consistency of arithmetic

In this module, we discuss the consistency problem for (natural number) arithmetic. The main theorems are the Gödel–Rosser Incompleteness Theorems.

Prerequisites

Students are assumed to have seen the completeness of first-order logic. Nevertheless, the lectures include a brief recapitulation.

Lectures

Each lecture is 95 minutes long, with a five-minute break in the middle.

Follow the links below for the notes in pdf. Please do let me know if you spot any typos or errors anywhere.

  1. Programs, 13 August 2018.

    Notes first uploaded on 13 August 2018; the definition of ≠ added, the recursion for the evaluation of terms clarified, and a couple of typos corrected on 17 August 2018; more typos corrected on 20 August 2018

  2. Truth and computation, 16 August 2018.

    Notes first uploaded on 17 August 2018; paragraph immediately before Proposition 2.5 rewritten, ℤ changed to ℝ, and a couple of typos corrected on 20 August 2018; Remark 2.5 added, moved the condition that ∃y does not appear as substrings from the notation θ(x1,x2,…,xk) to the formation of formulas, and one more typo fixed on 4 September 2018; last sentence in the definition of structures changed on 20 September 2018

  3. Σ1 completeness, 20 August 2018.

    Notes first uploaded on 20 August 2018; the definition of n modified, the case for the constant symbol 1 added in the proof of Lemma 3.3, and a typo fixed on 21 August 2018; (R1) added to R(exp), and the case t=1 rewritten in the proof of Lemma 3.3 on 20 September 2018

  4. Representability of recursive objects, 23 August 2018.

    Notes first uploaded on 23 August 2018; typo in Assignment 4.6 fixed on 28 August 2018; figure numbering fixed on 31 August 2018; added (Q1) to Q(exp) on 20 September 2018; attribution added for Theorem 4.4 on 3 October 2018; typo in (QS1) fixed on 19 October 2018

  5. Arithmetization of syntax, 27 August 2018.

    Notes first uploaded on 28 August 2018; cross reference for the definition of free occurrences of variables in formulas added on 4 September 2018; ′ changed to ⊤ in Table 5.1, the representation of variables changed in the paragraph immediately before the definition of Gödel numbers, and Example 5.1 adjusted accordingly on 25 September 2018

  6. Proofs, 30 August 2018.

    Notes first uploaded on 31 August 2018; defined what it means for a variable occurrence to be free in a formula added, RAA explained, completeness added as one of the requirements for proof systems, and a few stylistic changes made on 4 September 2018; typo in the definition of semantic entailment for formulas fixed on 2 November 2018

  7. Gödel’s Completeness Theorem, 3 September 2018.

    Notes first uploaded on 4 September 2018; remark at the end of the paragraph immediately after the statement of Gödel’s Completeness Theorem added on 7 September 2018; typo after the definition of a Henkinized set corrected on 3 October 2018; the statement of the Model Construction Theorem strengthened on 29 October 2018

  8. The First Incompleteness Theorem, 6 September 2018.

    Notes first uploaded on 7 September 2018; ′ changed to ⊤ in Table 8.1 on 25 September 2018; typo on the last line on page 29 fixed on 2 November 2018

  9. Provability, 10 September 2018.

    Notes first uploaded on 11 September 2018; the definition of φ(x) corrected in Assignment 9.3 on 15 September 2018; final sentence modified on 24 September 2018

  10. Programs for the verification of proofs, 13 September 2018.

    Notes first uploaded on 15 September 2018; x-1 changed to x-z on 20 September 2018; definition of var(x) changed at the bottom of page 38 on 25 September 2018; changed the definition (but not the meaning) of len on 13 November 2018

  11. Elementary Arithmetic, 17 September 2018.

    Notes first uploaded on 20 September 2018; made some stylistic changes towards the end of Lemma 11.4, added a paragraph immediately after Lemma 11.4, and added the Intuition at the end on 24 September 2018; the ¬ moved to the right place in the statement of Bounded Δ0(exp) Comprehension on 21 November 2018

  12. Formalized Σ1 completeness, 20 September 2018.

    Notes first uploaded on 24 September 2018; the irrelevant ā removed in Assignment 12.7 on 19 October 2018; broken cross reference on page 51 fixed, and dashed lines to changed double lines in proofs on 13 November 2018; fixed a typo in the summation sign in Remark 12.2, removed the dependence of the polynomial on t in Remark 12.4, specified the language in the statement of Theorem 12.6, corrected the polynomial length bound for t<s in the proof of Theorem 12.6, and added cross-reference in Remark 12.8 on 21 November 2018; another length bound added to Remark 12.2, the final sentence in the 0 case in the proof of Lemma 12.3 taken out of the box, some steps in Remark 12.4 corrected, typo fixed in the last sentence in the t<s box in the proof of Theorem 12.6, the calculation for the proof length in the t<s case in the proof of Theorem 12.6 corrected on 24 November 2018; corrected a typo in Remark 12.2, explained a bit how one should parse Lemma 12.3 before the statement of the lemma, and explained what the blue bubbles mean in the proof of Lemma 12.3 on 8 January, 2019

  13. A closer look at incompleteness, 1 October 2018.

    Notes uploaded on 3 October 2018

  14. The Diagram Lemma, 4 October 2018.

    Notes first uploaded on 5 October 2018; typo on the first line of the F case of the proof of the Diagram Lemma fixed on 29 November 2018

  15. Model completeness, 8 October 2018.

    Notes uploaded on 8 October 2018

  16. Presburger Arithmetic, 11 October 2018.

    Notes uploaded on 12 October 2018

  17. Ordinals, 15 October 2018.

    Notes first uploaded on 16 October 2018; IndP(δ) changed to ProgP(δ) on 19 October 2018

  18. Peano Arithmetic, 18 October 2018.

    Notes first uploaded on 19 October 2018; a nicety condition added to the plan of our consistency proof towards the end, equality added as a non-logical symbol in PA, the word ‘infinitary’ removed in the description of the quantifier rules for Nat, and Remark 18.2 added on 23 October 2018; revised the plan towards the end, as well as the paragraph immediately after that on 27 October 2018

  19. Cut elimination, 22 October 2018.

    Notes first uploaded on 23 October 2018, typo in the first (1) in the quantifier case of the proof of Lemma 19.2 fixed, π0, π1, π2 changed to π̃, π0, π1 respectively in the proof of Lemma 19.2, and solid lines changed to dashed lines in the proof of Lemma 19.2 where the deduction rule is broken on 27 October 2018

  20. Consistency proof, 25 October 2018.

    Notes first uploaded on 27 October 2018; final sentence modified on 2 November 2018

  21. End extension, 29 October 2018.

    Notes first uploaded on 29 October 2018; cross reference to Lemma 21.1 in Case I in the proof of the Mac Dowell–Specker Theorem corrected on 2 November 2018

  22. Indicators, 1 November 2018.

    Notes first uploaded on 2 November 2018; figures added on 3 November 2018; sentence added immediately before Proposition 22.5, intermediate-value axiom for indicators eliminated, and the proof of Theorem 22.9(2) simplified accordingly on 6 November 2018; typo in the definition of indicators fixed, and the countability condition in the definition of indicators removed on 20 November 2018

  23. Ramsey’s Theorems, 5 November 2018.

    Notes first uploaded on 6 November 2018; two figures added later on the same day; modified some numbers in the definition of YPH on 20 November 2018

  24. Indiscernibles, 8 November 2018.

    Notes uploaded on 20 November 2018

  25. Finite consistency, 12 November 2018.

    Notes first uploaded on 13 November 2018; page numbers shifted on 20 November 2018; typo in Example 25.4 fixed on 22 November 2018; corrected the definition of the diagonalization function D on page 124, corrected the first sentence in the penultimate paragraph, removed ‘sufficiently large’ in the statement of the Finite Incompleteness Theorem and modified the end of the proof accordingly on 28 December 2018; added a reference to Theorem 26.1 before the Finite Incompleteness Theorem on 8 January 2019

  26. Consistency statements, 15 November 2018.

    Notes uploaded on 30 December 2018

Additional materials

  • Outline of my solutions to the assignments.

    1.6 posted on 31 August 2018; 2.7 posted on 4 September 2018; 3.7 posted on 7 September 2018; 4.6 posted on 11 September 2018; 5.3 posted on 15 September 2018; 6.3 and 7.1 posted on 20 September 2018; 8.2 posted on 3 October 2018; 9.3 posted on 5 October 2018; 10.2 and 11.6 posted on 13 October 2018; 12.7 and 13.3 posted on 19 October 2018; 14.7 posted on 23 October 2018; 15.2 and 16.11 posted on 27 October 2018; 17.8 posted on 2 November 2018; 18.1 and 19.4 posted on 6 November 2018; 20.8 and 21.3 posted on 13 November 2018

  • Examination, 28 November 2018.

    Uploaded on 8 January 2019

  • Bibliographic and organizational remarks.

    Uploaded on 8 January 2019