Mathematical logic is the branch of mathematics that studies formal reasoning itself — making completely precise what counts as a valid step of inference, what a mathematical statement actually means, and what can (and, crucially, cannot) ever be proven. Developed substantially in response to 19th-century foundational anxieties, it gave rise to Gödel's landmark incompleteness results, the entire theory of computability, and the conceptual bedrock underlying every modern computer.
In everyday speech, words like "and," "or," "not," and "if...then" carry some looseness and ambiguity — context does a lot of work. Mathematical logic strips all of that ambiguity away, defining exactly, with total mathematical precision, what each of these logical connectives means, and exactly which chains of reasoning built from them are genuinely, unbreakably valid.
Logic as a subject of study is ancient — Aristotle's systematic treatment of syllogisms (c. 350 BCE) is often considered the starting point of Western formal logic. But mathematical logic — logic expressed using precise mathematical symbols and studied with the same rigour as any other branch of mathematics — is a much more recent development, emerging substantially in the late 19th and early 20th centuries through the work of Gottlob Frege, Giuseppe Peano, Bertrand Russell, and others.
Every computer program ultimately runs on circuits implementing basic logical operations (AND, OR, NOT gates) — mathematical logic, in a very direct sense, is the theoretical foundation underlying all of modern computing. Database search queries, spell-checkers verifying grammatical rules, and even the basic design of digital circuits all rest, at some level, on ideas first made rigorous within mathematical logic.
Propositional logic studies how simple statements ("it is raining," "the ground is wet") combine via connectives (AND, OR, NOT, IMPLIES) into more complex statements, and which combinations are always true regardless of the truth of the individual parts (tautologies). Predicate logic (also called first-order logic) extends this considerably, adding quantifiers — "for all x" (∀) and "there exists an x" (∃) — allowing genuinely rich mathematical statements like "every even number greater than 2 is a sum of two primes" (see the Goldbach Conjecture entry) to be expressed with full logical precision.
Proof theory studies mathematical proofs themselves as formal, mathematical objects in their own right — asking questions like which statements are provable within a given formal system, how long a shortest proof of a given statement must be, and how different proof systems relate to and can be translated into one another (see the Proof entry for the broader concept of proof itself).
Model theory studies the relationship between formal logical languages and the mathematical structures ("models") that make the statements in those languages true or false. A single set of axioms can have many different, genuinely non-isomorphic models — a striking and initially surprising fact model theory studies systematically, with significant applications in algebra, number theory, and beyond.
Set theory, covered substantially in the ZFC Axioms and Continuum Hypothesis entries, studies sets and their properties as a foundation for essentially all other mathematics, and is generally considered a core branch of mathematical logic in its own right, alongside the three above.
Computability theory (also called recursion theory) studies which mathematical problems can, even in principle, be solved by a mechanical, step-by-step procedure (an algorithm) — and, crucially, which cannot, no matter how cleverly designed the procedure. Alan Turing's foundational 1936 work defining the "Turing machine" (an idealised, maximally general model of mechanical computation) belongs to this branch, and directly established the theoretical limits of what any computer, however powerful, could ever compute.
David Hilbert posed the Entscheidungsproblem ("decision problem," 1928): does there exist a general mechanical procedure that could determine, for any given mathematical statement expressed in first-order logic, whether that statement is provable? Alonzo Church (1936) and, independently and almost simultaneously, Alan Turing (1936) both proved the answer is no — no such general procedure can possibly exist. Turing's proof, notably, proceeded by first rigorously defining a precise mathematical notion of "mechanical computation" (the Turing machine) — a definition that turned out to be enormously more consequential and influential than the specific negative result it was originally introduced to help establish.
Turing's approach yielded a closely related and even more striking result: the halting problem — given an arbitrary computer program and its input, determine whether that program will eventually stop running or continue running forever — is itself provably undecidable: no general algorithm can solve it correctly for every possible program and input. This landmark result, established using a clever self-referential argument closely related in spirit to Gödel's own incompleteness proof (see that entry) and to Cantor's diagonal argument (see the Continuum Hypothesis entry), established a fundamental, permanent limitation on what any computer could ever be programmed to determine about other computer programs in full generality.
The Church-Turing thesis proposes that Turing machines (and several other independently-developed, later mathematically proven exactly equivalent formal models of computation, including Church's lambda calculus and Gödel's own recursive functions) capture the complete, correct, maximally general notion of "mechanical computability" — that any procedure any reasonable person would agree counts as an "algorithm" can be carried out by some Turing machine. This is not itself a mathematical theorem capable of formal proof (since "any reasonable notion of algorithm" is inherently an informal, intuitive notion, not a precise mathematical one), but rather a foundational thesis about the correct scope of computability theory, essentially universally accepted by logicians and computer scientists alike.
The theoretical foundations of modern computer science trace directly back to mathematical logic: Turing machines directly inspired the architecture of real, physically constructed computers; formal logical languages underlie modern programming language design and formal software verification; and complexity theory (see the Big-O Notation and P vs NP entries) emerged as a natural refinement of computability theory, asking not just whether a problem can be solved by some algorithm at all, but how efficiently it can be solved. Alan Turing is consequently regarded as both a foundational figure in pure mathematical logic and, simultaneously, the father of theoretical computer science — one of relatively few individuals whose work is considered absolutely foundational to two entire, enormously significant academic disciplines at once.