Mathematical Logic

First-order logic (FOL), also called predicate logic or first-order predicate calculus, extends propositional logic with predicates, quantifiers (∀, ∃), and terms built from variables, constants, and functions, allowing statements about objects and their properties and relations. A first-order language is specified by a signature: a set of constant symbols, function symbols, and predicate (relation) symbols, together with logical symbols shared across all languages (connectives, quantifiers, variables, equality). Quantifiers range only over individual objects in a domain of discourse — not over sets, functions, or predicates themselves, which is what distinguishes 'first-order' from 'second-order' logic, where quantification over predicates or functions is allowed. First-order logic is the standard formal backbone of most of mathematics, including the axiomatizations of set theory (ZFC) and arithmetic (Peano arithmetic).

Modal logic extends propositional (or predicate) logic with operators expressing modes of truth beyond plain true/false — most commonly necessity (□, 'it is necessarily the case that') and possibility (◇, 'it is possibly the case that'), which are interdefinable via ◇φ ≡ ¬□¬φ. Its standard semantics, due to Saul Kripke, interprets formulas relative to a set of 'possible worlds' connected by an accessibility relation R, where □φ is true at a world w if φ is true at every world accessible from w, and ◇φ is true at w if φ is true at some accessible world. Different constraints on the accessibility relation (reflexive, transitive, symmetric, etc.) yield different modal systems — K (no constraints), T (reflexive), S4 (reflexive + transitive), and S5 (equivalence relation) — each validating different additional axioms. Beyond necessity/possibility, the same Kripke-world framework underlies temporal logic (□ = 'always,' ◇ = 'eventually'), epistemic logic (□ = 'it is known that'), and deontic logic (□ = 'it is obligatory that').

Second-order logic extends first-order logic by allowing quantification not only over individual elements of a domain (∀x, ∃x) but also over predicates, relations, functions, and subsets of the domain (∀P, ∃P). This extra expressive power lets second-order logic pin down structures that first-order logic provably cannot: the second-order induction axiom for arithmetic, 'every set containing 0 and closed under successor contains all natural numbers' (∀P [(P(0) ∧ ∀x(P(x)→P(x+1))) → ∀x P(x)]), categorically characterizes the standard natural numbers up to isomorphism, whereas first-order Peano arithmetic always has nonstandard models by the compactness theorem. This power comes at a steep price, established by Lindström's theorem and related results: second-order logic under its standard (full) semantics has no sound and complete proof system, is not compact, and does not satisfy any analogue of the Löwenheim–Skolem theorem, meaning many of the well-behaved 'finiteness' and proof-theoretic tools of first-order logic simply fail. A widely used compromise is Henkin semantics, in which the second-order quantifiers range only over a specified subset of all possible predicates/relations (rather than literally all of them); under Henkin semantics, second-order logic behaves exactly like a many-sorted first-order logic, regaining compactness and a complete proof system, but losing the categoricity that made full second-order logic attractive in the first place.

A formal proof system consists of a formal language, a set of axioms (formulas assumed true without proof), and a set of inference rules that license deriving new formulas from previous ones purely by syntactic pattern-matching, with no appeal to meaning. A formal proof (or derivation) of a formula φ is a finite sequence of formulas ending in φ, where each formula is either an axiom or follows from earlier formulas by an inference rule; if such a derivation exists we write ⊢ φ ('φ is a theorem' or 'φ is provable'). Common formal proof systems include Hilbert-style systems (few inference rules, many axiom schemas), natural deduction (many introduction/elimination rules, few or no axioms), and sequent calculus, all of which can be shown to prove exactly the same theorems for a given logic despite looking very different. The central achievement of proof theory is separating this syntactic notion of provability (⊢) from the semantic notion of truth in a model (⊨), a distinction made precise by the soundness and completeness theorems.

