Loading field map
Formal logic is the branch of logic that studies correct reasoning by constructing precise artificial languages, defining the conditions under which a conclusion follows necessarily from premises, and investigating the properties of those systems. Its central concern is not whether a claim is true in fact, but whether a conclusion is guaranteed by the premises that support it—that is, whether the inference is valid. To make this question tractable, formal logic replaces the messy ambiguities of natural language with symbols and rules, so that validity can be checked by the form of an argument rather than its content.
Everyday reasoning is full of inferences that seem compelling but are hard to evaluate precisely. Consider: "If it rains, the ground is wet. The ground is wet. Therefore it rained." Most people recognize this as a mistake, but explaining exactly why requires a standard of correctness. Formal logic supplies that standard by abstracting away from what "rain" and "ground" mean and focusing on the skeleton: "If P then Q. Q. Therefore P." Once the argument is expressed in this form, it becomes clear that the conclusion does not follow, because there could be other reasons for Q to be true.
The deeper problem is that natural language is not built for perfect precision. Words shift meaning with context, sentences have grammatical structure that obscures logical structure, and quantifiers like "all" or "some" behave in subtle ways. Formal logic responds by inventing languages with explicit syntax—rules for forming well-formed expressions—and explicit semantics—rules for what those expressions mean. In such a language, the question "Does this conclusion follow from those premises?" becomes a question that can be answered by calculation or proof, not by intuition or debate.
This project has two faces. On one side, formal logic is descriptive: it aims to capture the valid patterns that good reasoning already uses. On the other side, it is normative: it tells us which patterns we ought to accept, and it can reveal that some patterns we instinctively trust are actually invalid. The tension between these two aims runs through the entire history of the field.
The foundation of formal logic is propositional logic, also called sentential logic. It treats whole declarative sentences—propositions—as indivisible units, represented by letters like P and Q. These units are combined by connectives: "not" ($\neg $), "and" ($\land $), "or" ($\lor $), "if...then" ($\rightarrow $), and "if and only if" ($\leftrightarrow $). The meaning of each connective is fixed by a truth table, which specifies the truth value of a compound sentence for every possible assignment of truth values to its parts. Validity in propositional logic is truth-functional: an argument is valid if there is no assignment of truth values to the sentence letters that makes all premises true and the conclusion false.
Propositional logic is powerful enough to capture many patterns of reasoning, but it cannot see inside propositions. It cannot express the fact that "All humans are mortal" and "Socrates is human" together force "Socrates is mortal," because the internal structure of these sentences is invisible to it. Predicate logic, also called first-order logic, adds this expressive power. It introduces terms for objects (like "Socrates"), predicates for properties and relations (like "is human" or "is taller than"), and quantifiers: "for all" ($\forall $) and "there exists" ($\exists $). With these tools, the Socrates argument becomes: $\forall $x(Human(x) $\rightarrow $ Mortal(x)), Human(Socrates) ⊢ Mortal(Socrates). The validity of this inference is no longer a matter of truth tables but of a richer semantics, usually given by models—mathematical structures that specify what objects exist and which predicates apply to them.
First-order logic is often described as the canonical formal logic. It has a well-understood proof theory (systems of rules for deriving conclusions from premises), a well-understood model theory (the study of structures that satisfy sentences), and a famous pair of results about its limits. The completeness theorem, proved by Kurt Gödel in 1930, shows that every valid inference in first-order logic can be proved by a suitable proof system—the proof rules are strong enough to capture all logical consequence. The compactness theorem, a corollary, says that if every finite subset of a set of sentences has a model, then the whole set has a model. But Gödel's incompleteness theorems, proved shortly afterward, show that first-order logic cannot capture all truths of arithmetic: any consistent formal system strong enough to express basic arithmetic contains sentences that are true but unprovable within the system. These results mark the boundary of what formal methods can achieve and remain central to the field's self-understanding.
Formal logic has two deep historical roots. The first is the Aristotelian syllogistic, developed in ancient Greece. Aristotle analyzed arguments into premises and conclusions involving terms like "All S are P" or "Some S are not P," and classified the valid patterns among them. This system dominated logical teaching for over two thousand years, but it was limited: it could not handle relational reasoning, compound propositions, or arguments with more than two premises in a natural way.
The second root is the Stoic tradition, which studied propositional connectives and inference patterns involving them. The Stoics recognized that arguments like "If P then Q; P; therefore Q" are valid by their form, independent of content. But their work was largely lost or overshadowed, and it did not develop into a general formal system.
The modern field emerged in the late nineteenth century, primarily through the work of Gottlob Frege, who invented a notation for quantifiers and predicates that could express far more than Aristotelian logic. Frege's goal was to show that arithmetic could be reduced to logic, a project called logicism. Bertrand Russell and Alfred North Whitehead continued this project in their monumental Principia Mathematica, attempting to derive all of mathematics from logical axioms. The project encountered difficulties—most famously Russell's paradox, which showed that naive set theory, a natural companion to logic, is inconsistent—but it established the agenda of formal logic as the study of a universal language for reasoning.
In the twentieth century, formal logic split into several specialized subfields. Proof theory, founded by David Hilbert and developed by Gerhard Gentzen, studies formal proofs as mathematical objects. Model theory, pioneered by Alfred Tarski, studies the relationship between formal languages and the structures that interpret them. Recursion theory, also called computability theory, studies what can be computed by algorithms and what cannot, growing out of work by Alonzo Church, Alan Turing, and others. Set theory, which provides the mathematical universe in which models live, became a field in its own right. These subfields are distinct but deeply interconnected: model theory uses set theory, proof theory informs our understanding of consistency, and recursion theory sets limits on what formal systems can decide.
Within formal logic, several approaches coexist, each addressing a different aspect of the central problem of validity.
Proof-theoretic approaches define validity in terms of derivation: a conclusion follows from premises if there is a finite sequence of rule-governed steps leading from the premises to the conclusion. The rules are chosen to be obviously sound—each step preserves truth—and the hope is that they are also complete, capturing every valid inference. Natural deduction, introduced by Gentzen, presents rules that mirror ordinary reasoning: to prove "P and Q," prove P and prove Q; to prove "P implies Q," assume P and derive Q. Sequent calculus, also due to Gentzen, is a more abstract formulation that makes the structure of proofs explicit and is particularly useful for proving properties of proof systems. Proof theory is the approach that most directly answers the question "How can we be certain that a conclusion follows?" by exhibiting a certificate—the proof—that can be checked step by step.
Model-theoretic approaches define validity semantically: a conclusion follows from premises if every model that makes the premises true also makes the conclusion true. This definition, due to Tarski, is elegant and powerful. It connects logic to mathematics by treating sentences as descriptions of structures, and it enables powerful results about what can and cannot be expressed in a given language. The completeness theorem is the bridge between the two approaches: it says that the proof-theoretic and model-theoretic definitions of validity coincide for first-order logic. This is not a trivial fact; it is a deep result that took decades to prove, and it fails for some stronger logics.
Algebraic approaches treat logical connectives as operations on algebraic structures. Boolean algebra, which models propositional logic, is the simplest example: the connectives correspond to operations on a set with two elements, true and false. More sophisticated algebraic semantics, such as Heyting algebras for intuitionistic logic, reveal that different logics correspond to different algebraic structures. This approach is valuable because it brings the tools of algebra to bear on logic, and it clarifies the relationships between logical systems.
Proof-theoretic and model-theoretic approaches are not rivals in the sense of competing for the same job. They answer different questions and complement each other. Proof theory tells us how to construct and verify arguments; model theory tells us what arguments are about. The completeness theorem shows that, for first-order logic, the two perspectives agree. For other logics—second-order logic, modal logic, intuitionistic logic—they may diverge, and the study of these divergences is itself a rich area of research.
First-order logic is not the only formal logic, and much of the field's vitality comes from logics that extend or modify it.
Modal logic adds operators for necessity and possibility, usually written □ ("necessarily") and ◇ ("possibly"). It was originally developed to analyze philosophical notions like necessity and obligation, but it has found applications in computer science, where □ can mean "in all reachable states" and ◇ "in some reachable state." Modal logic is studied semantically through possible-worlds models, which are structures with a set of worlds and an accessibility relation between them. Different conditions on the accessibility relation correspond to different modal systems, and the field has developed a rich correspondence theory linking modal axioms to properties of relations.
Intuitionistic logic rejects the law of excluded middle—the principle that every proposition is either true or false—and the rule of double negation elimination. It arises from the constructive view that to prove a statement is to provide a construction or method for finding what it asserts. This logic is not merely a philosophical curiosity; it is the logic underlying many programming languages and proof assistants, because proofs in intuitionistic logic correspond to programs. The relationship between classical and intuitionistic logic is subtle: classical logic can be interpreted within intuitionistic logic via double-negation translations, and intuitionistic logic can be understood semantically through Kripke models or topological models.
Higher-order logic allows quantification over predicates and functions, not just objects. It is more expressive than first-order logic, but it lacks the nice meta-theoretic properties: there is no complete proof system, and the compactness theorem fails. This makes it less well-behaved but sometimes more natural for expressing mathematical statements. Type theory, which organizes expressions into types and allows functions between types, is a related framework that has become important in computer science and the foundations of mathematics.
Substructural logics relax or modify the structural rules of classical logic—the rules that say premises can be used any number of times, in any order, and that irrelevant premises can be ignored. Relevance logic requires that premises actually be used in deriving a conclusion; linear logic treats premises as resources that are consumed; non-monotonic logic allows conclusions to be withdrawn when new information arrives. These logics are motivated by different applications, from natural language processing to resource-aware computation, and they show that the classical framework is one choice among many rather than the only possible logic.
Formal logic today is not a single unified discipline but a family of interconnected research programs. In philosophy, it remains the tool for analyzing arguments and the subject of foundational inquiry: philosophers study the nature of logical consequence, the relationship between logic and mathematics, and the semantics of natural language using formal methods. In mathematics, model theory and set theory are active fields with deep connections to algebra and geometry. In computer science, logic is everywhere: automated theorem proving, program verification, database query languages, and the theory of computation all rely on formal logic. The Curry–Howard correspondence, which identifies proofs with programs and formulas with types, has created a productive bridge between logic and programming language theory.
The field is also marked by ongoing debates about its foundations. Is classical logic the correct logic, or should we adopt intuitionistic or paraconsistent logic? What is the right account of logical consequence—proof-theoretic, model-theoretic, or something else? Is logic a description of how we actually reason, a normative standard for how we should reason, or a purely formal discipline with no psychological content? These questions are not settled, and they are unlikely to be settled by formal results alone, because they concern the interpretation and purpose of formal systems rather than their internal properties.
What remains durable is the core insight that made formal logic possible: reasoning can be studied by constructing artificial languages in which validity is a matter of form, and those languages can be investigated with mathematical precision. The specific systems change, the applications multiply, and the philosophical interpretations shift, but the project of making reasoning exact through formalization continues to define the field.