A Gentle Introduction to Modern Model Theory
summary
Modern model theory makes a concrete claim: separate theory from model and split algebraic vs geometric theories, and category theory need not rest on set theory. Examples include a worked monoid example, a Euclidean construction that models Peano arithmetic, and the Goodstein sequence termination shown to require set theory rather than Peano proofs. For lambda calculus the concrete modeling tool is Scott's G∞ (continuous function universe), and larger foundational moves use a Grothendieck universe to embed ZF‑style theories.
AI-written summary · about
chapters (13)
- 0:00Introduction and background
- 1:22The nature of theories
- 2:45Formalizing monoids
- 5:46Partial orders and geometry
- 9:02Axioms and equational theory
- 12:25Set and category theory
- 17:26Theorems and completeness
- 21:30Algebraic vs geometric
- 26:17Models of theories
- 30:12Modeling in set theory
- 35:04The expression problem
- 38:22Lambda calculus modeling
- 42:37Conclusion and Q&A
related talks
53mIntroduction to Intuitionistic Type Theory
02h 24mCategory Theory Track
20mFully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logica
27mFunctorial Semantics for Partial Theories
30mDisplayed Monoidal Categories for the Semantics of Linear Logic
52mType Theory and its Meaning Explanations
23mImplementing a category-theoretic framework for typed abstract syntax
12mA Unified View of Modalities in Type Systems