README⤓ .txt 2026-07-17T121634.146 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 Syllogistics⤓ .md 2026-07-17T120407.600 000000000000896 Aristotle (4th c. BCE). Prior Analytics. Formal deduction from premises. Foundation of Western logic for two millennia.
Boolean Algebra⤓ .md 2026-07-15T060905.000 000000000021336 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-07-15T073250.000 000000000013680 Russell (1905). "The present King of France" problem. Contextual definition. Scope distinctions. Foundation for reference theory.
Epsilon Calculus⤓ .md 2026-07-17T120407.600 000000000000824 Hilbert, Bernays (1920s). Choice operator. Indefinite description. Quantifier elimination. Foundation of Hilbert's program.
First-Order Logic⤓ .md 2026-07-17T120407.600 000000000000832 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-07-15T071623.000 000000000013744 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-07-15T060500.000 000000000020544 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-07-15T070719.000 000000000014936 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-07-15T054024.000 000000000027632 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-07-17T120407.600 000000000000816 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-07-15T073254.000 000000000013712 Frege (1879), Leibniz earlier. Identity as logical notion. Substitutivity. Indiscernibility of identicals. Foundation for quantified logic.
Implicational Calculus⤓ .md 2026-07-17T120407.600 000000000000824 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; C. A. Meredith (1953) found a single axiom for the classical fragment. Church's simply typed λ-calculus (1940) is its Curry–Howard image, though nobody said so until Howard (1969).
Infinitary Logic⤓ .md 2026-07-15T055107.000 000000000026520 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-07-17T120407.600 000000000000792 G. Spencer-Brown, Laws of Form (Allen & Unwin, 1969), written while consulting on railway signalling circuits and published with a foreword by Bertrand Russell. 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.
Many-Sorted Logic⤓ .md 2026-07-17T120407.600 000000000000832 Schmidt (1938), Herbrand, Wang. Multiple domains. Typed quantification. Sort hierarchies. Foundation of typed formal systems.
Monadic Second-Order Logic⤓ .md 2026-07-15T070724.000 000000000014528 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-07-15T060502.000 000000000020288 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.
Predicate Calculus⤓ .md 2026-07-17T120407.600 000000000000832 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.
Propositional Calculus⤓ .md 2026-07-15T052400.000 000000000024232 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.
Propositional Logic⤓ .md 2026-07-15T052400.000 000000000024232 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.
Relational Calculus⤓ .md 2026-07-16T005218.000 000000000033360 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-07-15T053138.000 000000000025944 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-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.
Stone Duality⤓ .md 2026-07-17T120407.600 000000000000800 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-07-15T070722.000 000000000012504 Mortimer (1975) proved decidability. FO² — first-order with only two variables. Reuse variables via requantification. NEXPTIME-complete. Foundation for description logic complexity.
CRITERIA⤓ .txt 2026-07-17T120407.600 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).