propositional proofs
(4.1 hours to learn)
Summary
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.
Context
This concept has the prerequisites:
Goals
- 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)
-Free-
→ Coursera: Introduction to Logic (2014)
An introductory logic course geared towards computer scientists.
Location:
Lecture sequence "Propositional proofs"
Other notes:
- Click on "Preview" to see the videos.
→ Coursera: Logic: Language and Information (2014)
An introductory logic course geared towards philosophers.
→ Notes on Logic (2013)
-Paid-
→ 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
See also
-No Additional Notes-