• README ⤓ .txt 2026-10-22T165042.936 000000000000752
  The logics complete for Boolean algebras: the bivalent classical systems in which excluded middle, non-contradiction, and bivalence hold and consequence is truth preservation over two-valued models. The propositional core is complete for the two-element Boolean algebra; its quantificational extensions add cylindric and polyadic structure over the same Boolean base. It spans that core, its fragments and extensions, and the historical term and syllogistic traditions that codify classical validity.
• Aristotelian Modal Syllogistic ⤓ .md 2026-10-22T180154.561 000000000000936
  Aristotle (4th c. BCE). Prior Analytics A.8–22, with the modal conversion rules in A.3. The modal extension of the assertoric syllogistic: premises and conclusions qualified by necessity and contingency. The first system of modal logic. Disputed from the start — Theophrastus and Eudemus, Aristotle's own school, rejected his mixed apodeictic moods.
• Aristotelian Syllogistics ⤓ .md 2026-10-22T092432.000 000000000037208
  Aristotle (4th c. BCE). Prior Analytics. Formal deduction from premises. Foundation of Western logic for two millennia.
• Bernays-Schonfinkel Class ⤓ .md 2026-10-22T180154.561 000000000000896
  Paul Bernays and Moses Schönfinkel, "Zum Entscheidungsproblem der mathematischen Logik" (Mathematische Annalen 99, 1928, 342–372), proved satisfiability decidable for relational prenex sentences with prefix ∃∀, without equality. Frank P. Ramsey, "On a Problem of Formal Logic" (read to the London Mathematical Society in December 1928, published in its Proceedings 30, 1930, 264–286), extended the result to equality, proving as his combinatorial lemma the theorem now called Ramsey's theorem; the class with equality is the Bernays–Schönfinkel–Ramsey class. Harry R. Lewis (1980) proved satisfiability NEXPTIME-complete. The solvable-cases program it belongs to is codified in Egon Börger, Erich Grädel and Yuri Gurevich, The Classical Decision Problem (Springer, 1997).
• Boolean Algebra ⤓ .md 2026-08-20T061730.000 000000000037152
  Boole introduced algebraic logic (1847, 1854). Stone proved representation theorem (1936). Algebraic foundation of propositional logic. Every Boolean algebra is isomorphic to a field of sets. Universal in digital circuits, databases, and logic.
• Definite Descriptions ⤓ .md 2026-10-22T090836.000 000000000038616
  Russell (1905). "The present King of France" problem. Contextual definition. Scope distinctions. Foundation for reference theory.
• Epsilon Calculus ⤓ .md 2026-10-22T090936.000 000000000049024
  David Hilbert introduced the ε-operator in the early 1920s — "Die logischen Grundlagen der Mathematik" (1923) uses a dual form of the operator, and the standard form first appears in print in Ackermann's dissertation (1924) — as the device that would let quantifiers be traded for terms, so that consistency could be attacked by finitary means. Wilhelm Ackermann developed the substitution method (1924), and corrected and extended it in 1940. Hilbert and Bernays, Grundlagen der Mathematik II (1939), contains the two epsilon theorems and the fullest development. Bourbaki adopted a variant of the operator, written τ, as a primitive of the Éléments.
• First-Order Logic ⤓ .md 2026-08-20T084848.000 000000000051152
  Gottlob Frege's Begriffsschrift (1879) introduced quantification over individuals. Charles Sanders Peirce independently developed quantification (1885). Giuseppe Peano developed logical notation (1889). Bertrand Russell and Alfred North Whitehead systematized it in Principia Mathematica (1910-1913). Also called predicate logic, predicate calculus, or quantificational logic. The standard logic of mathematics and formal verification.
• Fluted Fragment ⤓ .md 2026-10-22T091839.000 000000000036304
  Quine (1969), Purdy (1996). Variables in strict order. No variable reordering in atoms. Decidable fragment of FOL. Between monadic and full FOL.
• Free Logic ⤓ .md 2026-10-22T165042.936 000000000000776
  Lambert introduced free logic (1960). Logic free of existential assumptions. Terms may denote nothing (non-denoting terms). Addresses: "The present king of France is bald." Empty domains allowed. Important for definite descriptions and fiction.
