README⤓ .txt 2026-08-19T232019.000 000000000008360 Proof calculi and the metatheory of derivation: the formats in which proofs are built and the theorems about their structure, normalization, and strength. Where a model-theoretic entry studies what a logic's formulas describe, an entry here studies how its proofs are constructed and what they cost.
Artin Gluing⤓ .md 2026-08-20T081215.000 000000000053280 The gluing construction is Artin's, from SGA4 (1972), where it assembles a topos from an open and its closed complement. Peter Freyd, "Aspects of topoi" (1972), used it to prove the disjunction and existence properties for intuitionistic logic categorically. Lambek and Scott's Introduction to Higher Order Categorical Logic (1986) is where the logical technique was systematized; Taylor's Practical Foundations (1999) and Streicher's later work extend it to type theory.
Averroes Logic⤓ .md 2026-08-20T075612.000 000000000034480 Ibn Rushd (1126-1198). Andalusian philosopher. Aristotle commentator. Against Avicenna on some points. Foundation of Latin Averroism.
Axiomatic Truth⤓ .md 2026-10-22T165042.936 000000000000744 Tarski (1933) showed truth is not definable in the object language and drew the hierarchy conclusion. The axiomatic alternative — add a truth predicate and axioms for it, rather than define it — was developed by Feferman (1962, 1991), Friedman and Sheard (1987), Cantini, Halbach (Axiomatic Theories of Truth, 2011), and Horsten. The Kripke–Feferman system axiomatizes what Kripke's fixed-point construction produces semantically.
BHK Interpretation⤓ .md 2026-08-20T065609.000 000000000036360 Brouwer, Heyting, Kolmogorov (1920s-1930s). Proofs as constructions. Meaning-as-use for connectives. Foundation for intuitionistic logic semantics. Basis for Curry-Howard.
Circular Proofs⤓ .md 2026-08-20T072654.000 000000000040336 Brotherston and Simpson (2007, 2011) gave the systematic treatment: CLKID^ω, a cyclic calculus for first-order logic with inductive definitions, set against LKID, the same logic with explicit induction rules. The technique has older roots — Niwiński and Walukiewicz (1996) used tableaux with a trace condition for the μ-calculus, and Santocanale (2002) gave circular proofs a categorical semantics. The governing idea is Fermat's infinite descent: a cycle is admissible when traversing it forever would force an infinite decrease.
Connection Method⤓ .md 2026-10-22T223951.000 000000000064240 Wolfgang Bibel, "On Matrices with Connections" (Journal of the ACM 28(4), 1981, 633–645), with the book-length development in Automated Theorem Proving (Vieweg, Wiesbaden 1982; second edition 1987); independently Peter B. Andrews, "Refutations by Matings" (IEEE Transactions on Computers C-25, 1976, 801–807) and "Theorem Proving via General Matings" (Journal of the ACM 28(2), 1981, 193–214), where the method is stated for arbitrary sentences rather than normal forms. Elmar Eder, Relative Complexities of First Order Calculi (Vieweg, 1992), is the systematic comparison of the method with resolution and the sequent-based calculi. Jens Otten and Bibel's leanCoP ("leanCoP: lean connection-based theorem proving", Journal of Symbolic Computation 36, 2003, 139–161) made the calculus the basis of a family of compact provers.
Curry-Howard Correspondence⤓ .md 2026-08-20T065744.000 000000000046032 Haskell Curry observed the combinator/axiom analogy (1934, 1958); William Howard wrote it out for natural deduction and typed lambda calculus (1969, published 1980). Also called the proofs-as-programs or propositions-as-types principle. The organizing bridge between logic, type theory, and computation.
Deep Inference⤓ .md 2026-10-22T090714.000 000000000051024 Guglielmi and others developed deep inference (2000s). Rules apply inside formulas, not just at root. Calculus of structures: main formalism. Enables new proof transformations. More symmetric than sequent calculus.
Dialectica Interpretation⤓ .md 2026-10-22T090631.000 000000000056480 Gödel, "Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes", published in the journal Dialectica in 1958, from which the interpretation takes its name. The paper was written to extend Hilbert's finitary standpoint far enough to give a consistency proof for arithmetic, replacing quantification over infinite domains by computable functionals of finite type. Diller and Nahm (1974) gave the bounded variant that avoids deciding the matrix; Shoenfield (1967) recast the interpretation for classical arithmetic directly; Kohlenbach's monotone functional interpretation (1996) turned it into the working tool of proof mining.
Display Logic⤓ .md 2026-08-20T064841.000 000000000042728 Belnap, "Display logic" (Journal of Philosophical Logic, 1982); also called the display calculus. Wansing (1998) and Goré (1998) developed the modal and substructural instances. Generalized sequent calculus with display property. Structures can be rearranged ("displayed"). Modular: add connectives by adding rules. Foundation for proof-theoretic analysis of many logics.
DPLL and SAT Solving⤓ .md 2026-08-20T062913.000 000000000034880 Davis-Putnam (1960), Davis-Logemann-Loveland (1962); conflict-driven clause learning (Marques-Silva, Sakallah, 1996; Chaff, 2001). Decision procedures for propositional satisfiability.
Existential Graphs⤓ .md 2026-10-22T180154.561 000000000000896 Charles Sanders Peirce invented the existential graphs in 1896 — Murphey's dating, cited by Zeman and repeated by Ma and Pietarinen — as the successor to the entitative graphs, published in "The Logic of Relatives" (The Monist, 1897). Peirce called the graphs his chef d'oeuvre and worked on them until his death, but printed almost nothing: the principal lifetime publication is "Prolegomena to an Apology for Pragmaticism" (The Monist 16(4), 1906, 492–546), and the main corpus reached print posthumously in the Collected Papers, volume IV, paragraphs 4.372–584 (1933). The modern metatheory begins with J. Jay Zeman's dissertation "The Graphical Logic of C. S. Peirce" (University of Chicago, 1964); Don D. Roberts, The Existential Graphs of Charles S. Peirce (Mouton, The Hague, 1973), is the standard study of the system and its manuscript development; Sun-Joo Shin, The Iconic Logic of Peirce's Graphs (MIT Press, 2002), re-reads the rules.
Focusing⤓ .md 2026-08-20T065043.000 000000000044592 Andreoli (1992) for linear logic. Organizes proof search phases. Synchronous vs asynchronous connectives. Eliminates don't-care nondeterminism. Foundation for modern proof search.
Game Semantics⤓ .md 2026-10-22T165042.936 000000000000808 Lorenzen's dialogical logic (1960s). Hintikka's game-theoretic semantics (1970s). Abramsky, Jagadeesan, Malacaria: full abstraction (1990s). Games between Proponent (verifier) and Opponent (falsifier). Foundation for programming language semantics.
Gentzen Systems⤓ .md 2026-10-22T165042.936 000000000000872 Gerhard Gentzen (1934-1935). Twin proof systems: natural deduction and sequent calculus. Hauptsatz (cut elimination). Consistency proof for arithmetic. Foundation of structural proof theory.
Geometry of Interaction⤓ .md 2026-08-20T023021.000 000000000049440 Jean-Yves Girard, "Geometry of interaction I: interpretation of System F" (1989), and the sequence through GoI V (1989–2011). Danos and Regnier's "Local and asynchronous beta-reduction" (1993, 1995) gave the path-algebra reading; Abramsky, Haghverdi, and Scott's "Geometry of interaction and linear combinatory algebras" (2002) gave the categorical axiomatization; Mackie's The Geometry of Interaction Machine (1995) built a compiler from it.
Ghazali Logic⤓ .md 2026-08-20T075804.000 000000000034448 Al-Ghazālī (1058-1111). Logic without metaphysics. Miʿyār al-ʿilm (Standard of Knowledge). Logic as neutral tool. Foundation of post-classical Islamic logic.
Godel Incompleteness Theorems⤓ .md 2026-10-22T180154.561 000000000000984 Gödel (1931). Intrinsic limits of formal axiomatic systems. Any consistent, effectively axiomatized theory strong enough for arithmetic is incomplete and cannot prove its own consistency.
Hetucakra⤓ .md 2026-10-22T165042.936 000000000000824 Dignāga (c. 480–c. 540 CE), in three works on reasoning: the Hetucakraḍamaru ("Drum Wheel of Reason"), preserved only in Tibetan translation; the Nyāyamukha, extant in Chinese; and the Pramāṇasamuccaya with his own commentary, the Pramāṇasamuccayavṛtti, four of whose six chapters concern inference and argument. His teacher Vasubandhu's Vādavidhi had already required of a good reason the indispensability relation avinābhāva; the trairūpya consolidates that line into three conditions, and the wheel is the classification Dignāga built on them. Śaṅkarasvāmin (c. 6th century), a pupil of Dignāga, condensed the system into the Nyāyapraveśa, which the Chinese tradition attributes to him and the Tibetan tradition to Dignāga himself. Xuanzang (602–664) translated the Nyāyapraveśa and the Nyāyamukha into Chinese; Yijing's later Chinese translation of the Pramāṇasamuccaya was lost; Kuiji (632–682), Xuanzang's student, fixed the East Asian reading in his Great Commentary on the Nyāyapraveśa.
Hilbert Systems⤓ .md 2026-10-22T180154.561 000000000000872 Gottlob Frege's Begriffsschrift (1879) is the first: six axioms over implication and negation, with modus ponens as the rule. David Hilbert and Wilhelm Ackermann, Grundzüge der theoretischen Logik (1928), and David Hilbert and Paul Bernays, Grundlagen der Mathematik (I 1934, II 1939), made the format the standard vehicle of metamathematics, which is why it carries Hilbert's name rather than Frege's. Jan Łukasiewicz simplified Frege's axiomatization — one of Frege's axioms is derivable from the others — and his three-axiom basis for classical propositional logic became the textbook standard.
Labelled Deduction⤓ .md 2026-08-20T030340.000 000000000037536 Gabbay (1990s). Labels encode semantic information. Worlds as labels in proof system. Relational atoms for accessibility. Uniform proof theory for modal logics.
Lambda-Mu Calculus⤓ .md 2026-10-22T180154.561 000000000000896 Michel Parigot, "λμ-calculus: an algorithmic interpretation of classical natural deduction" (LPAR 1992, Springer LNCS 624, pp. 190–201): a term calculus for classical natural deduction with multiple conclusions, extracted from Parigot's free deduction. The prehistory is control operators: Timothy Griffin, "A formulae-as-types notion of control" (POPL 1990), typed Felleisen's C operator with ¬¬A → A and call/cc with Peirce's law, extending Curry–Howard to classical logic through an existing programming construct; Parigot's calculus gave that discovery a proof theory of its own, with μ-abstraction as a primitive binder rather than a constant added to λ.
Medieval Consequentiae⤓ .md 2026-08-20T073918.000 000000000033960 14th century. Buridan, Ockham, Burley. Inference theory. Valid consequence. Foundation of medieval proof theory.
Medieval Sophismata⤓ .md 2026-08-20T074421.000 000000000034512 13th-14th century. Bradwardine, Heytesbury, Kilvington. Puzzle sentences. Logical analysis. Foundation of semantic puzzles.
Medieval Terminist Logic⤓ .md 2026-08-20T073638.000 000000000046720 13th-14th century. William of Sherwood, Peter of Spain, Ockham. Properties of terms. Supposition theory. Foundation of medieval semantics.
Natural Deduction⤓ .md 2026-08-20T061702.000 000000000039272 Gentzen (1934-1935). Proof system matching natural reasoning. Introduction and elimination rules. Normalization theorem. Curry-Howard correspondence to λ-calculus.
Navya-Nyaya⤓ .md 2026-08-20T074702.000 000000000039896 Gaṅgeśa Upādhyāya, Tattvacintāmaṇi (14th c.). Rigorous technical language. Property theory. Formal semantics. Developed by Raghunātha, Jagadīśa, Gadādhara. Foundation of late Indian logic.
Normalization⤓ .md 2026-10-22T090936.000 000000000036344 Gentzen (1935) cut elimination. Prawitz (1965) for natural deduction. Proofs simplify to canonical form. Foundation for proof theory and type theory.
Ordinal Analysis⤓ .md 2026-10-22T180154.561 000000000000880 Gentzen (1936), Buchholz, Pohlers, Rathjen. Proof-theoretic strength. Ordinal bounds. Consistency proofs. Foundation of proof theory.
Ordinal Logic⤓ .md 2026-10-22T090631.000 000000000036496 Alan Turing, Systems of Logic Based on Ordinals (PhD thesis under Church, 1938; published 1939) — the work he did between the halting problem and Bletchley Park, and the deepest response to incompleteness anyone made. Solomon Feferman, "Transfinite recursive progressions of axiomatic theories" (1962), reworked it and drew the conclusions; Feferman and Spector (1962) supplied the limitative results.
Polarized Logic⤓ .md 2026-10-22T090714.000 000000000041400 Girard introduced polarity (1991, 1993). Andreoli: focusing (1992). Laurent: polarized linear logic (2002). Formulas have polarity: positive (synchronous) or negative (asynchronous). Controls proof search. Foundation for focused proof systems.
Proof Mining⤓ .md 2026-08-20T071705.000 000000000043640 Kreisel asked in the 1950s, under the name unwinding, what a proof yields beyond the truth of its conclusion. Kohlenbach turned the question into a systematic program from the 1990s, based on a monotone variant of Gödel's Dialectica interpretation (1996) and collected in Applied Proof Theory (2008). The results of the subject are theorems of analysis obtained by logical means, not theorems about logic.
Proof Nets⤓ .md 2026-08-20T065251.000 000000000035928 Girard (1987) for linear logic. Graph representation of proofs. Identifies proofs differing only by inessential rule permutations. Correctness criterion replaces derivation trees.
Proof-Theoretic Semantics⤓ .md 2026-10-22T165042.936 000000000000896 Gentzen's remark (1934–35) that the introduction rules "define" the connectives and the eliminations are consequences of that definition. Prawitz turned it into a programme in Natural Deduction (1965) and "Ideas and results in proof theory" (1971); Dummett gave it the philosophical case in The Logical Basis of Metaphysics (1991). The term is Schroeder-Heister's (1991); Francez's Proof-Theoretic Semantics (2015) is the textbook.
Realizability⤓ .md 2026-10-22T092654.000 000000000061896 Kleene introduced realizability (1945) to interpret intuitionistic logic via computable functions. A formula is true if "realized" by a computation. Connects constructive logic to computability theory. Extended by Kreisel, Troelstra, and others. Foundation for program extraction from proofs.
Resolution⤓ .md 2026-08-20T061856.000 000000000050960 J. A. Robinson, "A Machine-Oriented Logic Based on the Resolution Principle" (JACM, 1965), which fused Herbrand's theorem with a single inference rule and made the instantiation step computable by syntactic unification. It replaced the ground enumeration of Davis and Putnam (1960) and of Gilmore (1960), where every proof had to guess Herbrand instances in advance. Kowalski and Kuehner's SL-resolution (1971) and the SLD restriction to Horn clauses gave Prolog its execution model; Robinson and Wos added paramodulation (1969) for equality, which later became superposition.
Reverse Mathematics⤓ .md 2026-08-20T013702.000 000000000040456 Friedman initiated reverse mathematics (1970s). Simpson systematized (1999). Studies which axioms are needed to prove theorems. Five main subsystems of second-order arithmetic. Calibrates logical strength of ordinary mathematics.
Sequent Calculus⤓ .md 2026-10-22T090714.000 000000000036936 Gentzen introduced sequent calculus (1934-35). Proof system with sequents Γ ⊢ Δ. Cut-elimination theorem: proofs can be normalized. Foundation for proof theory. Structural proof analysis and proof search.
Stoic Logic⤓ .md 2026-08-20T092119.000 000000000046000 Stoa, 3rd c. BCE. Chrysippus of Soli, building on Diodorus Cronus and Philo of Megara. The first systematic propositional logic. Reconstructed from Sextus Empiricus, Diogenes Laertius, Galen. Foundation of Western sentential inference, rediscovered by 20th-century logicians.
Superposition Calculus⤓ .md 2026-10-22T180154.561 000000000000928 Leo Bachmair and Harald Ganzinger, "Rewrite-based equational theorem proving with selection and simplification" (Journal of Logic and Computation 4(3), 1994, 217–247). The ancestry is twofold: George Robinson and Larry Wos's paramodulation (1969) added an equality-replacement rule to resolution, and Donald Knuth and Peter Bendix, "Simple word problems in universal algebras" (in Computational Problems in Abstract Algebra, ed. John Leech, Pergamon 1970, 263–297), showed that orienting equations by a reduction ordering and resolving critical pairs yields a decision procedure whenever completion terminates. Superposition is the merger: paramodulation disciplined by Knuth–Bendix-style orderings, with literal selection and a redundancy criterion that admits simplification into the calculus itself.
Tableaux⤓ .md 2026-10-22T090836.000 000000000035616 Beth (1955), Smullyan (1968). Tree-based proof search. Formulas labeled signed. Branch closure for contradiction. Foundation for automated reasoning.
Unification⤓ .md 2026-08-20T062308.000 000000000037528 Herbrand (1930) implicit; Robinson (1965) gave the explicit algorithm within resolution. Solving term equations by substitution. Core engine of automated deduction and type inference.
Uniform Proofs⤓ .md 2026-10-22T090714.000 000000000042360 Miller, Nadathur, Pfenning, Scedrov introduced uniform proofs (1991). Characterizes logic programming proof search. Goal-directed: right rules applied eagerly. Hereditary Harrop formulas: logic programming in higher-order setting. Foundation for λProlog.
CRITERIA⤓ .txt 2026-07-15T232215.000 000000000009360 Not sufficient: A result about models or definability (Model-Theory). A categorical semantics of proofs (Categorical). A theory of computability (Computability).