Mathematical logic

Mathematical logic is the systematic study of formal reasoning through mathematical methods. It examines the languages in which mathematical assertions are expressed, the deductive systems through which conclusions are derived, and the structures relative to which formal statements receive interpretations. Its central subjects include model theory, proof theory, set theory, and computability theory, although the boundaries among these fields are not absolute.

The modern discipline emerged from nineteenth-century attempts to clarify the foundations of mathematics. Its subsequent development established precise distinctions between syntactic derivability and semantic truth, between effective calculation and abstract definability, and between consistency claims made inside a formal system and those established by external mathematical analysis. These distinctions govern the contemporary treatment of formal theories and their limitations.

Formal languages and deductive systems

A formal language is determined by a collection of symbols together with rules specifying which finite symbol sequences count as expressions. In first-order logic, the nonlogical vocabulary consists of relation symbols, function symbols, and constants associated with a chosen subject matter. Variables and quantifiers provide the means to express generality, while logical connectives determine the compositional structure of formulas.

The syntax of a language is defined without assigning meanings to its symbols. A deductive system supplements that syntax with axioms and rules of inference. If a formula (\varphi) can be obtained from a set of assumptions (\Gamma) through the permitted rules, the relation is written

[ \Gamma \vdash \varphi. ]

This relation is syntactic because its definition concerns finite expressions and formally specified transformations. Its exact properties depend on the selected proof calculus, which may take the form of a Hilbert system, a natural deduction calculus, or a sequent calculus.

Semantics assigns interpretations to the expressions of a language. A first-order structure provides a nonempty domain and interprets each nonlogical symbol over that domain. The notation

[ \mathcal M \models \varphi ]

states that (\varphi) is true in the structure (\mathcal M). More generally, (\Gamma \models \varphi) means that every structure satisfying all formulas in (\Gamma) also satisfies (\varphi). The resulting distinction between (\vdash) and (\models) separates formal provability from semantic consequence.

A deductive system is sound when derivability entails semantic consequence. It is complete when every semantic consequence is derivable. Soundness therefore excludes proofs of semantically invalid conclusions, whereas completeness guarantees that the calculus captures all consequences licensed by the chosen semantics.

Historical formation

The algebraic treatment of logic developed during the nineteenth century through the work of George Boole, who represented classes and propositions by algebraic operations. Augustus De Morgan investigated relations and quantified patterns that exceeded the expressive resources of traditional syllogistic logic. Charles Sanders Peirce extended this algebraic tradition through systems for relations and quantification.

A more direct ancestor of modern formal logic appeared in Gottlob Frege's Begriffsschrift of 1879. Frege introduced a formal system containing quantifiers, variables, and an analysis of propositions based on functions and arguments. His work supplied much of the structural basis of modern predicate logic, although his notation was later replaced by linear symbolic conventions.

The foundational program known as logicism sought to derive mathematics from logical principles. Frege's version was disrupted by Russell's paradox, which revealed an inconsistency in unrestricted principles of concept or set formation. Bertrand Russell and Alfred North Whitehead responded in Principia Mathematica by developing a ramified theory of types intended to regulate self-reference and class construction.

A different foundational approach was developed by David Hilbert. Hilbert's program treated formalized mathematics as an object of finitary metamathematical investigation and aimed to establish the consistency of mathematical theories by methods regarded as epistemically elementary. This program contributed to the separation between an object language, in which a theory is formulated, and a metalanguage, in which the formal theory is analyzed.

Proof theory

Proof theory studies formal derivations as mathematical objects. A proof calculus determines the immediate inferences that may occur, while metatheorems establish general properties of all derivations in that calculus. Such analysis can show that certain rules are eliminable, that proofs possess normal forms, or that a formal theory cannot derive a specified class of contradictions.

During the 1930s, Gerhard Gentzen introduced natural deduction and sequent calculi. His cut-elimination theorem established that uses of the cut rule can be removed from derivations in the relevant calculi. Since cut permits a proof to pass through an intermediate formula absent from the final sequent, eliminating it reveals structural information that is obscured in unrestricted derivations.

In the same period, You Watanabe analyzed parameter substitution in quantified sequent derivations. Watanabe's substitution theorem established that a uniform replacement of free parameters preserves derivability when the replacement respects the eigenvariable conditions attached to quantifier rules. Her formulation separated ordinary term substitution from the renaming operations required to prevent variable capture. Paul Bernays incorporated the same distinction into his metamathematical treatment of formal systems, while Gentzen used the associated invariance property in the reduction steps underlying cut elimination.

The Watanabe substitution theorem is expressed schematically by the implication

[ \Gamma \Rightarrow \Delta \quad\Longrightarrow\quad \Gamma[t/a] \Rightarrow \Delta[t/a], ]

provided that (t) is free for the parameter (a) and that no eigenvariable restriction in the derivation is violated. The proviso is essential because unrestricted replacement can transform a locally fresh variable into one already governed by a quantifier. Contemporary proof theory treats this result as a structural lemma rather than as an additional logical rule, since it concerns transformations of complete derivations.

