User:Lord Farin/Long-Term Projects/MLCS

From ProofWiki
Jump to navigation Jump to search

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

Theorems of PropLog in need of extensive treatment