Loading field map
Formal logic studies the patterns that make deductive arguments valid. Its central tension has always been whether natural language can be regimented into an artificial language precise enough to capture all and only the inferences that deserve the label 'logical'. Different frameworks have answered this question by proposing different logical vocabularies, different accounts of logical form, and different standards of what counts as a proof or a model. The history of formal logic is the history of these competing proposals and the relationships among them.
The first systematic framework, Aristotelian Syllogistic (c. 350 BCE–1600 CE), analyzed inference in terms of the relations between general terms. A syllogism such as 'All humans are mortal; all Greeks are human; therefore all Greeks are mortal' was taken to exhibit the fundamental pattern of deduction. The framework classified valid forms (Barbara, Celarent, etc.) and treated the subject–predicate structure of sentences as the carrier of logical form. Its great strength was its intuitive match with ordinary reasoning; its limitation was that it could not handle inferences turning on propositional connectives such as 'if' and 'not', nor could it express relations or multiple quantifiers.
A rival ancient framework, Stoic Propositional Logic (c. 300–200 BCE), focused on the logical relations among whole propositions rather than terms. The Stoics identified five basic indemonstrable argument forms built from connectives such as 'if', 'and', and 'or'. Their system was a genuine propositional logic, but it was largely lost after the fall of the Roman Empire and did not directly influence the medieval tradition. It would be rediscovered only in the late nineteenth century, when it became clear that a propositional layer is indispensable for any complete formal system.
Medieval Terminist Logic (1100–1500 CE) inherited the Aristotelian framework but expanded it considerably. Medieval logicians developed theories of supposition (what a term stands for in a given context) and theories of consequence (valid inference patterns). They analyzed the logical behaviour of syncategorematic words such as 'every', 'some', 'not', and 'if', and they distinguished between formal and material consequence. This framework preserved the term-based orientation of Aristotle while adding a sophisticated treatment of propositional structure. It remained tied to natural language, however, and did not produce a fully symbolic calculus.
Algebra of Logic (1847–1913) broke decisively with the natural-language tradition. George Boole and his successors (De Morgan, Peirce, Schröder) treated logic as an algebraic system in which classes and propositions are represented by symbols and operations such as addition, multiplication, and negation. The framework showed that many deductive patterns could be calculated mechanically. Its limitation was that it could not handle multiple generality—inferences involving nested quantifiers such as 'Every number has a successor'. The algebraic notation had no way to represent the scope of quantifiers independently.
Logicism (1879–1931) addressed this limitation head-on. Gottlob Frege invented a quantifier–variable notation that could represent the scope of quantifiers unambiguously, solving the multiple-generality problem that had stumped the algebraic tradition. Frege's system also included a theory of functions and objects, and he attempted to derive arithmetic from purely logical axioms. The logicist program collapsed after Gödel's incompleteness theorems (1931) showed that no consistent formal system can capture all truths of arithmetic. What survived was Frege's formal language itself, which became the basis for Classical Predicate Logic (1879–present).
Classical predicate logic (often called first-order logic) is the dominant framework of modern formal logic. It combines propositional connectives with quantifiers (∀, ∃) that range over individuals, and it treats predicates as functions from individuals to truth values. Its metatheoretic properties are well understood: it is complete (every valid formula is provable) and compact, but it is undecidable (there is no algorithm that always determines validity). Classical predicate logic is the infrastructure on which most other frameworks build. It is not a replacement for the algebraic tradition so much as an absorption of its insights into a more expressive notation.
Type Theory (1903–present) arose from a crisis within logicism. Bertrand Russell discovered that Frege's system allowed the paradox of the set of all sets that are not members of themselves. Russell's response was to stratify objects into types: individuals, sets of individuals, sets of sets of individuals, and so on. The ramified theory of types further restricted quantification to avoid impredicative definitions. Type theory coexists with classical predicate logic as an alternative foundation for mathematics. It has been transformed by the discovery of the Curry–Howard correspondence, which links types to propositions and programs to proofs, giving it a central role in computer science and constructive mathematics.
Truth-Functional Propositional Logic (1921–present) systematized the propositional layer that the Stoics had pioneered. In this framework, the truth value of a compound sentence is determined entirely by the truth values of its parts, as shown by truth tables. The framework is decidable and complete, and it serves as the propositional fragment of classical predicate logic. It revived the Stoic insight that propositional connectives are the primary logical constants, but it did so within a fully formalized, truth-functional setting.
Modal Logic (1918–present) extended classical logic with operators for necessity (□) and possibility (◇). C. I. Lewis developed the first axiomatic systems (S1–S5) to capture different notions of necessity. For decades modal logic remained a syntactic curiosity because no one had a clear semantics for the modal operators. That changed with Possible World Semantics (1959–present), which interprets □p as 'p is true in all accessible possible worlds'. This framework transformed modal logic from a marginal system into a rich field with applications in metaphysics, epistemology, and computer science. Possible world semantics did not replace earlier modal systems; it gave them a model-theoretic foundation that made their differences precise.
Many-Valued Logic (1920–present) challenged the principle of bivalence—the assumption that every proposition is either true or false. Łukasiewicz and Post independently introduced logics with three or more truth values, motivated by problems about future contingents and by algebraic considerations. Many-valued logics coexist with classical logic as specialized tools for reasoning about vagueness, partial information, and quantum phenomena. They do not reject classical logic wholesale; they narrow its scope by relaxing one of its core assumptions.
Intuitionistic Logic (1930–present) grew out of L. E. J. Brouwer's philosophy of mathematics, which rejected the law of excluded middle for infinite domains. Arend Heyting formalized the logic that Brouwer's constructive mathematics allowed. Intuitionistic logic preserves the classical rules for conjunction, disjunction, and existential quantification but rejects the equivalence of ¬¬p and p. It is not a rival to classical logic so much as a stricter system that requires proofs to be constructive. It has deep connections with type theory and with the proof-theoretic tradition.
Proof Theory (1920–present) studies logical consequence from the syntactic side. David Hilbert's program aimed to prove the consistency of mathematics using finitary methods. Gerhard Gentzen transformed the field by inventing natural deduction and the sequent calculus, which display the structure of proofs in a systematic way. Proof theory analyses the structural rules that govern inference—weakening, contraction, exchange—and it provides a framework for comparing different logics by their proof-theoretic properties. It is the natural home for intuitionistic logic and for substructural logics.
Model-Theoretic Semantics (1933–present) studies logical consequence from the semantic side. Alfred Tarski defined truth in a formal language by specifying how the truth of a sentence depends on the interpretation of its parts. This made it possible to define logical consequence as truth preservation across all interpretations (models). Model theory is the semantic complement to proof theory: a proof shows that a conclusion follows from premises by syntactic manipulation, while a model-theoretic argument shows that no counterexample exists. The two frameworks are complementary rather than competing, though they embody different philosophical commitments about the nature of logical consequence.
Paraconsistent Logic (1948–present) rejects the principle of explosion (ex contradictione quodlibet), which says that from a contradiction any proposition follows. Paraconsistent logicians argue that some contradictions can be true without trivializing the system. These logics are designed for reasoning about inconsistent information, such as in legal reasoning or in theories that are known to be inconsistent but still useful. Paraconsistent logic does not reject classical logic entirely; it modifies the rule that allows any conclusion from a contradiction.
Substructural Logics (1958–present) are a family of systems that restrict one or more of the structural rules of the sequent calculus. Relevance logic, for example, drops the rule of weakening to ensure that premises must actually be used in a proof. Linear logic drops both weakening and contraction, treating each premise as a resource that can be used exactly once. Substructural logics arose from proof-theoretic analysis of structural rules, but they also have independent philosophical motivations in relevance, resource sensitivity, and the logic of computation.
Today formal logic is a pluralistic field. Classical predicate logic remains the default framework for most mathematical and philosophical work; it is the infrastructure on which other systems are built. Proof theory and model-theoretic semantics are the two main metatheoretic perspectives, and they coexist in a productive tension: proof theorists emphasize the constructive and computational aspects of logic, while model theorists emphasize the semantic and algebraic aspects. Modal logic, many-valued logic, intuitionistic logic, paraconsistent logic, and substructural logics are all active research areas, each with its own community and applications.
The leading frameworks agree that logical consequence can be studied formally, that different logics are appropriate for different domains, and that metatheoretic results (completeness, decidability, consistency) are central to the discipline. They disagree about which logic is fundamental, about the role of semantics versus proof theory, and about whether classical logic should be the default or one option among many. This disagreement is not a sign of crisis; it is the engine of the field's continued development.