Series
Collections of notes arranged in reading order. Start with a guide or choose a subject within a series.
All series
2 series, 34 partsHistory of Logic 28 parts · Started 2026-09-01 #history-of-logic#mathematical-logic#foundations-of-mathematics#interactive-labs#proof-theory +132 more topics
- History of Logic: Series Guide Part 0 introduces the series, its reading order, and routes through foundations, computation, formalization, and earlier logical traditions. #history-of-logic#mathematical-logic#foundations-of-mathematics#formalization#history-of-philosophy#interactive-learning 00
- Boole and the Algebraic Tradition How an algebra of classes became a calculus of relations and quantifiers, through Boole, De Morgan, Peirce, and Schröder. #history-of-logic#mathematical-logic#algebraic-logic#history-of-mathematics#boolean-algebra#relations#quantifiers#interactive-labs 01
- Frege, Quantifiers, and Logical Form Why variables, scope, and explicit inference changed the representation of mathematical proof, and how Frege's project differed from modern first-order logic. #history-of-logic#mathematical-logic#formal-language#foundations-of-mathematics#quantifiers#first-order-logic#logicism#higher-order-logic#interactive-labs 02
- Rigor, Infinity, and the Axiomatic Method How analysis, infinite sets, arithmetic, and alternative geometries changed the questions mathematicians asked about foundations. #history-of-logic#mathematical-logic#foundations-of-mathematics#set-theory#axiomatization#infinity#real-analysis#non-euclidean-geometry#interactive-labs 03
- Paradoxes and Competing Foundations Russell's contradiction, Frege's Basic Law V, ramified types, predicativity, and axiomatic set theory as distinct responses to foundational problems. #history-of-logic#mathematical-logic#foundations-of-mathematics#set-theory#type-theory#logicism#paradoxes#russells-paradox#predicativity#axiomatization#interactive-labs 04
- Hilbert's Program and the Study of Proof Formalization, finitary reasoning, and the attempt to justify infinitary mathematics through a mathematical analysis of finite derivations. #history-of-logic#mathematical-logic#proof-theory#consistency#foundations-of-mathematics#hilberts-program#finitism#epsilon-calculus#formalization 05
- Intuitionism and Mathematical Construction Brouwer, Heyting, constructive evidence, realizability, and the different mathematical programs behind the word constructive. #history-of-logic#mathematical-logic#constructivism#proof-theory#intuitionistic-logic#realizability#classical-logic 06
- Syntax, Truth, and Completeness The distinction between derivability and semantic consequence, from formal syntax and Tarski's semantics to Gödel's theorem, Henkin's construction, and nonstandard models. #history-of-logic#mathematical-logic#semantics#model-theory#completeness#first-order-logic#truth#compactness#lowenheim-skolem 07
- Gödel, Rosser, and Incompleteness How arithmetic represents proofs, how diagonalization produces an undecidable sentence, and what the two incompleteness theorems establish. #history-of-logic#mathematical-logic#incompleteness#proof-theory#foundations-of-mathematics#godels-theorems#arithmetic#diagonalization#consistency 08
- The Emergence of Computability Church, Turing, Kleene, Post, and the mathematical analysis of algorithms, undecidability, relative computation, and Diophantine equations. #history-of-logic#mathematical-logic#computability#algorithms#turing-machines#undecidability#halting-problem#lambda-calculus#interactive-labs 09
- Gentzen and the Structure of Proof Natural deduction, sequent calculus, cut elimination, ordinal analysis, and the continuing investigation of the strength and computational content of proofs. #history-of-logic#mathematical-logic#proof-theory#natural-deduction#consistency#reverse-mathematics#sequent-calculus#cut-elimination#ordinal-analysis#interactive-labs 10
- Model Theory Becomes Mathematics Definability, quantifier elimination, ultraproducts, nonstandard analysis, and classification as tools for understanding mathematical structures. #history-of-logic#mathematical-logic#model-theory#semantics#definability#quantifier-elimination#ultraproducts#nonstandard-analysis#stability-theory 11
- Set Theory and Independence Choice, the continuum hypothesis, Gödel's constructible universe, Cohen's forcing, and the continuing question of which axioms to adopt. #history-of-logic#mathematical-logic#set-theory#independence#foundations-of-mathematics#forcing#continuum-hypothesis#axiom-of-choice#constructibility 12
- Modal Logic: Necessity, Time, Knowledge, and Provability How the study of implication developed into a family of logics whose operators express different kinds of necessity. #history-of-logic#mathematical-logic#modal-logic#semantics#kripke-semantics#temporal-logic#epistemic-logic#provability-logic#interactive-labs 13
- Alternative Logics: Truth, Relevance, Inconsistency, and Resources Four distinct reasons to reconsider classical inference, illustrated through truth values, relevant implication, inconsistent information, and structural rules. #history-of-logic#mathematical-logic#nonclassical-logic#proof-theory#linear-logic#many-valued-logic#relevance-logic#paraconsistent-logic#structural-rules 14
- Lambda Calculus and the Curry–Howard Correspondence How substitution became a theory of computation, and how typed terms came to represent proofs with computational behavior. #history-of-logic#mathematical-logic#lambda-calculus#type-theory#curry-howard#proof-theory#computation#normalization#interactive-labs 15
- Dependent Type Theory: Proofs, Data, and Universes How types came to express specifications that depend on values, and why equality, induction, and universe rules became foundational decisions. #history-of-logic#mathematical-logic#dependent-types#foundations-of-mathematics#proof-assistants#type-theory#identity-types#universes#inductive-types 16
- Categorical Logic: Structure, Quantification, and Internal Languages How categories provided structural interpretations of proof, function types, quantifiers, and mathematical foundations. #history-of-logic#mathematical-logic#categorical-logic#semantics#foundations-of-mathematics#category-theory#adjunctions#topos-theory#type-theory 17
- Functional Programming and Programming-Language Semantics From Lisp and lambda-based language design to mathematical accounts of recursion, polymorphic type inference, and abstraction. #history-of-logic#mathematical-logic#functional-programming#programming-languages#semantics#lambda-calculus#denotational-semantics#type-inference#domain-theory 18
- Automated Theorem Proving: Clauses, Unification, Equality, and Search How proof procedures turn a mathematical problem into a search, and why representation, inference rules, and search strategy each matter. #history-of-logic#mathematical-logic#automated-reasoning#resolution#theorem-proving#unification#equality#proof-search#first-order-logic 19
- Complexity, SAT, and SMT Why decidable reasoning can be difficult, how conflict-driven solvers exploit structure, and how Boolean search cooperates with mathematical theories. #history-of-logic#mathematical-logic#complexity#sat#smt#automated-reasoning#np-completeness#dpll#cdcl#decision-procedures#interactive-labs 20
- Logic Programming: Clauses as Programs How proof search can compute answers, and why a program's logical consequences must be distinguished from the behavior of its execution strategy. #history-of-logic#mathematical-logic#logic-programming#prolog#automated-reasoning#horn-clauses#sld-resolution#datalog#unification 21
- Proof Assistants: Foundations and Trust The distinct histories of Automath, LCF, Mizar, inductive provers, dependent-type systems, Metamath, and Lean—and what each architecture asks us to trust. #history-of-logic#mathematical-logic#proof-assistants#formalization#foundations-of-mathematics#type-theory#trusted-kernel#lean#lcf#coq 22
- Program Verification: Invariants, Semantics, and Local Reasoning How assertions became a logic of programs, and how proofs of loops, heap operations, compilers, and kernels depend on precise specifications. #history-of-logic#mathematical-logic#program-verification#hoare-logic#separation-logic#formal-methods#loop-invariants#weakest-preconditions#compiler-correctness 23
- Temporal Verification, Model Checking, and Abstraction How logics of time became tools for checking ongoing systems, and how symbolic representations and abstraction address the growth of possible behaviors. #history-of-logic#mathematical-logic#model-checking#temporal-logic#abstract-interpretation#formal-methods#safety-and-liveness#symbolic-verification#abstraction#interactive-labs 24
- Formalized Mathematics: Proofs and Reusable Libraries How mechanically checked mathematics grew from individual texts and landmark proofs into shared infrastructure for further mathematical work. #history-of-logic#mathematical-logic#formalized-mathematics#mathematical-libraries#proof-assistants#formalization#proof-reflection#mathlib#lean 25
- Homotopy Type Theory and Univalence How identity types acquired a geometric interpretation, why equivalence can induce identification, and how cubical theories address computation. #history-of-logic#mathematical-logic#homotopy-type-theory#univalence#foundations-of-mathematics#type-theory#dependent-types#identity-types#cubical-type-theory 26
- Learned Theorem Proving: Search, Formalization, and Discovery How statistical guidance works with formal checking, from premise selection to AlphaProof and research formalization, with careful distinctions about evidence and novelty. #history-of-logic#mathematical-logic#ai#theorem-proving#formalization#automated-reasoning#machine-learning#proof-search#autoformalization 27
History of Logic: Earlier Traditions 6 parts · Started 2026-09-05 #history-of-logic#history-of-philosophy#logical-consequence#medieval-logic#syllogistic-logic +31 more topics
- Greek and Late-Antique Logic Aristotelian demonstration, syllogistic inference, Stoic arguments, and the commentators and translators who shaped their later study. #history-of-logic#ancient-logic#aristotle#stoicism#history-of-philosophy#syllogistic-logic#propositional-logic#demonstration 01
- Arabic, Islamic, and Jewish Logical Traditions Translation, demonstration, Avicennan innovations, later teaching traditions, and the movement of logical ideas across Arabic, Hebrew, and Latin. #history-of-logic#arabic-logic#avicenna#medieval-logic#islamic-philosophy#jewish-philosophy#syllogistic-logic#translation 02
- Medieval Latin Logic: Reference, Consequence, and Paradox How medieval logicians analyzed the use of terms, the force of logical particles, valid consequences, and self-referential statements. #history-of-logic#medieval-logic#semantics#paradoxes#supposition-theory#logical-consequence#self-reference#history-of-philosophy 03
- Indian Logic: Inference, Evidence, and Analysis Nyāya, Buddhist theories of inference, and Navya-Nyāya's technical language, examined through the justification and failure of inferential signs. #history-of-logic#indian-logic#nyaya#buddhist-logic#epistemology#inference#navya-nyaya#history-of-philosophy 04
- Chinese Traditions of Argument: Names, Kinds, and Distinctions Mohist standards of reasoning, the School of Names, the white-horse discussion, and Xunzi's account of naming and orderly discourse. #history-of-logic#chinese-philosophy#mohism#argumentation#philosophy-of-language#analogy#school-of-names#history-of-philosophy 05
- Before Boole: Reform, Leibniz, and Bolzano Early-modern projects for improving inquiry and calculation, followed by Bolzano's account of propositions, variation, consequence, and explanation. #history-of-logic#early-modern-logic#leibniz#bolzano#induction#logical-consequence#symbolic-logic#history-of-philosophy 06