Proof Theory for Propositional Logic
Notion of a proof system
A set of proof rules, each of which specifies how to derive a formula from zero or more other formulas.
- Typical requirement: polynomial-time algorithm to check whether a rule application is valid according to the rule system
We write if we can derive formula in some proof system . We omit when it is clear.
Proof tree and proof sequences.
Proof complexity: given such that , the size of smallest proof of in .
Soundness of a proof system
System is sound if for every formula ,
We can only prove true formulas.
Completeness of a proof system
System is complete if for every formula ,
We can prove all valid formulas.
Some Example Proof Systems
Case analysis proof system
A simple A sound and complete proof system.
Rule 1: Case analysis rule:
Rule 2: Evaluation rule: derive if has no variables and it evaluates to true.
We can also add simplification rules. Adding sound rules preserves soundness and completeness.