Mathematical Logic: Foundations, Proof, and Computation

1. Propositional Logic

Propositional logic is the simplest formal system, capturing reasoning about atomic statements combined with logical connectives. Every statement is either true or false — no quantification, no internal structure. Despite its simplicity, propositional logic underlies circuit design, SAT solving, and classical deduction.

Syntax and Connectives

A propositional formula is built from atomic propositions (p, q, r, ...) using connectives. The standard connectives are negation (NOT), conjunction (AND), disjunction (OR), implication (IMPLIES), and biconditional (IFF). Any formula can be written using only NOT and AND, or using only NOT and OR — these minimal sets are called functionally complete bases. Even a single connective suffices: NAND (NOT AND) is by itself functionally complete.

Truth Tables

A truth table lists the truth value of a compound formula for every possible assignment of truth values to its atomic propositions. For n propositions there are 2^n rows. Truth tables provide a complete decision procedure for propositional logic — a formula is a tautology if and only if every row shows TRUE.

Tautologies and Logical Equivalences

A tautology is a formula true under every truth assignment. A contradiction is always false. Two formulas are logically equivalent if they have identical truth tables. The most important equivalences form the algebraic laws of propositional logic.

Normal Forms: CNF and DNF

Every propositional formula can be converted to two standard forms. A literal is an atomic proposition or its negation. A clause is a disjunction of literals. Conjunctive Normal Form (CNF) is a conjunction of clauses — the standard input for SAT solvers. A minterm is a conjunction of literals. Disjunctive Normal Form (DNF) is a disjunction of minterms.

CNF is central to automated reasoning because SAT solvers work directly on CNF formulas using the DPLL algorithm or CDCL (Conflict-Driven Clause Learning). The satisfiability problem for CNF is NP-complete (3-SAT is the canonical instance).

2. Predicate Logic (First-Order Logic)

First-order logic (FOL) extends propositional logic with a richer language: variables ranging over a domain, function symbols, relation symbols (predicates), and quantifiers. It is the standard formal language of mathematics — virtually all classical mathematics can be expressed in first-order logic over appropriate axioms.

Syntax: Terms and Formulas

A first-order signature specifies constant symbols, function symbols (with arities), and relation symbols (with arities). Terms are built from variables and constants using function symbols. Atomic formulas apply a relation symbol to terms. Complex formulas combine atomics with propositional connectives and quantifiers.

Free and Bound Variables

A variable occurrence is bound if it falls within the scope of a quantifier binding that variable, and free otherwise. A sentence is a formula with no free variables — sentences have definite truth values in a given interpretation. Formulas with free variables express properties depending on how those variables are assigned.

Interpretations and Models

An interpretation (or structure) for a signature consists of: a non-empty domain D, an element of D for each constant, a function on D for each function symbol, and a relation on D for each relation symbol. A sentence is true in an interpretation if it holds when evaluated in that domain.

A model of a theory T is an interpretation in which every sentence of T is true. Semantic consequence (T entails phi, written T |= phi) means phi is true in every model of T. The central concern of model theory is the relationship between theories and their models.

Quantifier Laws and Prenex Normal Form

Quantifiers obey important laws governing their interaction with connectives and each other. Every first-order formula can be converted to Prenex Normal Form (PNF): a string of quantifiers followed by a quantifier-free matrix. PNF is used in the Herbrand theorem and undecidability proofs.

3. Proof Systems

A proof system provides formal rules for deriving conclusions from premises. The central meta-theoretic properties are soundness (every provable formula is valid) and completeness (every valid formula is provable). Different proof systems trade off between human readability and mathematical tractability.

Natural Deduction

Natural deduction, introduced by Gentzen in 1935, provides introduction and elimination rules for each connective. Proofs are trees of formulas. A key feature is the discharge of assumptions: from an assumption A derive B, then discharge A to conclude A IMPLIES B. This mirrors actual mathematical practice.

Sequent Calculus

Gentzen's sequent calculus LK operates on sequents of the form Gamma |- Delta, meaning: if all formulas in Gamma hold, then at least one formula in Delta holds. Structural rules (weakening, contraction, exchange) manipulate the context. Logical rules introduce connectives on left or right. The key result is the cut-elimination theorem: any proof using the cut rule can be converted to a cut-free proof.

Resolution

Resolution, introduced by Robinson in 1965, is the basis for automated theorem proving and logic programming (Prolog). The resolution rule: from clause (A OR C) and clause (NOT A OR D), derive clause (C OR D). To prove a formula phi, negate it, convert to CNF, and apply resolution until the empty clause (contradiction) is derived.

Hilbert Systems