Gödel's two incompleteness theorems (1931) are among the most significant results in mathematical logic. The first incompleteness theorem states that any consistent formal system F that is recursively axiomatizable (its axioms can be listed by an algorithm) and strong enough to express basic arithmetic (e.g. Peano arithmetic or anything encoding it) contains true statements about the natural numbers that F cannot prove or disprove. The second incompleteness theorem, a corollary of the first's proof method, states that such a system F cannot prove its own consistency (a statement 'Con(F)' expressible within F itself) unless F is actually inconsistent. These theorems apply specifically to sufficiently powerful, recursively axiomatizable, consistent formal systems — not to every conceivable formal or informal system, and not to logic in general (they do not contradict Gödel's own 1930 completeness theorem for first-order logic, which is a separate, different-scope result).

Proof by contradiction (reductio ad absurdum) establishes a statement P by assuming its negation ¬P and deriving a logical contradiction — typically a statement of the form Q ∧ ¬Q — from that assumption together with known facts. Because a contradiction can never be true, and ¬P led to one, ¬P must be false, so P must be true. This method relies on the law of excluded middle (P ∨ ¬P) and, in its full strength, is generally rejected by constructive/intuitionistic logic, which accepts only the weaker principle that ¬¬P does not immediately give P without further construction. It is the classical proof strategy behind landmark results such as the irrationality of √2 and the infinitude of primes.

Proof by contrapositive establishes a conditional statement P → Q by instead proving the logically equivalent statement ¬Q → ¬P: assume the conclusion fails and show the hypothesis must fail too. This works because p → q and ¬q → ¬p are logically equivalent (identical truth tables), so proving one legitimately proves the other. Unlike proof by contradiction, which assumes ¬P and can invoke any accumulated fact to reach an arbitrary contradiction, contrapositive proof is a direct proof of a specific different statement (¬Q → ¬P) and is accepted even in constructive/intuitionistic logic. It is especially useful when the direct implication P → Q is hard to unpack but its negated, reversed form is comparatively straightforward — often when Q's negation gives a clean algebraic or structural property to work with.

Proof by cases (also called proof by exhaustion or case analysis) establishes a statement P by splitting the situation into finitely many sub-situations C₁, C₂, ..., Cₙ that together cover every possibility, and then proving P separately within each case. The method rests on a simple disjunction: if C₁ ∨ C₂ ∨ ... ∨ Cₙ is guaranteed to hold (the cases are exhaustive), and P follows from each Cᵢ individually, then P follows overall — there is no gap between the cases for a counterexample to hide in. Two things must be checked with care: exhaustiveness (the cases really do cover every possibility, with no situation falling through the cracks) and validity within each case (the argument for P under Cᵢ must actually only use the assumption Cᵢ, not sneak in facts that hold elsewhere). The method is often the natural response when a direct or contrapositive argument would otherwise require juggling several unrelated sub-arguments at once, and it becomes proof by exhaustion in the extreme when the 'cases' are simply every element of a large but finite set, as in the 1976 computer-assisted proof of the four color theorem.

Many mathematical claims assert that an object with a certain property exists, or that it exists and is the only one with that property — written formally with the quantifiers ∃x P(x) (existence) and ∃!x P(x) (existence and uniqueness). These are logically two separate obligations that are easy to conflate: existence shows that at least one object satisfies P, while uniqueness shows that at most one object does, and only together do they pin down 'exactly one.' Existence proofs come in two flavors: constructive proofs that explicitly exhibit a witness object (or an algorithm producing one), and non-constructive proofs that establish existence indirectly — for instance via contradiction, the pigeonhole principle, or a counting/dimension argument — without ever displaying the object itself. Uniqueness proofs almost always follow one recipe: assume two objects a and b both satisfy P, then show a = b, so there cannot really be two different ones.

Natural deduction is a formal proof system, introduced independently by Gerhard Gentzen and Stanisław Jaśkowski in 1934, designed to mirror the way mathematicians actually reason rather than to minimize the number of primitive axioms. Instead of a handful of axiom schemas and one inference rule (as in Hilbert-style systems), natural deduction gives every logical connective and quantifier a matched pair of rules: an introduction rule, showing how to derive a formula whose main connective is that symbol, and an elimination rule, showing what can be derived from such a formula. Its signature device is the discharged assumption: to prove an implication φ → ψ, you temporarily assume φ, derive ψ under that assumption, and then discharge (retract) the assumption, packaging the whole sub-argument into a single implication that no longer depends on φ. This assumption-and-discharge bookkeeping is exactly how conditional and indirect proofs are written in ordinary mathematical practice, which is why natural deduction (and its descendant, sequent calculus) is the proof system of choice for proof assistants like Coq, Lean, and Isabelle.

Resolution, introduced by John Alan Robinson in 1965, is a single, uniform inference rule that is refutation-complete for both propositional and first-order logic, meaning it can, in principle, detect the unsatisfiability of any inconsistent set of clauses. A clause is a disjunction of literals; the resolution rule takes two clauses that contain complementary literals (one has p, the other ¬p) and produces a new clause — the resolvent — consisting of the remaining literals of both, with the complementary pair removed. To prove a first-order sentence φ follows from a set of premises, resolution theorem provers negate φ, convert everything to clausal (conjunctive normal) form, and repeatedly resolve clauses looking for the empty clause □ (a contradiction); reaching □ certifies that the premises plus ¬φ are unsatisfiable, hence the premises entail φ. In first-order logic, resolving clauses with variables requires unification — the process of finding a substitution that makes two terms syntactically identical — and Robinson's unification algorithm computes a most general unifier (mgu), the least-committal substitution that works, from which every other unifying substitution can be obtained by further instantiation. This combination of resolution and unification is the theoretical engine behind automated theorem provers and the logic programming language Prolog.

The deduction theorem is a metatheorem — a theorem about a formal proof system rather than a theorem stated within it — asserting that Γ ∪ {φ} ⊢ ψ if and only if Γ ⊢ φ → ψ. In Hilbert-style systems, where the only inference rule is typically modus ponens and there is no built-in way to 'assume and discharge' a hypothesis, this equivalence is not automatic; it must be proved, by an induction on the length of the derivation of ψ from Γ ∪ {φ}, showing how to systematically eliminate φ as a bare assumption and replace every line of the original derivation with a corresponding derivation of φ → (that line), using only the axioms and modus ponens. The theorem is what licenses the informal habit, universal in ordinary mathematics, of writing 'assume φ; ...; therefore φ → ψ' — in a Hilbert system that convenience must be earned by the theorem's proof, whereas in natural deduction the analogous move (→-introduction) is simply built directly into the system as a primitive rule. The deduction theorem's converse direction is essentially just one application of modus ponens, so the mathematical content lies entirely in the forward direction.

Intuitionistic logic, formalized by Arend Heyting in 1930 to capture L. E. J. Brouwer's constructivist philosophy of mathematics, rejects the law of excluded middle (φ ∨ ¬φ) as a universally valid principle, along with double-negation elimination (¬¬φ → φ), demanding instead that every proof of a disjunction φ ∨ ψ explicitly exhibit which disjunct holds, and every proof of an existential ∃x φ(x) explicitly exhibit a witness. Classically, φ ∨ ¬φ is true regardless of whether anyone can decide which disjunct holds — it is simply guaranteed by the two-valued semantics of truth tables — but intuitionistically, asserting φ ∨ ¬φ means possessing an actual method that either proves φ or proves ¬φ, and for many undecided mathematical statements no such method is known to exist, so the disjunction is not intuitionistically assertable. This gives intuitionistic logic a computational, constructive reading formalized precisely by the Curry–Howard correspondence, under which intuitionistic proofs correspond exactly to programs (terms in typed lambda calculus) and propositions correspond to types — a proof of φ → ψ literally IS a program transforming any witness of φ into a witness of ψ. Intuitionistic logic is strictly weaker than classical logic (every intuitionistically provable formula is classically provable, but not conversely) and is the logic underlying constructive mathematics and proof assistants such as Coq and Agda.

Proof theory studies formal proofs as mathematical objects. It investigates what can be proved, how efficiently, and at what logical strength. Key topics include cut elimination, ordinal analysis of theories, consistency proofs, and the relationship between proof systems and computational complexity.

Reverse mathematics asks: which axioms are actually necessary to prove a given theorem? Instead of proving theorems from axioms, one proves that specific axioms are equivalent to specific theorems over a weak base theory. Most theorems of ordinary mathematics fall into exactly five levels (the 'Big Five'), revealing a remarkable classification of mathematical content by logical strength.

A logical connective is an operation that combines one or more propositions into a new proposition, whose truth value is determined entirely by the truth values of its inputs. The standard connectives are negation (¬, unary), conjunction (∧, 'and'), disjunction (∨, 'or', inclusive), the conditional (→, 'implies'), and the biconditional (↔, 'if and only if'); XOR and NAND/NOR are common derived or minimal alternatives. Every one of these connectives is truth-functional — its output depends only on the truth values of its arguments, never on their content or context — which is what makes truth tables a complete method for evaluating any propositional formula. A small set of connectives, such as {¬, ∧} or the single NAND connective, is functionally complete, meaning every possible truth function can be built from it alone.

A truth table is a complete tabular listing of the truth value of a propositional formula for every possible combination of truth values of its variables. A formula with n distinct propositional variables has exactly 2ⁿ rows, since each variable independently takes one of two values. Truth tables provide a mechanical, exhaustive method to determine whether a formula is a tautology (true in every row), a contradiction (false in every row), a contingency (true in some rows and false in others), or logically equivalent to another formula (identical truth-value columns). Because propositional logic's connectives are all truth-functional, truth tables are a complete decision procedure for propositional validity, though the 2ⁿ row count makes them impractical for formulas with many variables.

A logical fallacy is an argument whose conclusion does not actually follow from its premises, even though it may look persuasive. Formal fallacies are errors in the argument's logical structure itself — the argument would be invalid no matter what statements are substituted into its variables — and are typically named by the invalid inference pattern they mimic. The two most common formal fallacies are affirming the consequent (from P → Q and Q, wrongly concluding P) and denying the antecedent (from P → Q and ¬P, wrongly concluding ¬Q); both are easily confused with the genuinely valid rules modus ponens (P → Q, P ⊢ Q) and modus tollens (P → Q, ¬Q ⊢ ¬P). This is distinct from informal fallacies (such as ad hominem or appeal to authority), which are errors in content or context rather than structure — a formal fallacy is invalid for every substitution of its propositional variables, which is exactly why truth tables and formal proof can catch it mechanically.

Soundness and completeness are the two theorems that connect syntax (⊢, formal derivability) to semantics (⊨, truth in every model) for a given logic and proof system. Soundness states that every provable formula is semantically valid — Γ ⊢ φ implies Γ ⊨ φ — meaning the proof system never lets you derive a false conclusion from true premises; it guarantees the system doesn't 'lie.' Completeness, the converse, states that every valid formula is provable — Γ ⊨ φ implies Γ ⊢ φ — meaning the proof system is powerful enough to prove everything that is semantically true; it guarantees the system doesn't 'miss' anything. Kurt Gödel proved in his 1930 completeness theorem that standard first-order logic, with a suitable proof system (e.g. Hilbert-style or natural deduction), is both sound and complete — a foundational, positive result that should not be confused with his separate (and quite different) 1931 incompleteness theorems about arithmetic.

The compactness theorem is a cornerstone result of first-order model theory: a set of first-order sentences Σ has a model if and only if every finite subset of Σ has a model. The forward direction is trivial (a model of all of Σ is automatically a model of any finite piece of it); the substance is the converse — that satisfiability can be verified 'locally,' one finite piece at a time, and this automatically guarantees a single model exists for the entire, possibly infinite, set. It follows immediately from Gödel's completeness theorem (a set is satisfiable iff it is consistent, and any proof of a contradiction from Σ can only use finitely many sentences of Σ), though it can also be proved directly via ultraproducts. Compactness is the key tool behind many striking existence results: it shows that if a first-order theory has arbitrarily large finite models, it must have an infinite model; it produces nonstandard models of arithmetic containing 'infinite' numbers; and it underlies the construction of the hyperreal numbers in nonstandard analysis.

The Löwenheim–Skolem theorem describes how little control first-order logic has over the cardinality (size) of the models of a theory. The downward form says that if a countable first-order theory has an infinite model, it has a model of every infinite cardinality up to and including ℵ₀ (countably infinite) — in particular, it has a countable model, even if the theory was designed with an uncountable structure in mind. The upward form says that if a theory has an infinite model, it has models of every infinite cardinality larger than that model too. Together, downward and upward Löwenheim–Skolem show that no first-order theory with an infinite model can pin down a unique infinite cardinality for its models — this is the technical content behind Skolem's paradox: Zermelo–Fraenkel set theory (ZFC) proves the existence of uncountable sets, yet if ZFC is consistent it has a countable model (by downward Löwenheim–Skolem applied to ZFC itself), meaning a model that is 'from the outside' countable nonetheless satisfies, from the inside, the sentence asserting the existence of uncountable sets. This is not a contradiction — it reflects that 'countable' and 'uncountable' are relative to which bijections exist, and a countable model of ZFC may simply lack the bijection (from inside the model) that would witness its universe or some subset of it as countable, even though such a bijection exists outside the model looking in.

Model theory studies the relationship between formal first-order languages and the mathematical structures (models) that interpret them — where proof theory asks 'what can be derived syntactically,' model theory asks 'what is true in which structures.' A structure (or model) M for a language L consists of a nonempty domain (universe) together with an interpretation of each constant, function, and relation symbol of L; a sentence φ is satisfied by M, written M ⊨ φ, when φ comes out true under that interpretation. Two structures M and N are elementarily equivalent (M ≡ N) if they satisfy exactly the same first-order sentences, even if they are not isomorphic — a strictly weaker relationship than isomorphism, since (by Löwenheim–Skolem) elementarily equivalent structures can even have different cardinalities. A substructure N ⊆ M is an elementary substructure (N ≺ M) if it agrees with M not just on quantifier-free formulas but on ALL first-order formulas, including those with quantifiers ranging over the larger structure M — a much stronger condition than merely being a substructure, since a plain substructure can satisfy an existential sentence 'accidentally' using elements outside N, without N itself containing the required witness.

Model theory studies the relationship between formal languages and their interpretations (models). It asks: which mathematical structures satisfy a given set of sentences? Key results include the completeness theorem, compactness, Löwenheim–Skolem, and the powerful tools of types and saturation used in algebra and geometry.

Predicate logic (also called first-order logic, predicate calculus, or quantificational logic) is a formal system used across mathematics, philosophy, linguistics, and computer science. Unlike propositional logic, which treats statements like 'all humans are mortal' as indivisible units, predicate logic looks inside them: it introduces variables, predicates, and quantifiers, so the same statement becomes 'for all x, if x is a human, then x is mortal' — where 'for all x' is a quantifier, x is a variable, and 'is a human' / 'is mortal' are predicates. This extra structure makes predicate logic strictly more expressive than propositional logic, while still building on its connectives.

A mathematical proof is a deductive argument for a mathematical statement, showing that the stated assumptions logically guarantee the conclusion. The argument may use other previously established statements, such as theorems, but every proof can, in principle, be constructed using only certain basic or original assumptions known as axioms, along with the accepted rules of inference. Proofs are examples of exhaustive deductive reasoning that establish logical certainty, to be distinguished from empirical arguments or non-exhaustive inductive reasoning that establish 'reasonable expectation.' Presenting many cases in which a statement holds is not enough for a proof, which must demonstrate that the statement is true in all possible cases. A proposition that has not been proved but is believed to be true is known as a conjecture, or a hypothesis if frequently used as an assumption for further mathematical work.

A quantifier specifies how many members of a domain satisfy a given property, turning an open statement with a free variable ('x is even') into a statement with a definite truth value ('for all x, x is even' — false; 'there exists an x that is even' — true). The two quantifiers of first-order logic, universal (∀) and existential (∃), are the backbone of how mathematics states general laws and existence claims precisely.

Descriptive set theory studies the complexity of subsets of Polish spaces (complete separable metric spaces), classifying them through the Borel and projective hierarchies. It connects logic, topology, and measure theory, and has deep interactions with determinacy axioms, large cardinals, and effective computability.

Forcing is Paul Cohen's revolutionary technique (1963) for constructing models of set theory in which specific statements — notably the Continuum Hypothesis and the Axiom of Choice — have chosen truth values. It established that the Continuum Hypothesis is independent of ZFC, completing Gödel's earlier consistency result.