• Guarded Fragment ⤓ .md 2026-10-22T090749.000 000000000045432
  Andréka, van Benthem, Németi (1998). Decidable fragment of first-order logic. Variables must be "guarded" by atoms. Generalizes modal logic to first-order. Foundation for description logic decidability.
• Higher-Order Logic ⤓ .md 2026-08-20T062849.000 000000000047088
  Alonzo Church's simple theory of types (1940) combined lambda calculus with logic. Leon Henkin provided semantics (1950). Mike Gordon developed HOL for hardware verification (1980s). Basis for major proof assistants: Isabelle/HOL, HOL4, HOL Light, PVS. Distinct from second-order logic in treatment of types and functions.
• Horn Logic ⤓ .md 2026-10-22T093123.000 000000000041216
  Alfred Horn, "On sentences which are true of direct unions of algebras" (Journal of Symbolic Logic, 1951) — the clauses are named for a preservation theorem, not for a computational property, and the computational property was found twenty years later. Kowalski (1974) read Horn clauses as procedures; Dowling and Gallier (1984) gave the linear-time propositional algorithm.
• Identity Logic ⤓ .md 2026-08-20T062233.000 000000000049504
  Leibniz stated the two principles that bear his name — identicals are indiscernible, and (more contentiously) indiscernibles are identical. Frege gave identity its first formal treatment in the Begriffsschrift (1879), where he read it as sameness of content between signs, and revised that reading in "Über Sinn und Bedeutung" (1892) after seeing that the informativeness of a = b cannot be explained if identity relates signs. Whitehead and Russell's Principia defined identity second-order, by indiscernibility. Hilbert and Ackermann (1928) fixed the modern first-order treatment: identity as a distinguished binary predicate with its own axioms, part of the logic rather than of any theory.
• Implicational Calculus ⤓ .md 2026-10-22T090413.000 000000000048224
  Frege's Begriffsschrift (1879) already isolates it; Łukasiewicz and Tarski studied the axiomatics through the 1920s–30s; Tarski and Bernays gave the standard three axioms; Łukasiewicz found a single axiom for the classical fragment and proved it shortest (1948). Church's simply typed λ-calculus (1940) is its Curry–Howard image, though nobody said so until Howard (1969).
• Infinitary Logic ⤓ .md 2026-08-20T062948.000 000000000046488
  Developed in the 1960s-70s by Carol Karp, Dana Scott, and others. Extends first-order logic to allow infinitely long formulas — infinite conjunctions and disjunctions. Studies the boundary between first-order and second-order expressiveness. Key results: Scott's isomorphism theorem, Lopez-Escobar's theorem on invariant formulas.
• Laws of Form ⤓ .md 2026-08-20T065427.000 000000000046488
  G. Spencer-Brown, Laws of Form (Allen & Unwin, 1969), written while consulting on railway signalling circuits and published with a Bertrand Russell endorsement on the dust jacket — a blurb, not a foreword, though it is routinely upgraded to one in the secondary literature. Received by the cybernetics community — Heinz von Foerster reviewed it, Francisco Varela extended it (1975), Louis Kauffman formalized the reception. Niklas Luhmann built his social systems theory on its distinction primitive.
• Leibniz Logical Calculus ⤓ .md 2026-10-22T180154.561 000000000000888
  Gottfried Wilhelm Leibniz, in working drafts spanning 1679–1690, none published in his lifetime: the characteristic-number essays of April 1679 (Elementa calculi and its companions), the Generales Inquisitiones de Analysi Notionum et Veritatum (1686), and the calculus of real addition of about 1690 (Gerhardt, Philosophische Schriften VII, 236–247; translated by Parkinson as "A Study in the Calculus of Real Addition"). Nineteenth-century editions by Erdmann and Gerhardt printed fragments; Louis Couturat's La Logique de Leibniz (1901) and Opuscules et fragments inédits de Leibniz (1903) recovered the program whole — the Generales Inquisitiones appeared there for the first time — after Peirce and Frege had already built modern logic without it.
