SE212

Proof Theory

Proof theories (also called deductive systems) provide means of ”calculating” things about the logic. Each proof theory is a means of doing proofs in that logic.

• Proof theories are methods that perform mechanical manipulations on strings of symbols.
• Proof theories are based on pattern matching.
• For a particular proof theory, there may be multiple ways to prove a formula.

$P_1,P_2,\dots ,P_n|-Q$ means that from $P_1,P_2,\dots P_n$ we can prove $Q$ using a proof theory.

• $|-$ defines what is a proof
• We say that $P_1,P_2,\dots ,P_n$ “proves” $Q$

Also see Semantics.

Concepts

• Soundness
• Completeness