User:Lord Farin/Long-Term Projects/MLCS
Processing of 'Mathematical Logic for Computer Science (3e)'
First page it covers: Definition:Statement.
First page covered by Appendices: Definition:Set.
A book extensively and rigorously building the basic foundations of logic.
Progress thus far
Initial set-up complete. --Lord_Farin (talk) 22:26, 15 February 2013 (UTC)
Appendix covered up to $\text{A}.4$, stopped at Definition:Finite Cartesian Product. --Lord_Farin (talk) 23:19, 15 February 2013 (UTC)
Appendix covered. --Lord_Farin (talk) 09:20, 16 February 2013 (UTC)
Up to Definition:Language of Propositional Logic/Alphabet/Sign/Connective. --Lord_Farin (talk) 15:48, 16 February 2013 (UTC)
Up to $\S 2.7$, Semantic Tableau Algorithm/Heuristics. — Lord_Farin (talk) 11:58, 26 March 2014 (UTC)
Up to $\S 2.10$: Exercises; ended at Completeness Theorem for Semantic Tableaus. — Lord_Farin (talk) 19:17, 26 March 2014 (UTC)
Up to $\S 3$. Ended at Semantic Tableau Algorithm Terminates. Only took over a year. — Lord_Farin (talk) 15:37, 27 March 2014 (UTC)
Up to $\S 3.3$. Ended at Soundness and Completeness of Gentzen Proof System. — Lord_Farin (talk) 23:00, 3 April 2014 (UTC)
Up to $\S 3.6$. Ended at Principle of Commutation/Forward Implication/Formulation 2/Proof 2. — Lord_Farin (talk) 10:57, 5 April 2014 (UTC)
Missing Proofs
None atm
Skipped thus far (that is, what needs to be done still)
- Part of $\S 2.7.2$ proving Completeness Theorem for Semantic Tableaus using Hintikka sets.
- Proving correctness of heuristic adaptation of Semantic Tableau Algorithm, Exc. 2.19.
- Covering of derived rules of inference from $\S 3.4$, probably most easily done by introducing a third formulation on existing rules. Applies to $3.15,3.17,3.19,3.21,3.24,3.26$. Skipped rest of $\S 3.4$ and $\S 3.5$ because of this.
Other things
- Equivalence of Definitions of Semantic Equivalence for Boolean Interpretations
- Classification of Alpha-Formulas
- Classification of Beta-Formulas