README⤓ .txt 2026-10-22T165042.936 000000000000752 The logics complete for Heyting algebras: intuitionistic logic, which identifies truth with construction and drops unrestricted excluded middle, and the systems bounded below by it. Consequence is preservation of designated values over Heyting-algebra models, equivalently validity in the Kripke frames those algebras dualize.
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.
Basic Propositional Logic⤓ .md 2026-08-20T072920.000 000000000046840 Albert Visser, "A propositional logic with explicit fixed points" (1981), where the system arose from the study of provability rather than from a philosophical programme. Developed by Ruitenburg, Ardeshir, Suarez, and Celani–Jansana. A subintuitionistic logic: strictly weaker than intuitionistic propositional calculus, obtained by dropping the reflexivity of the accessibility relation.
Dual-Intuitionistic Logic⤓ .md 2026-10-22T090631.000 000000000044280 C. Rauszer, "A formalization of the propositional calculus of H-B logic" (1974) and the series through 1980, which gave Heyting–Brouwer logic with both implication and co-implication; the dual fragment alone is Goodman's (1981) and Urbas's (1996). McKinsey and Tarski's closure algebras (1946) are the algebraic ancestor. Crolard (2001) gave the type-theoretic reading; Pinto and Uustalu (2009) the sequent calculus.
Esakia Duality⤓ .md 2026-10-22T085315.000 000000000048272 Leo Esakia, "Topological Kripke models" (1974), which gave the duality for Heyting algebras; the Blok–Esakia theorem (Blok 1976, Esakia 1976) is its most consequential corollary. Esakia's Heyting Algebras: Duality Theory was published in English only in 2019, thirty-four years after the Russian original, which is part of why the subject was slow to travel.
Godel Logic⤓ .md 2026-08-20T070143.000 000000000039512 Gödel introduced Gödel logics (1932) studying intuitionistic logic. Infinite-valued with min/max operations. Also called Gödel-Dummett logic. Characterized by linearity axiom: (A→B)∨(B→A). Intermediate between intuitionistic and classical.
Intermediate Logics⤓ .md 2026-08-20T065721.000 000000000046696 Gödel (1932) showed IPC has no finite characteristic matrix and exhibited the first infinite chain; Jaśkowski (1936) gave a characteristic matrix sequence. Dummett (1959) axiomatized LC; Umezawa (1959) and Hosoi (1967) began the systematic study; Jankov (1968) proved the lattice has the cardinality of the continuum. Kuznetsov and Maksimova developed the theory from the 1970s. Logics between intuitionistic and classical. Superintuitionistic logics. Uncountably many exist. Lattice structure under extension.
Internal Logic⤓ .md 2026-08-20T082130.000 000000000045664 Lawvere, Kock, and others (1960s-1970s). Logic interpreted inside a category. Subobject classifier replaces truth values. Intuitionistic in general topoi. Foundation for categorical proof theory.
Intuitionistic Logic⤓ .md 2026-08-20T065602.000 000000000055864 L.E.J. Brouwer founded mathematical intuitionism (1907-1920s), rejecting non-constructive existence proofs. Arend Heyting formalized intuitionistic logic (1930). Kolmogorov gave the "problem interpretation" (1932). Connected to computation via Curry-Howard: proofs are programs, propositions are types. Foundation for constructive mathematics and type-theoretic proof assistants.
Jankov Logic⤓ .md 2026-10-22T090149.000 000000000043576 V. A. Jankov, "The calculus of the weak law of excluded middle" (Izvestiya, 1968), which named and studied it; the axiom appears earlier in Gödel and in Kolmogorov's circle. Jankov's characteristic formulas (1963, 1969) — the tool that made the lattice of intermediate logics tractable — came out of the same work.
Kreisel-Putnam Logic⤓ .md 2026-08-20T074414.000 000000000032408 Georg Kreisel and Hilary Putnam, "Eine Unableitbarkeitsbeweismethode für den intuitionistischen Aussagenkalkül" (Archiv für mathematische Logik, 1957). Constructed to refute a conjecture: Łukasiewicz had proposed that intuitionistic logic is the only intermediate logic with the disjunction property, and KP is the counterexample.
Lax Logic⤓ .md 2026-10-22T180154.561 000000000000712 Haskell Curry found the modality first: his 1948 Notre Dame lectures, published as A Theory of Formal Deducibility (1957), contain a modality with axiom schemata essentially those below, refined in "The elimination theorem when modality is present" (Journal of Symbolic Logic 17, 1952, pp. 249–265), which proves cut elimination with the modality present; the sequent rules below are the ones Curry suggested. Robert Goldblatt, "Grothendieck topology as geometric modality" (Mathematical Logic Quarterly 27, 1981, pp. 495–529), rediscovered it as "it is locally the case that", with nuclei on Heyting algebras as its algebraic semantics. Michael Mendler's Edinburgh thesis (1993) found it a third time in hardware verification, as correctness up to constraints, and Matt Fairtlough and Mendler, "Propositional Lax Logic" (Information and Computation 137, 1997, pp. 1–33), named the logic and consolidated its proof theory and Kripke semantics. Benton, Bierman and de Paiva, "Computational types from a logical perspective" (Journal of Functional Programming 8(2), 1998, pp. 177–193), proved the fourth reading: under Curry–Howard the logic is Moggi's computational lambda calculus.
Markov Principle⤓ .md 2026-08-20T070032.000 000000000045112 A.A. Markov (1950s). Russian constructive mathematics. Computable sequences. Church's thesis. Foundation of recursive mathematics.
Medvedev Logic⤓ .md 2026-10-22T085744.000 000000000041184 Yuri Medvedev, "Finite problems" (1962) and "Interpretation of logical formulas by means of finite problems" (1966). An intermediate logic arising from a semantics of problems rather than of proofs: the logic of finite problems, ML. Studied since by Maksimova, Shehtman, Skvortsov, and connected to inquisitive semantics by Ciardelli and Roelofsen.
Minimal Logic⤓ .md 2026-10-22T090151.000 000000000035816 Johansson introduced minimal logic (1937). Weaker than intuitionistic logic. No ex falso quodlibet (⊥ → A not valid). Negation defined: ¬A = A → ⊥, but ⊥ doesn't imply everything. Foundation for studying negation and absurdity.
Nelson Logic⤓ .md 2026-10-22T165042.936 000000000000792 David Nelson (1949). Constructive logic with strong negation. Two negations: ¬ (weak) and ~ (strong). N3 and N4 variants. Foundation for constructive falsity.
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.
Sheaf Semantics⤓ .md 2026-10-22T090413.000 000000000053960 Grothendieck's sites and sheaves (SGA4, 1963–64, published 1972) supplied the machinery; Lawvere and Tierney's elementary topos (1970) made it logic. Kripke–Joyal forcing is Joyal's reformulation of Kripke's semantics inside a topos; Fourman and Scott, "Sheaves and logic" (1979), and Fourman and Hyland's sheaf models of intuitionistic analysis (1979) are where the model theory was built. Van Dalen and Troelstra's Constructivism in Mathematics (1988) is the standard exposition.
Topos Logic⤓ .md 2026-10-22T165042.936 000000000000824 Lawvere and Tierney developed topos theory (1960s-70s). Toposes generalize both sets and sheaves. Internal logic of a topos is intuitionistic. Provides categorical semantics for higher-order intuitionistic logic. Unifies algebraic geometry, logic, and category theory.
CRITERIA⤓ .txt 2026-10-22T180154.561 000000000000768 Not sufficient: Bivalent classical semantics (Boolean). A many-valued matrix whose motivation is degrees rather than a Heyting reduct (Many-Valued). A term calculus presented purely as a typing discipline (Type). A proof-conditional interpretation of the connectives (BHK, realizability, Dialectica), which is metatheory.