• English only

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.

Gentzen proof system

Recall Gentzen's proof system from proofs and induction part of lecture02, ignoring rules for predicates and induction.

Resolution 