Mathematical logic is a subfield of mathematics that formalizes the principles of reasoning and inference using symbolic systems. It encompasses the study of formal languages, axiomatic systems, proof theory, model theory, recursion theory, and set theory. Originating in the 19th and early 20th centuries from the work of logicians such as George Boole, Gottlob Frege, and Kurt Gödel, mathematical logic provides the foundational framework for mathematics and computer science, allowing precise analysis of truth, provability, and computability.
1 Historical development
1.1 Origins in Aristotelian logic
The systematic study of logic began with Aristotle in the 4th century BCE. His *Organon* introduced the syllogism—a form of reasoning consisting of two premises and a conclusion. Aristotelian logic dominated Western thought for over two millennia, focusing on categorical propositions and their relationships. While powerful, it lacked the expressive and formal precision needed to handle complex mathematical statements.
1.2 Boolean algebra and propositional logic
In the mid‑19th century, George Boole developed an algebraic system that encoded logical operations (conjunction, disjunction, negation) as algebraic equations. His work, presented in *The Laws of Thought* (1854), provided the first symbolic treatment of propositional logic. Boolean algebra became the foundation for digital circuit design and remains a core tool in computer science.
1.3 Frege's predicate logic
Gottlob Frege, in his *Begriffsschrift* (1879), introduced a fully formalized system of predicate logic, including quantifiers and variables. He separated the logical form of statements from their content, enabling the representation of relations and quantificational reasoning. Frege’s work laid the groundwork for modern first‑order logic and influenced the development of analytic philosophy.
1.4 Logical positivism and the Hilbert program
In the early 20th century, the Vienna Circle advanced logical positivism, holding that meaningful statements are either empirically verifiable or logically true. David Hilbert proposed a formalist program aimed at proving the consistency of all mathematics using finitary methods. This program inspired intensive research into axiomatic systems and proof theory.
1.5 Gödel's incompleteness theorems
In 1931, Kurt Gödel published his two incompleteness theorems, which shattered Hilbert’s dream. The first theorem states that any consistent formal system strong enough to encode arithmetic contains a true but unprovable sentence. The second theorem shows that such a system cannot prove its own consistency. These results established fundamental limits on formal proof and marked a turning point in mathematical logic.
2 Propositional logic
Propositional logic (also called sentential logic) studies the truth‑functional relationships between propositions. Its basic units are atomic propositions, which are combined using logical connectives to form compound formulas.
2.1 Syntax and semantics
The syntax of propositional logic defines the well‑formed formulas (wffs): atomic propositions and their combinations via connectives. The semantics assigns truth values (true or false) to each atomic proposition and determines the truth value of any compound formula according to the meaning of the connectives.
2.1.1 Logical connectives
The standard connectives are negation (¬), conjunction (∧), disjunction (∨), implication (→), and biconditional (↔). Each connective has a fixed truth‑functional definition: for example, ¬p is true exactly when p is false; p ∧ q is true only when both p and q are true.
2.1.2 Truth tables
A truth table lists all possible truth‑value assignments to the atomic propositions and shows the resulting truth value of a compound formula. Truth tables provide a complete semantic evaluation method for finite formulas and are used to define equivalence and validity.
2.2 Tautologies and contradictions
A tautology is a formula that is true under every possible assignment (e.g., p ∨ ¬p). A contradiction is false under every assignment (e.g., p ∧ ¬p). Tautologies represent logical truths, while contradictions represent logical falsehoods. Satisfiable formulas are those that are true under at least one assignment.
2.3 Logical equivalence and normal forms
Two formulas are logically equivalent if they have the same truth value for every assignment. This equivalence is fundamental for simplifying formulas and for reasoning about circuits and programs. Normal forms provide a canonical representation.
2.3.1 Disjunctive normal form
A formula is in disjunctive normal form (DNF) if it is a disjunction (OR) of conjunctions (AND) of literals (atomic propositions or their negations). Every propositional formula can be transformed into an equivalent DNF.
2.3.2 Conjunctive normal form
A formula is in conjunctive normal form (CNF) if it is a conjunction (AND) of disjunctions (OR) of literals. CNF is especially important in automated theorem proving and SAT‑solving algorithms, as it provides a standard input format.
2.4 Soundness and completeness
A proof system for propositional logic is *sound* if every provable formula is a tautology, and *complete* if every tautology is provable. Classical propositional logic has many sound and complete proof systems (e.g., natural deduction, Hilbert systems). These properties ensure that syntactic deduction exactly captures semantic truth.
3 Predicate logic
Predicate logic extends propositional logic by allowing quantification over objects and by representing relations and functions. It provides a much richer language for expressing mathematical statements.
3.1 First-order logic
First‑order logic (FOL) is the most widely used logical system. It includes variables, quantifiers (∀, ∃), predicate symbols, function symbols, and equality. FOL can formalize statements such as “every natural number has a successor” and “there exists a prime greater than 2.”
3.1.1 Quantifiers and variables
The universal quantifier ∀x φ(x) means “for all x, φ(x) holds”; the existential quantifier ∃x φ(x) means “there exists an x such that φ(x) holds.” Variables range over the domain of discourse, and quantifiers can be seen as infinite conjunctions/disjunctions.
3.1.2 Terms and formulas
Terms are expressions built from variables, constants, and function symbols (e.g., f(x, g(y))). Atomic formulas consist of a predicate symbol applied to terms (e.g., P(x, f(c))). Complex formulas are built by connecting atomic formulas with logical connectives and adding quantifiers.
3.1.3 Models and interpretations
A model (or structure) for a first‑order language consists of a domain (a set of objects) and interpretations for each constant, function, and predicate symbol. An interpretation assigns meaning to each variable by an assignment function. A formula is true in a model if it holds under the given assignment; otherwise it is false.
3.2 Second-order and higher-order logics
Second‑order logic extends first‑order logic by allowing quantification over sets of objects and over relations. Higher‑order logic extends this to arbitrary types. These systems have greater expressive power (e.g., they can characterize natural numbers up to isomorphism) but are not complete in the sense of Gődel’s completeness theorem.
3.3 Completeness and compactness theorems
Gődel’s completeness theorem (1930) states that first‑order logic is complete: every logically valid formula is provable in a suitable deductive system. The compactness theorem follows: a set of formulas has a model iff every finite subset has a model. These theorems are fundamental tools in model theory.
3.4 Lindström's theorem
Lindström’s theorem (1969) characterizes first‑order logic as the strongest logic that satisfies both the compactness theorem and the Löwenheim–Skolem theorem (downward version). It provides a precise sense in which first‑order logic is the natural logic for expressing “elementary” mathematical structures.
4 Proof theory
Proof theory studies the structure of formal proofs and the relation between syntax and semantics. It originated in Hilbert’s program and has developed powerful methods for analyzing logical systems.
4.1 Axiomatic systems
An axiomatic system consists of a set of axioms (basic truths) and inference rules (rules for deriving new truths from old ones). Proofs are finite sequences of formulas, each of which is an axiom or follows from earlier formulas by an inference rule.
4.1.1 Hilbert-style deduction
Hilbert‑style systems have many axioms and few inference rules (typically modus ponens). They are easy to reason about metamathematically but often cumbersome for actual theorem proving. Their main use is in proving soundness and completeness.
4.1.2 Natural deduction
Natural deduction, introduced by Gentzen (1934), uses inference rules that mimic natural reasoning: introduction and elimination rules for each connective and quantifier. It is closer to how mathematicians actually argue and is well‑suited for proof assistants.
4.1.3 Sequent calculus
Also due to Gentzen, sequent calculus works with sequents (Γ ⊢ Δ), meaning “from assumptions Γ, at least one formula in Δ follows.” It provides a symmetric presentation of logical rules and is especially useful for studying cut elimination and consistency.
4.2 Cut elimination and normalization
The cut rule in sequent calculus (analogous to using a lemma) can be eliminated: every proof can be transformed into a cut‑free proof. This result (Gentzen’s Hauptsatz) leads to the subformula property—every formula appearing in a cut‑free proof is a subformula of the conclusion or of an axiom. Normalization for natural deduction achieves a similar effect.
4.3 Consistency and independence results
Proof‑theoretic methods are used to establish consistency of formal theories (e.g., Gentzen’s consistency proof for arithmetic using transfinite induction). Independence results show that a certain statement is not provable from given axioms, often by constructing a model where the statement fails.
5 Model theory
Model theory studies the relationship between formal languages and their interpretations (models). It investigates what classes of structures can be defined by a given theory and how properties of structures are reflected in their theories.
5.1 Structures and elementary classes
A structure is a set equipped with functions, relations, and distinguished elements. An elementary class is the collection of all models of a first‑order theory. Model theory analyzes the expressive power of first‑order logic: for example, the class of all groups is elementary, but the class of all finite groups is not.
5.2 Compactness and Löwenheim–Skolem theorems
The compactness theorem (see §3.3) and the Löwenheim–Skolem theorems are central to model theory. The Löwenheim–Skolem theorem states that if a countable first‑order theory has an infinite model, then it has models of every infinite cardinality. The downward version provides countable models, and the upward version provides models of arbitrarily large cardinalities.
5.3 Types and saturation
A (complete) type is a maximal consistent set of formulas with free variables. Types describe the possible behavior of an element (or tuple) in a model. A model is κ‑saturated if it realizes all types over subsets of size < κ. Saturated models are “rich” and often used to characterize theories.
5.4 Stability theory and classification
Stability theory, developed by Shelah in the 1970s, classifies first‑order theories according to the number of types they have over a given set of parameters. Stable theories (e.g., algebraically closed fields) admit a well‑behaved notion of independence and allow a classification of their models up to isomorphism. Unstable theories (e.g., the theory of dense linear orders) are more complex.
6 Recursion theory
Recursion theory, also called computability theory, studies the formal notion of effective calculability and the limits of algorithmic methods. It originated in the work of Gödel, Church, Turing, and Post in the 1930s.
6.1 Computable functions and Turing machines
A function is computable if there exists an algorithm (a Turing machine, a recursive function definition, another computational model) that produces its output for any valid input. The Church–Turing thesis states that these formal models capture the intuitive notion of effective computation. Turing machines are the most widely used model.
6.2 Decidability and undecidability
A decision problem (a set of yes‑no questions) is *decidable* if there is an algorithm that correctly answers all instances. It is *undecidable* if no such algorithm exists. Many problems in mathematics and computer science are undecidable.
6.2.1 Halting problem
The halting problem asks whether a given Turing machine, when started on a given input, eventually halts. Turing (1936) proved that no algorithm can solve this problem for all machines and inputs. It is the canonical example of an undecidable problem.
6.2.2 Rice's theorem
Rice’s theorem (1953) states that any non‑trivial property of the language recognized by a Turing machine is undecidable. “Non‑trivial” means that some languages have the property and some do not. Thus, almost all interesting questions about program behavior are undecidable.
6.3 Recursively enumerable sets
A set of natural numbers is recursively enumerable (r.e.) if it is the domain of a partial computable function—equivalently, if there is an algorithm that lists its elements. (The algorithm may not halt for numbers not in the set.) The halting set (the set of indices of Turing machines that halt on their own index) is r.e. but not computable.
6.4 Degrees of unsolvability
Two sets are Turing‑equivalent if each is computable from the other (using the other as an oracle). The equivalence classes are called Turing degrees. The Turing degrees form a partial order with a least element (the computable sets) and infinite chains of increasing unsolvability. The study of degrees is a central part of recursion theory.
7 Set theory
Set theory provides a foundation for virtually all of mathematics by formalizing the notion of a set. It studies infinite numbers (cardinals and ordinals) and the limits of axiomatization.
7.1 Axiomatic set theory
Axiomatic set theory avoids the paradoxes (e.g., Russell’s paradox) by restricting comprehension. The most common foundation is Zermelo–Fraenkel set theory with the Axiom of Choice (ZFC).
7.1.1 Zermelo–Fraenkel axioms
ZF consists of axioms: Extensionality (sets are equal if they have the same elements), Pairing, Union, Power Set, Infinity, Replacement (or Separation), and Foundation (Regularity). These axioms define the cumulative hierarchy of sets, built from the empty set by repeatedly taking power sets and unions.
7.1.2 Axiom of choice and its equivalents
The Axiom of Choice (AC) states that for any family of non‑empty sets, there exists a choice function selecting one element from each set. AC is independent of ZF. Its equivalents include Zorn’s Lemma, the Well‑Ordering Theorem, and the comparability of cardinals. AC is used in many proofs in analysis, algebra, and topology.
7.2 Ordinal and cardinal numbers
Ordinal numbers extend the natural numbers to represent order types of well‑ordered sets. Cardinal numbers measure the size of sets (including infinite sizes). The continuum hypothesis (CH) states that there is no cardinal between ℵ₀ (the size of natural numbers) and 2^ℵ₀ (the size of the continuum). CH is independent of ZFC.
7.3 Forcing and independence proofs
Forcing, invented by Paul Cohen (1963), is a method for constructing new models of set theory. Cohen used it to prove that both the Continuum Hypothesis and the Axiom of Choice are independent of ZF. Forcing has become an essential tool for establishing the consistency and independence of many set‑theoretic statements.
7.4 Large cardinals and inner models
Large cardinals (e.g., inaccessible, measurable, Woodin cardinals) are axioms asserting the existence of very large infinite sets. They are not provable in ZFC but yield much richer set‑theoretic universes. Inner model theory constructs canonical models (such as Gödel’s constructible universe L) that contain large cardinals and provide a finer understanding of the set‑theoretic hierarchy.
8 Applications and connections
Mathematical logic has deep connections with other areas of mathematics and computer science, and it raises important philosophical questions.
8.1 Foundations of mathematics
Set theory (particularly ZFC) provides the standard foundation for all of mathematics. Most mathematical objects (numbers, functions, spaces) can be defined as sets, and theorems are provable from the axioms. The search for new axioms (e.g., large cardinal axioms) continues to be an active area of foundational research.
8.2 Computational complexity and logic
Descriptive complexity theory uses logical formulas to characterize complexity classes. For example, the class P (polynomial time) is captured by first‑order logic with least fixed point, while NP is captured by existential second‑order logic (Fagin’s theorem). This connection allows the translation of complexity‑theoretic questions into logical ones.
8.3 Automated theorem proving
Algorithms that automatically prove theorems (or find proofs) rely heavily on logical methods. Resolution for first‑order logic, SAT‑solvers (for propositional logic), and SMT‑solvers (satisfiability modulo theories) are used in software verification, program synthesis, and formal mathematics.
8.4 Philosophical implications
Mathematical logic addresses deep philosophical issues: the nature of truth (e.g., Tarski’s undefinability theorem), the limits of formal reasoning (Gödel’s theorems), and the foundations of mathematics (formalism, intuitionism, Platonism). It also informs debates about artificial intelligence, machine reasoning, and the possibility of automating mathematical discovery.