README⤓ .txt 2026-07-17T121634.146 000000000000808 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-07-16T004442.000 000000000035304 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-07-17T121634.146 000000000000864 Ibn Rushd (1126-1198). Andalusian philosopher. Aristotle commentator. Against Avicenna on some points. Foundation of Latin Averroism.
Axiomatic Truth⤓ .md 2026-07-17T120407.600 000000000000872 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-07-15T064845.000 000000000015912 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-07-15T071223.000 000000000014616 Brotherston, Simpson (2007). Proofs with cycles. Infinite descent for induction. Finitely representable infinite proofs. Foundation for cyclic proof theory.
Curry-Howard Correspondence⤓ .md 2026-07-17T120407.600 000000000000968 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-07-15T063106.000 000000000018816 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-07-15T064727.000 000000000014112 Gödel (1958) for consistency of arithmetic. Interprets formulas as games between ∃ and ∀. Extracts computational content. Foundation for proof mining.
Display Calculus⤓ .md 2026-07-17T120407.600 000000000000880 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.
Display Logic⤓ .md 2026-07-17T120407.600 000000000000880 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-07-17T120407.600 000000000000912 Davis-Putnam (1960), Davis-Logemann-Loveland (1962); conflict-driven clause learning (Marques-Silva, Sakallah, 1996; Chaff, 2001). Decision procedures for propositional satisfiability.
Focusing⤓ .md 2026-07-15T064550.000 000000000017016 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-07-15T061325.000 000000000020848 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-07-15T064716.000 000000000017712 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-07-16T001736.000 000000000034408 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-07-17T121634.146 000000000000856 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-07-17T120407.600 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.
Labelled Deduction⤓ .md 2026-07-15T064847.000 000000000017856 Gabbay (1990s). Labels encode semantic information. Worlds as labels in proof system. Relational atoms for accessibility. Uniform proof theory for modal logics.
Medieval Consequentiae⤓ .md 2026-07-17T120407.600 000000000000928 14th century. Buridan, Ockham, Burley. Inference theory. Valid consequence. Foundation of medieval proof theory.
Medieval Sophismata⤓ .md 2026-07-17T120407.600 000000000000904 13th-14th century. Bradwardine, Heytesbury, Kilvington. Puzzle sentences. Logical analysis. Foundation of semantic puzzles.
Medieval Terminist Logic⤓ .md 2026-07-17T120407.600 000000000000944 13th-14th century. William of Sherwood, Peter of Spain, Ockham. Properties of terms. Supposition theory. Foundation of medieval semantics.
Natural Deduction⤓ .md 2026-07-15T064548.000 000000000018584 Gentzen (1934-1935). Proof system matching natural reasoning. Introduction and elimination rules. Normalization theorem. Curry-Howard correspondence to λ-calculus.
Navya-Nyaya⤓ .md 2026-07-15T081616.000 000000000018960 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-07-15T065423.000 000000000014528 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-07-17T120407.600 000000000000880 Gentzen (1936), Buchholz, Pohlers, Rathjen. Proof-theoretic strength. Ordinal bounds. Consistency proofs. Foundation of proof theory.
Ordinal Logic⤓ .md 2026-07-17T120407.600 000000000000856 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-07-15T063308.000 000000000018968 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 Nets⤓ .md 2026-07-15T064715.000 000000000015928 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-07-15T235708.000 000000000044704 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-07-15T055807.000 000000000022232 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-07-15T071855.000 000000000015256 Robinson (1965). Refutation-complete for first-order logic. Clause form reasoning. Single inference rule. Foundation for Prolog and SAT solvers.
Reverse Mathematics⤓ .md 2026-07-15T063452.000 000000000019184 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-07-15T062340.000 000000000018360 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-07-17T120407.600 000000000000784 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.
Tableaux⤓ .md 2026-07-15T071852.000 000000000013864 Beth (1955), Smullyan (1968). Tree-based proof search. Formulas labeled signed. Branch closure for contradiction. Foundation for automated reasoning.
Unification⤓ .md 2026-07-17T120407.600 000000000000840 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-07-15T063301.000 000000000018304 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-17T120407.600 000000000000824 Not sufficient: A result about models or definability (Model-Theory). A categorical semantics of proofs (Categorical). A theory of computability (Computability).