• Lesniewski Systems ⤓ .md 2026-10-22T224254.000 000000000079288
  Stanisław Leśniewski (1886–1939), professor of the foundations of mathematics at Warsaw from 1919 and, with Jan Łukasiewicz, co-founder of the Warsaw School of Logic. The three systems were built in the reverse of their logical order: Mereology first, in "Podstawy ogólnej teorii mnogości I" (Moscow: Popławski, 1916); the single axiom of Ontology in 1920, published in "Über die Grundlagen der Ontologie" (Sprawozdania z posiedzeń Towarzystwa Naukowego Warszawskiego 22, 1930, 111–132); Protothetic last, published in "Grundzüge eines neuen Systems der Grundlagen der Mathematik" (Fundamenta Mathematicae 14, 1929, 1–81; continuation in Collectanea Logica 1, 1938), with the philosophical series "O podstawach matematyki" (Przegląd Filozoficzny 30–34, 1927–1931) running alongside. Alfred Tarski, Leśniewski's only doctoral student (doctorate 1924), proved in his dissertation that conjunction is definable from material equivalence and the quantifier, so equivalence can serve as Protothetic's sole primitive. The systems survive through reconstruction — Jerzy Słupecki ("St. Leśniewski's protothetics", Studia Logica 1, 1953, 44–111; "S. Leśniewski's calculus of names", Studia Logica 3, 1955, 7–71), Bolesław Sobociński, Czesław Lejewski ("Logic and Existence", 1954; "On Leśniewski's Ontology", 1958), E. C. Luschei (The Logical Systems of Leśniewski, 1962), the Srzednicki–Stachniak volumes (S. Leśniewski's Lecture Notes in Logic, 1988; Leśniewski's Systems: Protothetic, Nijhoff International Philosophy Series, 1998), and Peter Simons's Stanford Encyclopedia entry (2007, revised 2020).
• Many-Sorted Logic ⤓ .md 2026-10-22T180154.561 000000000000832
  Arnold Schmidt's "Über deduktive Theorien mit mehreren Sorten von Grunddingen" (1938) is the first systematic treatment, though sorted reasoning is older than its formalization — geometry had always quantified separately over points, lines and planes, and Herbrand worked with sorted domains informally. Hao Wang's "Logic of many-sorted theories" (1952) settled the relation to ordinary first-order logic by giving the relativization translation and proving it faithful. Goguen and Meseguer later developed order-sorted algebra, adding a subsort ordering and the regularity conditions that make it usable, and through the algebraic specification tradition — OBJ, CASL, Maude — many-sorted logic became the default setting for machine-checked specification.
• Mohist Logic ⤓ .md 2026-10-22T180154.561 000000000000792
  Later Mohist school, c. 300 BCE. The six dialectical chapters of the Mòzǐ (books 40–45): two books of Canons (jīng 經), two of Explanations (jīngshuō 經說), the Dàqǔ 大取 and the Xiǎoqǔ 小取, together the Mòbiàn 墨辯, compiled between the late 4th and mid 3rd century BCE. Transmitted in disorder and badly damaged, the Dàqǔ worst. A. C. Graham, Later Mohist Logic, Ethics and Science (School of Oriental and African Studies / Chinese University Press 1978) is the reconstruction and the only Western-language translation; Chris Fraser's Stanford Encyclopedia entries "Mohist Canons" and "Logic and Language in Early Chinese Philosophy" and Dan Robins, "The Later Mohists and Logic" (History and Philosophy of Logic 2010) carry the current interpretation. The tradition ended with the Qin.
• Monadic First-Order Logic ⤓ .md 2026-10-22T180154.561 000000000000896
  Leopold Löwenheim, "Über Möglichkeiten im Relativkalkül" (Mathematische Annalen 76, 1915, 447–470), proved satisfiability decidable for first-order formulas whose predicates are all unary — the first substantial decidability result for a fragment of first-order logic, in the same paper that proved the Löwenheim–Skolem theorem. Thoralf Skolem, "Untersuchungen über die Axiome des Klassenkalküls" (1919), extended decidability to monadic second-order logic, and Heinrich Behmann's Habilitation thesis (Mathematische Annalen, 1922) solved the class again independently; the word "Entscheidungsproblem" itself first appears in Behmann's Göttingen lecture of 10 May 1921. The small-model argument that became the textbook proof was outlined by Hilbert and Bernays in their 1922/23 lecture course and printed in Hilbert–Ackermann (1928). Harry R. Lewis, "Complexity Results for Classes of Quantificational Formulas" (Journal of Computer and System Sciences 21, 1980), settled the complexity: NEXPTIME-complete.