Hilbert-style systems use a small set of axiom schemas and typically only modus ponens as an inference rule. Though proofs are cumbersome for humans, Hilbert systems are mathematically clean and easy to reason about meta-theoretically. The deduction theorem — if T plus A proves B then T proves A IMPLIES B — is a key meta-theorem.

Soundness and Completeness

Soundness: if phi is provable in the system, then phi is logically valid. Completeness: if phi is logically valid, then phi is provable. Together they mean proof and truth coincide. For propositional logic, truth tables give a simple decision procedure. For first-order logic, Gödel's completeness theorem (1929) establishes this equivalence.

4. Gödel's Completeness Theorem

Kurt Gödel's 1929 doctoral dissertation proved that first-order logic is complete. This established FOL as the right formal language for mathematics and culminated efforts to give logic solid meta-theoretic foundations.

Statement

Significance

Completeness means the proof rules of first-order logic are adequate — they capture all logical truths. If something is true in every model, there is always a finite proof of it. This justifies the axiomatic method: to reason about all models of a theory, it suffices to reason syntactically from the axioms.

The completeness theorem should not be confused with completeness of specific theories. First-order logic (the proof system) is complete. But specific theories like Peano arithmetic are incomplete — Gödel's incompleteness theorem addresses this distinct phenomenon.

Henkin Construction

The standard proof of completeness uses the Henkin construction. Given a consistent theory T, one builds a maximal consistent extension T* by adding new witness constants (Henkin constants) for each existential statement. The canonical model has the equivalence classes of terms as its domain, with interpretation determined by T*. This model satisfies exactly T.

5. Gödel's Incompleteness Theorems

In 1931, two years after his completeness theorem, Gödel published the most profound results in the history of mathematical logic. The incompleteness theorems showed that Hilbert's program — finding a complete, consistent, decidable axiomatization of all mathematics — is impossible.

Peano Arithmetic and Sufficient Strength

The theorems apply to any formal system F satisfying: (1) F is consistent, (2) F is recursively axiomatizable, and (3) F is sufficiently strong to express elementary arithmetic — specifically Peano Arithmetic (PA) or even the weaker Robinson arithmetic Q.

Gödel Numbering

The technical core of the incompleteness proofs is Gödel numbering: a systematic encoding of syntactic objects (symbols, formulas, proofs) as natural numbers. Each symbol gets a number; a sequence is encoded using prime factorization. This allows arithmetic to talk about its own syntax — every statement about provability becomes a statement about natural numbers.

Crucially, the provability predicate Prov(n) — meaning the formula with Gödel number n is provable in F — is expressible in the language of arithmetic. This enables self-reference via the Fixed Point (Diagonal) Lemma.

First Incompleteness Theorem

