README⤓ .txt 2026-07-17T121634.146 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-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.
Basic Propositional Logic⤓ .md 2026-07-15T225637.000 000000000026344 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-07-16T004541.000 000000000034544 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-07-17T120407.600 000000000000808 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, forty-five years after the Russian original, which is part of why the subject was slow to travel.
Godel Logic⤓ .md 2026-07-15T061745.000 000000000018008 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-07-15T235628.000 000000000016312 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-07-15T064539.000 000000000015952 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-07-15T053330.000 000000000026744 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-07-16T001249.000 000000000030392 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-07-16T001249.000 000000000025608 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.
Markov Principle⤓ .md 2026-07-17T120407.600 000000000000824 A.A. Markov (1950s). Russian constructive mathematics. Computable sequences. Church's thesis. Foundation of recursive mathematics.
Medvedev Logic⤓ .md 2026-07-15T230424.000 000000000028408 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-07-15T061546.000 000000000018744 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-07-15T070816.000 000000000013648 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-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.
Sheaf Semantics⤓ .md 2026-07-17T121634.146 000000000000856 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-07-15T060040.000 000000000022824 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-07-16T004541.000 000000000012312 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.