• Monadic Second-Order Logic ⤓ .md 2026-10-22T091841.000 000000000038080
  Büchi (1960) for automata theory. Second-order quantification over sets only. Decidable on trees (Rabin). Captures regular languages. Foundation for automata-logic connection.
• Plural Logic ⤓ .md 2026-08-20T063138.000 000000000039224
  Boolos argued for plural quantification (1984, 1985). Avoids set-theoretic commitment for second-order-like reasoning. "There are some critics who admire only one another." Plurals in natural language. Linnebo and others developed formal systems.
• Propositional Logic ⤓ .md 2026-10-22T090143.000 000000000042392
  Gottlob Frege's Begriffsschrift (1879) provided the first fully formal propositional calculus. Bertrand Russell and Alfred North Whitehead systematized it in Principia Mathematica (1910-1913). George Boole's earlier algebraic logic (1847, 1854) established the connection between logic and algebra. Also called sentential logic, statement logic, or zeroth-order logic.
• Quantified Boolean Formulas ⤓ .md 2026-10-22T180154.561 000000000000976
  Larry J. Stockmeyer and Albert R. Meyer, "Word Problems Requiring Exponential Time: Preliminary Report" (Proceedings of the 5th ACM Symposium on Theory of Computing, 1973, 1–9), proved the truth problem for quantified Boolean formulas PSPACE-complete; the encoding of a long computation by recursive halving follows the construction of Savitch's theorem (1970). Stockmeyer, "The Polynomial-Time Hierarchy" (Theoretical Computer Science 3, 1976, 1–22), fixed the bounded-alternation levels: with k alternating quantifier blocks beginning existentially, truth is Σᵖₖ-complete (Celia Wrathall, 1977, for CNF and DNF matrices). Q-resolution is from Hans Kleine Büning, Marek Karpinski and Andreas Flögel, "Resolution for Quantified Boolean Formulas" (Information and Computation 117, 1995, 12–18); the dependency-quantified extension descends from Gary L. Peterson and John H. Reif, "Multiple-Person Alternation" (FOCS 1979), completed in Peterson, Reif and Azhar (2001).
• Relational Calculus ⤓ .md 2026-10-22T090146.000 000000000038312
  E. F. Codd, "A relational model of data for large shared data banks" (1970) and "Relational completeness of data base sublanguages" (1972), where the calculus and the theorem relating it to the algebra both appear. Lacroix and Pirotte (1977) gave the domain variant. The founding result of database theory, and the reason SQL looks like logic and runs like algebra.
• Second-Order Logic ⤓ .md 2026-08-20T085834.000 000000000048080
  Implicit in Frege's Grundgesetze (1893). Explicitly developed through work on foundations of mathematics. David Hilbert and Wilhelm Ackermann distinguished first and second order (1928). Debates about its status: is it really "logic" or disguised set theory? Quine skeptical; Boolos and others defended it.
• 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.
• Stone Duality ⤓ .md 2026-08-20T065407.000 000000000037960
  Marshall Stone, "The theory of representations for Boolean algebras" (1936) and "Applications of the theory of Boolean rings to general topology" (1937). Priestley extended it to bounded distributive lattices (1970). The theorem that made "algebra and topology are the same subject twice" a working method rather than a slogan.
• Two-Variable Logic ⤓ .md 2026-10-22T091842.000 000000000049840
  Dana Scott (1962) showed that FO² without equality reduces to the Gödel prefix class ∀∀∃*, and so is decidable; the reduction is what is now called Scott normal form. Michael Mortimer (1975) extended the result to FO² with equality, proving the finite model property with a doubly exponential bound on model size. Erich Grädel, Phokion Kolaitis and Moshe Vardi (1997) sharpened the bound to exponential and settled the complexity: FO² satisfiability is NEXPTIME-complete. The fragment then acquired a second life as the explanation of why description logics and modal logics are decidable, since the standard translation of modal logic lands inside it.
• CRITERIA ⤓ .txt 2026-10-22T180154.561 000000000000768
  Not sufficient: A first-order theory whose novelty is its non-logical signature and axioms rather than its logic—arithmetic, set theory, mereology (those belong in Theories). Completeness for Heyting algebras or a proper subvariety (Heyting). Admitting a third value or degrees (Many-Valued). Failure of distribution (Orthomodular). Adding a modal, temporal, or other intensional operator (Modal).