The Gödel sentence G_F is constructed by the Fixed Point Lemma to satisfy: G_F is equivalent (in F) to the claim that G_F is not provable in F. If F proves G_F, then G_F is false — contradiction. If F proves NOT G_F, then G_F is true but F has proved its negation — contradiction (by Rosser's improvement, just consistency suffices). Therefore neither is provable. G_F is in fact true in the standard model of arithmetic.

Second Incompleteness Theorem

The proof shows that if F proved Con(F), it could prove G_F — but G_F is unprovable. Con(F) can be expressed arithmetically as the claim that no Gödel number of a proof of 0=1 exists. The second theorem ended Hilbert's hope of finding a finitary consistency proof for all of mathematics within mathematics itself.

6. Computability Theory

Computability theory studies what can in principle be computed by an ideal machine with unlimited time and memory. It was developed independently by Turing, Church, Kleene, and Post in the 1930s, and the equivalence of their formalisms is a profound mathematical fact in itself.

Turing Machines

A Turing machine consists of: a finite set of states Q, a finite tape alphabet (including a blank symbol), a transition function delta(state, symbol) = (new state, new symbol, direction L/R), an initial state, and halting states. The machine reads and writes on an infinite tape, moving left or right. A function is Turing-computable if some Turing machine computes it — halting with the output whenever the function is defined, running forever otherwise.

Church-Turing Thesis

The Church-Turing thesis is the informal claim that any function computable by an effective procedure is Turing-computable. This is not a theorem — it cannot be proved because "effective procedure" is informal. But every proposed model of computation (lambda calculus, recursive functions, Post systems, RAM machines, cellular automata) turns out equivalent to Turing machines.

The Halting Problem

The halting problem is the canonical undecidable problem. Turing's 1936 proof is a masterpiece of diagonalization.

Rice's Theorem

Rice's theorem vastly generalizes the halting problem: any non-trivial semantic property of programs is undecidable. A property of partial functions is non-trivial if it is neither true of all functions nor false of all functions. Examples: whether a program computes a total function, whether it outputs 42 on some input, whether it computes the same function as another program — all undecidable by Rice's theorem.

Rice's theorem explains why program analysis is fundamentally limited: no general-purpose static analyzer can decide any interesting property of program behavior. Practical static analyzers are necessarily either unsound or incomplete.

Degrees of Unsolvability

Not all undecidable problems are equal. The Turing degree of a problem A is the equivalence class of problems Turing-reducible to A and vice versa. The halting problem is Turing-complete for the class of recursively enumerable (r.e.) sets. There exist infinitely many incomparable Turing degrees between decidable and the halting problem. The arithmetic hierarchy classifies problems by the quantifier alternation needed to define them.

7. Decidability of Theories

A first-order theory T is decidable if there exists an algorithm that determines, for any first-order sentence phi, whether T proves phi. Decidability results identify theories where automated reasoning is possible; undecidability results explain where it is not.

Decidable Theories

Undecidable Theories

Quantifier Elimination

A theory T admits quantifier elimination if every first-order formula is provably equivalent in T to a quantifier-free formula. Quantifier elimination directly yields decidability for theories with decidable quantifier-free fragments. The technique involves showing that existential quantifiers can be eliminated by algebraic manipulation, then iterating for nested quantifiers.

8. Model Theory

Model theory studies the relationship between formal languages and their interpretations (models). It asks: what structures satisfy a given theory? How do different models of the same theory relate? What properties can first-order logic express?

Compactness Theorem

Compactness follows from the completeness theorem: if every finite subset is satisfiable, every finite subset is consistent, hence T is consistent (by finiteness of proofs), hence T has a model. Applications include constructing non-standard models. Take T = PA plus sentences saying a new constant c exceeds each standard number. Every finite subset is satisfiable, so by compactness T has a model containing an element larger than every standard natural — a non-standard model with "infinite" elements.

Löwenheim-Skolem Theorems

Elementary Equivalence

Two structures M and N are elementarily equivalent (M equiv N) if they satisfy the same first-order sentences. Elementary equivalence is weaker than isomorphism — non-isomorphic structures can be elementarily equivalent. For example, the ordered field of real numbers R is elementarily equivalent to any non-standard real closed field, even though they are not isomorphic.

Ultraproducts

Given structures M_i (for i in an index set I) and an ultrafilter U on I, the ultraproduct is a new structure whose elements are equivalence classes of functions from I to the union of the M_i, with two functions identified if they agree on a set in U. By Los's theorem, a first-order sentence holds in the ultraproduct iff the set of indices where it holds is in U. Ultraproducts provide a powerful construction tool — non-standard analysis can be developed rigorously via ultraproducts of the reals.

9. Proof Theory

Proof theory studies proofs as mathematical objects, analyzing their structure, complexity, and information content. It was Hilbert's original approach to foundations, and though incompleteness showed its limits, proof theory remains vibrant with connections to computability and ordinal analysis.

Gentzen's Cut Elimination

The cut rule in sequent calculus allows using a lemma: derive A somewhere, then use A elsewhere. Cut elimination (Hauptsatz) proves that any proof with cuts can be transformed into a cut-free proof — at the cost of potentially enormous size increase (non-elementary in general).

Cut-free proofs have the subformula property: every formula appearing in the proof is a subformula of the endsequent. This makes cut-free proofs analyzable and yields consistency proofs. A cut-free proof of a contradiction in LK would have to contain the contradiction as a subformula from the start, which is impossible.

Ordinal Analysis

Gentzen proved consistency of PA in 1936 using transfinite induction up to the ordinal epsilon_0 (the smallest ordinal satisfying omega^x = x). This ordinal is the proof-theoretic ordinal of PA — a measure of the theory's strength. Each theory has a characteristic ordinal measuring how much transfinite induction it can prove.

Reverse Mathematics

Reverse mathematics, pioneered by Friedman and Simpson, asks which axioms are actually necessary to prove standard mathematical theorems. Working over a weak base theory (RCA_0, roughly computable mathematics), one determines the exact subsystem of second-order arithmetic needed for each theorem. Remarkably, most theorems fall into one of five systems (the "Big Five"), suggesting deep structural reasons for their equivalence.

10. Set Theory Connections

Set theory provides the standard foundational framework for all of mathematics. The Zermelo-Fraenkel axioms with Choice (ZFC) are the accepted foundation, and mathematical logic studies both what ZFC can prove and what it cannot.

ZFC Axioms

Independence Results

Gödel (1938) showed that the Axiom of Choice and the Continuum Hypothesis (CH, asserting 2^aleph_0 = aleph_1) are consistent with ZF by constructing the constructible universe L. Cohen (1963) showed that AC and CH are independent of ZF and ZFC respectively, using the method of forcing. Forcing builds new models by adjoining generic sets satisfying controlled properties.

Since Cohen, hundreds of set-theoretic statements have been shown independent of ZFC. The independence of CH means that neither "the real numbers have cardinality aleph_1" nor its negation follows from the standard axioms.

Large Cardinals

Large cardinal axioms assert the existence of very large infinite cardinals with strong reflection properties. They form a natural linear hierarchy of consistency strength beyond ZFC: inaccessible cardinals, Mahlo cardinals, measurable cardinals, Woodin cardinals, and supercompact cardinals. These axioms are not provable from ZFC (by the second incompleteness theorem) but are widely accepted as natural and justified by set theorists.

Measurable cardinals (those admitting a non-principal countably complete ultrafilter) are deeply connected to model theory — their existence is equivalent to the existence of a non-trivial elementary embedding from the universe V into a transitive inner model.

11. Type Theory and the Curry-Howard Correspondence

Type theory provides an alternative foundation for mathematics where types play the role of sets and terms play the role of elements. Unlike set theory, type theory is constructive by design and directly corresponds to functional programming — a proof is literally a program.

Simply Typed Lambda Calculus

Church's lambda calculus assigns a type to every term. Types are built from base types (nat, bool) using the function type constructor (A to B). A term of type A to B is a function taking terms of type A to terms of type B. The simply typed lambda calculus is strongly normalizing — all computations terminate — but not Turing-complete.

The Curry-Howard Correspondence

The Curry-Howard isomorphism reveals that the simply typed lambda calculus is the same thing as intuitionistic propositional logic, viewed from different angles. Propositions are types; proofs are programs.

Dependent Types

Dependent type theory allows types to depend on terms. The dependent function type Pi x:A. B(x) generalizes A to B when B does not depend on x. A term of type Pi x:A. B(x) is a function that takes a:A and produces a term of type B(a). This allows types to express precise specifications: the type of vectors of length n, or the type of proofs that p is prime.

Proof assistants like Coq (based on the Calculus of Constructions), Agda, and Lean use dependent types. In these systems, writing a function of the right type is the same as proving a theorem. The compiler type-checks the proof — no human referee needed.

Homotopy Type Theory (HoTT)

Homotopy Type Theory reinterprets Martin-Löf type theory through the lens of homotopy theory. The key insight (the univalence axiom, due to Voevodsky) is that equivalent types are identical. This gives a natural account of isomorphism invariance. HoTT provides a foundation where types are spaces, and proofs of equality are paths.

12. Applications: Formal Verification and Automated Reasoning

Mathematical logic is not merely foundational philosophy — it underpins practical tools for building reliable software, hardware, and databases.

Formal Verification

Formal verification uses mathematical proof to guarantee that a system meets its specification. Model checking exhaustively explores finite state spaces to verify temporal logic properties (safety: nothing bad ever happens; liveness: something good eventually happens). Deductive verification uses theorem provers to handle infinite-state systems via program annotations in Hoare logic or separation logic.

SAT Solvers

Modern SAT solvers decide propositional satisfiability for formulas with millions of variables. The DPLL algorithm (Davis-Putnam- Logemann-Loveland, 1962) uses backtracking search with unit propagation and pure literal elimination. CDCL (Conflict-Driven Clause Learning) adds conflict analysis that learns new clauses from dead ends, enabling dramatic performance gains.

SAT solvers are used in chip verification (bounded model checking), automated test generation, planning, and as back-ends for SMT solvers, which handle quantifier-free fragments of first-order theories like linear arithmetic and arrays.

Automated Theorem Proving

Automated theorem provers (ATPs) attempt to prove first-order theorems without human guidance. Resolution-based provers (Vampire, E, SPASS) apply resolution and paramodulation to clausified problems. They compete in the CASC competition on thousands of benchmark problems. ATPs are effective for discrete mathematics and algebraic problems.

Database Query Languages

Relational algebra and SQL are directly rooted in first-order logic. A relational database is a model (interpretation) of a first-order language where relations are table instances. Relational algebra operations (select, project, join, union, difference) correspond to first-order formula operations. Codd's theorem establishes the equivalence of relational algebra and domain relational calculus, a fragment of first-order logic.

Datalog — a restricted logic programming language — has exactly the expressive power of least fixed-point logic on finite structures, and is used in program analysis, knowledge graphs, and network analysis.

Interactive Theorem Provers

Interactive theorem provers (ITPs) require human guidance but verify every step mechanically. The main systems are: Coq (Calculus of Inductive Constructions), Lean 4 (dependent type theory, with the growing Mathlib library), Isabelle/HOL (classical higher-order logic), and Agda (Martin-Löf type theory). ITPs are increasingly used for research-level mathematics.

13. Practice Problems

Work through these problems to solidify your understanding. Click to reveal the solution after attempting each problem.

Quick Reference: Key Results

Further Study