(4.1 hours to learn)
A formal proof is an argument in a formal system where each step is justified by one of a precisely defined set of inference rules. Formal proofs are used as a model for studying mathematics itself, and are used in formal verification. One hopes a proof system is sound, in that each inference rule yields only true statements when its premises are true. A system is complete if all true statements expressible in some logical language can be proved within the system. Various proof systems have been defined for propositional logic which are both sound and complete.
This concept has the prerequisites:
- understand the difference between formal and informal proofs
- be able to prove tautologies in a formal propositional proof system
- know what it means for a proof system to be sound and complete
- prove the soundness of a propositional proof system
- prove the completeness of a propositional proof system
Core resources (read/watch one of the following)
→ Coursera: Introduction to Logic (2014)
An introductory logic course geared towards computer scientists.
Location: Lecture sequence "Propositional proofs"
- Click on "Preview" to see the videos.
→ Coursera: Logic: Language and Information (2014)
An introductory logic course geared towards philosophers.
→ Notes on Logic (2013)
Lecture notes for a course on first order logic.
Location: Section 6, "Formal proofs," pages 13-17
→ The Language of First-Order Logic
An undergraduate logic textbook aimed at philosophers, with an educational software package.
- Section 3.8, "Methods of proof," pages 58-66
- Section 3.9, "Formal proofs," pages 66-82
- Section 4.4, "Methods of proof," pages 99-104
- Section 4.5, "Formal proofs," pages 104-108
- Section 4.6, "Speeding up proofs," pages 108-112
-No Additional Notes-
- create concept: shift + click on graph
- change concept title: shift + click on existing concept
- link together concepts: shift + click drag from one concept to another
- remove concept from graph: click on concept then press delete/backspace
- add associated content to concept: click the small circle that appears on the node when hovering over it
- other actions: use the icons in the upper right corner to optimize the graph placement, preview the graph, or download a json representation