User:Lord Farin/Books/Kunen Foundations
Processing of 'The Foundations of Mathematics'
Rigour on Model Theory and Proof Theory. Also Set Theory, but that's already covered a lot, so I'm skipping the naive set theory approach taken in the first part of the book.
Progress thus far
Initial set-up complete. — Lord_Farin (talk) 21:03, 5 January 2016 (UTC)
Paragraph $\text{II}.8$ somewhere, last located Satisfiability preserved in Supersignature
Up to $\text{II}.8.22$ Theory of Structure is Complete. — Lord_Farin (talk) 16:06, 10 May 2022 (UTC)
Up to $\text{II}.8.25$ Alphabetic Substitution is Semantically Equivalent. — Lord_Farin (talk) 15:18, 17 May 2022 (UTC)
Up to $\text{II}.10.1$ Definition:Hilbert Proof System Instance 1 for Predicate Logic. — Lord_Farin (talk) 20:09, 18 May 2022 (UTC)
Up to $\text{II}.10.5$ Soundness Theorem for Hilbert Proof System for Predicate Logic. — Lord_Farin (talk) 18:17, 2 June 2022 (UTC)
Up to $\text{II}.11.1$ Deduction Theorem for Hilbert Proof System for Predicate Logic. — Lord_Farin (talk) 08:48, 17 June 2022 (UTC)
Up to $\text{II}.11.8$ Universal Instantiation/Proof System. — Lord_Farin (talk) 18:25, 10 September 2022 (UTC)
Stopped for now at $\text{II}.11.9$ De Morgan's Laws (Predicate Logic)/Denial of Universality/Formulation 2/Forward Implication. — Lord_Farin (talk) 20:47, 22 September 2022 (UTC)
Missing Proofs
- Exercise $II.8.25$: Alphabetic Substitution is Semantically Equivalent
- Exercise $II.10.2$: Axioms of Hilbert Proof System Instance 1 for Predicate Logic are Tautologies
Skipped thus far (that is, what needs to be done still)
- Discussion of types of substructure (subgroup, subsemigroup) etc. after $II.8.17$
- Exercise $II.8.20$ establishing that completeness does not hold regarding an extended signature
- Exercise $II.8.26$ extending Alphabetic Substitution is Semantically Equivalent to substitutions in subformulas
- Definition $II.11.2$ and Lemma $II.11.3$ dealing with the
{{expand}}tag on Definition:Inconsistent (Logic) - Definition $II.11.5$ and Lemma $II.11.6$ dealing with "tautological reasoning"
Other things
The definition of Kunen for Definition:Language of Predicate Logic is slightly different because it is in Polish notation. This page needs to be set up, similar to Definition:Language of Propositional Logic/Keisler-Robbin.