Axiom Systems and Theorems of Completeness

Motivation: Do “True” and “Provable” Coincide?

In propositional logic, we have two independent concepts: semantics (what is true under every assignment) and syntax (what is derived from axioms by rules). The completeness theorem states their equivalence: everything semantically true is provable. The soundness theorem asserts the converse: everything provable is true. Together, they guarantee the adequacy of the formal system.

Propositional Calculus (Hilbert-Style)

Axioms:

(A1) φ → (ψ → φ) — "weakening"
(A2) (φ → (ψ → χ)) → ((φ → ψ) → (φ → χ)) — "distribution"
(A3) (¬ψ → ¬φ) → (φ → ψ) — "contraposition"

The sole inference rule: Modus Ponens (MP): from φ and φ → ψ derive ψ.

Derivation from Γ: a sequence φ₁, ..., φₙ, where each φᵢ is either an axiom, belongs to Γ, or is obtained from previous formulas using MP. Γ ⊢ φ — φ is derivable from Γ.

Theorems of Soundness and Completeness

Soundness Theorem: Γ ⊢ φ ⟹ Γ ⊨ φ. Proof: induction on the length of the derivation. Axioms are tautologies; MP preserves truth.

Completeness Theorem (Post 1921): Γ ⊨ φ ⟹ Γ ⊢ φ. Every semantic consequence is syntactically provable. This means: the axiom system is "sufficient" for the whole of classical logic.

Deduction Theorem: Γ ∪ {φ} ⊢ ψ ⟺ Γ ⊢ φ → ψ. A hypothesis can be "moved" into the antecedent of an implication.

Compactness Theorem: Γ ⊨ φ ⟺ there exists a finite Γ₀ ⊂ Γ such that Γ₀ ⊨ φ. Equivalently: Γ is satisfiable ⟺ every finite subset is satisfiable.

Functional Completeness

Basis of connectives: a set through which all others are expressible.

{¬, ∧} is a basis: p∨q ≡ ¬(¬p∧¬q).
{NAND} is one-element: p NAND q ≡ ¬(p∧q); ¬p ≡ p NAND p.
{NOR} is one-element: p NOR q ≡ ¬(p∨q).

Criterion of functional completeness (Post): A set F is functionally complete ⟺ it is not contained in any of the five Post classes (monotone, self-dual, T-preserving, F-preserving, linear).

Numeric Example

Task: Derive p → p in the Hilbert system.

Step 1. Write A2 with φ = p, ψ = (p→p), χ = p: (p→((p→p)→p)) → ((p→(p→p)) → (p→p)). — (1)

Step 2. A1 with φ = p, ψ = (p→p): p→((p→p)→p). — (2)

Step 3. A1 with φ = p, ψ = p: p→(p→p). — (3)

Step 4. MP from (1) and (2) — eliminate the first antecedent (1): (p→(p→p)) → (p→p). — (4)

Step 5. MP from (4) and (3): p→p. ■

Final derivation write-up:

p→((p→p)→p) [A1]
(p→((p→p)→p))→((p→(p→p))→(p→p)) [A2]
(p→(p→p))→(p→p) [MP from 2,1]
p→(p→p) [A1]
p→p [MP from 3,4]

Verification: p→p is a tautology (for p=0: 0→0=1; for p=1: 1→1=1) ✓.

Real-World Application

Automated theorem proving (ATP): systems like Prover9, E-prover use the completeness of logic to automatically search for proofs. The deduction theorem is a key tool for converting the problem "prove A ⊨ B" into the problem "is ¬(A→B) satisfiable?" (via negation).

Additional Aspects

Axiom systems are not limited to Hilbert-style calculus with modus ponens, but also include natural deduction systems (Gentzen, Pratt), sequent calculi, and tableau methods. The soundness (everything provable is true) and completeness (everything true is provable) theorems for propositional logic were fully established by the 1920s. Completeness for first-order predicate logic (Gödel’s theorem, 1929) is much deeper: it asserts that syntactic derivation captures all semantic consequences and is used in any modern automatic theorem prover. For intuitionistic and modal logics, there are their own completeness theorems with respect to Kripke models.

Relation to Other Areas of Mathematics

Theorems of completeness and compactness naturally go beyond pure logic and are part of the repertoire of modern mathematicians. In model theory, they are used for transferring results between algebraic structures. A classic example is the axiomatization of fields: first-order logic completeness allows formalizing the proof of Tarski's theorem that the theory of real closed fields is model complete and admits quantifier elimination; from this follows the elementary equivalence of all real closed fields of a given characteristic. This is directly related to real analysis and differential equations, where such fields serve as "generalized" continua.

In abstract algebra, the Löwenheim–Skolem theorem and compactness yield nontrivial consequences: for instance, the existence of uncountable models of countable theories of groups, rings, fields. Malcev’s result on locally finite groups relies on model-theoretic methods, where logic’s completeness enables the transition from “all finite substructures satisfy ...” to the existence of a model for the entire axiom system.

In topology, logical methods manifest through the construction of the Stone space for the Boolean algebra of propositions. Stone’s representation (1936) connects Boolean algebras to compact totally disconnected spaces; the completeness of classical logic is expressed here by the fact that every consistent set of formulas is realized by an ultrafilter, that is, a point of such a space.

In probability theory, Kolmogorov’s axiomatics (1933) are formulated in the language of set theory logic: the soundness and completeness of systems like ZFC set the boundaries of what can be formally justified about probabilistic models. In numerical methods and computational mathematics, completeness of propositional logic underlies the soundness of SAT solvers: the model search algorithm essentially implements the semantic side, and the resulting resolution proofs are interpreted as syntactic derivations (the completeness of resolution for propositional logic was proved by Robinson in 1965).

Historical Note and Development of the Idea

Semantic completeness of classical logic was gradually recognized in the early 20th century. For the propositional calculus, the first rigorous proofs are attributed to Emil Post (1921) and the associated tradition of Hilbert-type axiomatics. Completeness of first-order logic was established by Kurt Gödel in 1929 in an article in Monatshefte für Mathematik und Physik: he showed that if a formula is true in all models, then there is a derivation in the standard axiomatics. This became the foundation of a new field—proof theory and model theory. Motivating problems came from Hilbert’s program: to formalize all of mathematics and justify its consistency using purely syntactic means. The logical systems of Frege and post-cardano developments by Peano and Weyl prepared the ground for posing the question of the coincidence of “logical truth” and “provability.” In parallel, Post and Sheffer investigated functional completeness of connectives, preparing the algebraic outlook on logic. In the mid-20th century, after the works of Gödel, Tarski, Henkin, Löwenheim, and Skolem, model theory took shape as an independent field.