Foundational Questions
Logic is one of the oldest intellectual disciplines and one of the most technically demanding. A logician studies the formal principles of valid reasoning — but what does that mean in practice?
Summary
A logician studies the formal principles of valid reasoning. This includes developing mathematical theories of proof and inference, investigating the foundations of mathematics and language, and applying formal methods to computation, artificial intelligence, and philosophy. Logicians prove theorems about what can and cannot be derived within a formal system, construct and analyse proof systems, study the relationship between syntax and semantics, and explore the limits of formal reasoning. The discipline sits at the intersection of mathematics, philosophy, and computer science.
Logic is the study of valid inference: when does a conclusion follow necessarily from given premises, and why? The question sounds simple but its formal development is one of the most technically demanding areas of mathematics.
A formal logic consists of: a language for expressing statements precisely; axioms or inference rules specifying which transitions between statements are valid; and often a semantics specifying what the statements mean — usually in terms of mathematical structures called models.
Logic as a formal discipline emerged in the nineteenth century from the work of Boole, Frege, and Peano, and reached its classical form in the twentieth century through Gödel, Tarski, Turing, and Gentzen. Today it encompasses a wide range of specialisms: proof theory, model theory, set theory, computability theory, philosophical logic, and their many intersections with computer science and AI.
The mathematical study of formal proofs: their structure, transformations, and properties. Proof theorists construct proof systems such as natural deduction and sequent calculus, prove normalisation and cut-elimination theorems, study proof complexity, and investigate the relationship between proof and meaning. Proof theory includes proof-theoretic semantics, which identifies meaning with inferential role.
The study of the relationship between formal languages and mathematical structures. Model theorists investigate when a set of sentences has a model (a structure in which all the sentences are true), how many models a theory can have, and what properties of structures can be expressed in a given language. Key results include the compactness theorem and the Löwenheim–Skolem theorem.
The study of mathematical collections and their properties, traditionally taken to provide the foundations of all mathematics. Set theorists investigate axiom systems such as ZFC, the independence of statements from axioms (notably Cantor’s continuum hypothesis), large cardinal axioms, and the structure of the set-theoretic universe.
The study of what can and cannot be computed or decided algorithmically, and at what cost. Originating in Gödel’s incompleteness theorems and Turing’s analysis of computation, this area addresses the limits of formal systems and algorithms: which problems are decidable, which are not, and how efficiently decidable problems can be solved.
The application of formal methods to questions in philosophy: the logic of necessity and possibility (modal logic), of obligation and permission (deontic logic), of time (temporal logic), of knowledge and belief (epistemic logic), and of meaning itself. Philosophical logic connects the technical apparatus of mathematical logic with substantive philosophical questions.
Logic sits across several disciplines, and logicians are found in correspondingly diverse settings.
Mathematics departments are the traditional home of mathematical logic. Logicians here work on foundational questions in set theory, model theory, and computability, often with close connections to algebra, topology, and combinatorics.
Philosophy departments host philosophical logicians working on modal, epistemic, deontic, and other applied logics, as well as the philosophy of mathematics and the theory of meaning. The interface between proof-theoretic semantics and the philosophy of language is primarily a philosophical concern.
Computer science departments employ logicians working on programming language theory, type theory, formal verification, database theory, and automated reasoning. The Curry–Howard correspondence — which identifies proofs with programs and propositions with types — is among the most productive intellectual connections in twentieth-century logic.
AI research groups and industry increasingly employ logicians to work on knowledge representation, formal verification of AI systems, neuro-symbolic reasoning, and the logical foundations of explainability.
A logician’s primary tool is formal proof. Arguments are written out in full, with every step explicitly licensed by an inference rule, so that the reasoning can be checked and verified. This is distinct from informal mathematical argument, where steps are sometimes justified by appeals to intuition or omitted as “obvious.”
Key formal systems include natural deduction, which models reasoning by introducing and discharging assumptions; sequent calculus, which represents proofs as transformations on pairs of sets of formulas; and type theory, which represents proofs as programs and provides the basis for modern proof assistants such as Lean, Coq, and Agda.
Logicians also use semantic methods: constructing models to demonstrate that a statement is consistent, or showing that no model satisfies a given set of sentences to establish a contradiction. The interplay between proof-theoretic and model-theoretic methods — completeness theorems, which establish that what is provable coincides with what is true in all models — is among the deepest results in the field.
Increasingly, logicians use proof assistants: software systems that check formal proofs for correctness. The formalisation of classical mathematical results in proof assistants such as Lean has become a major research programme, connecting logic with computer science in a new way.
Common Questions
Logic is not the same as mathematics, but they are deeply intertwined. Logic was originally hoped to provide the foundations of all mathematics — Russell and Whitehead’s Principia Mathematica attempted to derive all of mathematics from logical axioms. Gödel’s incompleteness theorems showed this programme faces fundamental limits. Today, logic is a branch of mathematics (mathematical logic) and also a philosophical discipline (philosophical logic), and its results are used throughout both mathematics and computer science.
They overlap but are not the same. Critical thinking is a broad intellectual skill concerned with evaluating arguments, identifying assumptions, and resisting fallacies. Logic, as a formal discipline, is the mathematical study of valid inference: it specifies precisely when conclusions follow necessarily from premises, and proves theorems about formal systems. Critical thinking draws on logical concepts but is not confined to formal systems.
Most logicians come from mathematics, philosophy, or computer science backgrounds. Undergraduate study in any of these disciplines provides relevant foundations. Advanced training typically involves postgraduate study — an MSc followed by a PhD — specialising in mathematical logic, proof theory, or philosophical logic. The field is small but internationally connected; doctoral supervision and research community are important in finding a path through it.
Gödel’s completeness theorem (1929): every valid first-order sentence has a proof. Gödel’s incompleteness theorems (1931): any consistent formal system strong enough to express arithmetic contains true statements it cannot prove. Turing’s halting problem (1936): there is no algorithm that correctly decides whether an arbitrary program terminates. Gentzen’s cut-elimination theorem (1934): every proof in sequent calculus can be transformed into a direct proof without shortcuts. Cohen’s forcing (1963): the continuum hypothesis is independent of the standard axioms of set theory.
From This Site
For an explanation of proof-theoretic semantics — one of the central research programmes in contemporary proof theory — see What is proof-theoretic semantics?
For the relationship between logic and AI, see How does logic relate to AI?
Gheorghiu is currently accepting PhD students in logic and related areas. Enquiries are welcome via the Contact page.