This is an old revision of the document!
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 , \[
(\vdash_S F) \rightarrow (\models F)
\] We can only prove true formulas.
Completeness of a proof system
System is complete if for every formula , \[
(\models F) \rightarrow (\vdash F)
\] We can prove all valid formulas.
Case analysis proof system
A sound and complete proof system.
Case analysis rule: \[
\frac{P\{p \mapsto {\it true}\}\ ;\ P\{p \mapsto {\it false}\}} {P}
\]
Evaluation rule: derive if has no variables and it evaluates to true.
Adding simplification rules. Adding sound rules preserves soundness and completeness.
Gentzen proof system
Recall Gentzen's proof system from proofs and induction part of lecture02, ignoring rules for predicates and induction.
Resolution
Definition and soundness. Completeness in next lecture.