Notes / Series
History of Logic
Notes in this series, arranged in reading order.
#history-of-logic#mathematical-logic#foundations-of-mathematics#interactive-labs#proof-theoryAll 137 topics
Reading order
28 parts- 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 Part 0
- 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 Part 1
- 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 Part 2
- 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 Part 3
- 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 Part 4
- 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 Part 5
- 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 Part 6
- 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 Part 7
- 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 Part 8
- 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 Part 9
- 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 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 Part 27