Proof theory

Proof theory studies formal proofs and the deductive systems that produce them. It examines which conclusions follow from axioms, how proofs can be transformed, and what those transformations reveal about the chosen logic. Natural deduction organizes a proof through introduction and elimination rules for logical connectives and quantifiers.

A refutation of a collection of logical assumptions is a derivation of a contradiction from them. To prove a logical formula $\phi$ by refutation in classical propositional logic, add its negation $\neg \phi$ to the assumptions and derive falsity. The correctness of this inference follows from the rules of the chosen proof system.

For example, the clauses $p\vee q$, $\neg p$ and $\neg q$ have a resolution refutation: the first two resolve to $q$, and $q$ with $\neg q$ yields the empty clause. No truth assignment satisfies the three original clauses. This distinguishes the semantic claim of unsatisfiability from a syntactic certificate establishing it. In automated proving, producing a refutation is useful because another program can check the individual inference steps without repeating the search.

A Hilbert proof system specifies axiom schemes and inference rules, commonly including modus ponens. A formal proof is a finite sequence of axiom instances, permitted assumptions and conclusions obtained from preceding lines by those rules. Soundness and completeness compare this syntactic derivability with semantic validity or semantic entailment. These properties concern the particular chosen axioms and rules.

One presentation of classical propositional logic uses the schemes $A\to (B\to A)$, $(A\to (B\to C))\to ((A\to (\neg B\to C))\to (A\to C))$, and $(A\to B)\to (A\to (\neg B\to C))$, together with modus ponens rule and the case rule from $A\to B$ and $\neg A\to B$ to $B$. Its deduction theorem for propositional logic follows by induction on logical derivations: conditional modus ponens handles a modus ponens rule line, and the second scheme handles a case-rule line.

Take precisely the propositional tautologies as axioms and supply no inference rules. A one-line proof then establishes exactly the valid propositional formulas, so this calculus is sound and complete for theoremhood. Its axiom set is decidable by finite truth tables. This construction does not by itself give strong completeness for consequence from arbitrary assumptions.

An inference rule deriving a clause from two clauses containing complementary literals. In propositional logic the displayed rule eliminates the atom $A$. For first-order clauses, complementary atoms can first be made identical by a suitable first-order substitution.

A rule that combines first-order clauses by unifying complementary first-order literals and retaining the other literals under the resulting first-order substitution. Completeness requires the appropriate calculus and search conditions.

A family of resolution calculi for first-order Horn clauses. A selection function chooses either the positive head atom alone or a nonempty set of body atoms. Permitted inferences respect those choices; fair saturation is refutationally complete. Function symbols need not be excluded, so completeness does not by itself guarantee termination. ^[ref]

The use of resolution on ground clauses. A finite refutation ends in the empty ground clause and establishes unsatisfiability of the chosen ground instances. Herbrand's theorem explains the completeness of searching for such refutations for universal equality-free first-order clauses.