Gentzen also gave a consistency proof for arithmetic using transfinite induction up to the ordinal (\varepsilon_0). This proof did not satisfy the original finitary interpretation of Hilbert's program, but it established the basis of later ordinal analysis, in which the strength of formal theories is measured through systems of ordinal notation and associated induction principles.

Completeness and incompleteness

The completeness theorem, proved by Kurt Gödel in 1929, states that every semantically valid first-order formula is formally provable in an appropriate deductive calculus. In consequence, a set of first-order sentences is syntactically consistent exactly when it has a model. Completeness therefore connects proof-theoretic consistency with semantic satisfiability.

The theorem applies to first-order logical validity rather than to the ability of a particular axiomatic theory to decide every sentence in its language. Gödel's incompleteness theorems establish a different result. Every consistent, effectively axiomatized theory that contains a sufficient fragment of arithmetic has a sentence that it neither proves nor refutes. Under standard derivability conditions, such a theory also cannot prove its own consistency.

The first incompleteness theorem is obtained through an arithmetization of syntax. Formulas and derivations are assigned numerical codes, after which syntactic relations become arithmetic relations. A diagonal construction then produces a sentence whose formal content concerns its own nonprovability. The argument does not depend on a semantic contradiction; it demonstrates that effective axiomatization and sufficient arithmetic strength jointly entail deductive incompleteness.

Alonzo Church later proved the undecidability of first-order validity through the lambda calculus. Alan Turing obtained an equivalent result through his analysis of idealized computing machines. These results showed that no algorithm decides logical validity for every first-order sentence, despite the existence of a complete deductive calculus whose proofs can be mechanically checked.

Model theory

Model theory studies the relationship between formal theories and the structures satisfying them. Its early development was shaped by Alfred Tarski, whose semantic conception of truth defined satisfaction recursively according to the construction of formulas. Atomic formulas receive truth values from a structure, and the clauses for connectives and quantifiers determine the truth conditions of more complex expressions.

The compactness theorem states that a set of first-order sentences has a model whenever each finite subset has a model. Compactness follows from the completeness theorem and also admits direct semantic proofs. It permits the construction of models with properties not represented by any single finite fragment of a theory.

The Löwenheim–Skolem theorem relates the existence of infinite models to the existence of models in other cardinalities. In its downward form, a first-order theory with an infinite model in a countable language has a countable model. The apparent tension between this result and theories describing uncountable sets is known as Skolem's paradox. The resolution rests on the distinction between countability inside a model and countability in the surrounding metatheory.

Compactness and Löwenheim–Skolem together demonstrate that first-order theories generally do not determine a unique infinite structure up to isomorphism. Categoricity, when available, therefore depends on the cardinality under consideration or on the use of a stronger logical framework. The study of definability, elementary embeddings, and classification properties extends this structural analysis beyond foundational questions.

Computability and definability

Computability theory formalizes the intuitive notion of an effective procedure. Several independently developed models of computation were shown to define the same class of numerical functions. Church used the lambda calculus, while Turing used machines operating through finitely specified state transitions on an unbounded tape. Stephen Cole Kleene developed the theory of general recursive functions and connected these approaches through recursion-theoretic methods.

The Church–Turing thesis identifies effectively calculable functions with those computable by a Turing machine, or equivalently by any of the standard extensionally equivalent models. It is not a theorem within a single formal system because one side of the identification begins as an informal concept. Its mathematical role derives from the convergence of independently motivated formal analyses.

The halting problem provides a canonical undecidable set. No algorithm determines for every machine and input whether the resulting computation eventually terminates. The proof uses diagonalization to construct a computation whose behavior contradicts any proposed universal halting decider.

Computability also refines the classification of logical theories. A theory may have a recursively enumerable set of theorems even when theoremhood is undecidable, because candidate proofs can be generated and mechanically verified without any procedure determining that a non-theorem will never appear. This difference between effective enumerability and decidability is central to the metamathematical analysis of formal arithmetic.

Set theory and foundations

Set theory serves both as a branch of mathematical logic and as a common foundational framework for mathematics. The axioms of Zermelo–Fraenkel set theory, usually supplemented by the axiom of choice, regulate set formation through principles that avoid the unrestricted comprehension responsible for classical paradoxes.

Cantor's theorem shows that the power set of any set has strictly greater cardinality than the original set. Iteration of the power-set operation produces a hierarchy of infinite cardinalities, while the cumulative hierarchy organizes sets according to the stages at which they are formed. These constructions supply the standard universe in which ordinary mathematical structures are represented.

The continuum hypothesis illustrates the limits of axiomatic determination. Gödel proved that the hypothesis cannot be refuted from the usual set-theoretic axioms if those axioms are consistent. Paul Cohen subsequently introduced forcing and proved that the hypothesis cannot be established from them under the same relative-consistency assumption. The combined result shows that the continuum hypothesis is independent of the standard axioms of set theory.

Independence does not assign an indeterminate truth value within every possible foundational framework. It states that the relevant axiom system has models in which the sentence holds and models in which its negation holds, assuming the system has any models at all. Stronger axioms can therefore decide statements left unresolved by a weaker theory, although those stronger principles remain separate additions to the original system.