Ma6/106c Spring 2026: Logic
Caltech, Linde Hall Room 187, Tuesday-Thursday 1:00-2:30 pm; the TA for the class is Edward Hou
Instructor:
Matilde Marcolli
This class provides a general introduction to mathematical logic. The content of the class is being revised (compared to previous years) so it is currently in an "experimental phase": the usual material previously covered in Ma6c will be included (propositional and first order logic and computability) and additional complementary topics will be added at the discretion of the instructor. The class is offered Letter Grade with the option of Pass/Fail. The students workload will consist of completeing an assigned number of homework problems and preparing a final presentation on a topic of choice selected from the reading material posted on this page. Homework policy: collaboration (exclusively with human collaborators who are registered students in this same class) is allowed and strongly encouraged, but solutions should then be written up individually.
Slides of Lectures
Slides of lectures will be posted here as the class progresses
Summary of lectures
- Tuesday March 31: Boolean semiring, propositional variables and connectives, well formed formulae, Boolean valuations, satisfiability and logical implication, De Morgan laws, Boolean functions and formulae, Boolean functions and circuits, logic gates, complete sets of gates, truth-functions analysis of propositional logic, Boolean algebras, concrete Boolean algebras and set theoretic operations, syntax and semantics of propositional logic, axioms and satisfiability, logical equivalence, deduction on clauses, deduction and logical implication.
- Thursday April 2: logical equivalence and the Lindenbaum algebra of a theory, truth functions and Boolean homomorphisms, Boolean atoms and truth functions, characteristic function and Boolean atoms, truth functions and atoms of the Lindenbaum Boolean algebra, Hilbert proof system, deduction trees, soundness of the Hilbert proof system, completeness of the Hilbert proof system.
- Tuesday April 7: Godel compactness theorem, infinite branching in trees and compactness, intuitionistic propositional logic, Heyting algebras, pseudocomplement, complementation, change to De Morgan laws, topological spaces, interior and closure, topolgical semantics of intuitionistic logic, examples, proof system for intuitionistic logic, intermediate logics.
- Thursday April 9: Modal logic: modal systems, Kripke many world semantics, accessibility, frames, forcing, validity, system K, some other modal systems and properties of the accessibility relation, proof systems axioms and inference rules, derived rules, soundness and completeness of the K-system, topological semantics of the S4 modal logic, Godel translation (intuitionistic and S4 modal logic), polyhedral semantics
- Tuesday April 14: First order logic: structures, first order language, terms, well formed formulae, parse trees, quantifiers and scope, bound and free variables, structures and semantic interpretation, structures and models, validity and satisfiability, tautologies, substitution
- Thursday April 16: definability, definable relations, definable functions, quantifiers and projection, examples of definability, definability with parameters, top-down and bottom-up description of structures, quantifier elimination and model completeness, examples, semialgebraic sets, isomorphism of structures and non-definability criterion, theories, theory of partial orders, difference between first and second order logic (example of well-ordered sets)
- Tuesday April 21:
- Thursday April 23:
- Tuesday April 28:
- Thursday April 30:
- Tuesday May 5:
- Thursday May 7:
- Tuesday May 12:
- Thursday May 14:
- Tuesday May 19: cancelled due to travel
- Thursday May 21:
- Tuesday May 26:
- Thursday May 28:
- Tuesday June 2: students presentations (room and schedule to be announced)
- Thursday June 4: students presentations (room and schedule to be announced)
Reading Materials
There is no specific textbook for the class. Some suggested
reading material will be posted here.
Books
- pdf Yuri I.Manin, "Logic for Mathematicians"
- pdf I.Moerdijk, J.van Oosten, "Sets, Models and Proofs"
Some sets of lecture notes
- pdf Lou van den Dries, "Mathematical Logic Lecture Notes"
- pdf T.Streicher, "Introduction to Category Theory and Categorical Logic"
- pdf Jean Gallier and Jocelyn Quaintance, "Proofs, Computability, Undecidability, Complexity, And the Lambda Calculus. An Introduction"
- pdf Mario Román García, "Category Theory and Lambda Calculus"
Papers (more material will be added here as the class progresses):
- pdf F.W.Lawvere, "An elementary theory of the category of sets"
- pdf F.W.Lawvere, "Diagonal Arguments and Cartesian Closed Categories"
- pdf S.A.Kurtz, "A Brief Introduction to the Intuitionistic Propositional Calculus"
- pdf D.Trufas, "Intuitionistic Propositional Logic in Lean"
- pdf
S. Adam-Day, N. Bezhanishvili, D. Gabelaia V. Marra, "The Intermediate Logic of Convex Polyhedra"
- pdf B.M.Bumpus, Z.A.Kocsis, "Degree of satisfieability in Heyting Algebras"
- pdf C.Lutz "Modal Logics for Computer Science"
- pdf
M.E.Coniglio, L.Prieto-Sanabria, "Modal logic S4 as a paraconsistent logic with a topological semantics"
- pdf
I. Garcia-Contreras, V.K.H. Govind, S Shoham, A Gurfinkel "Fast Approximations of Quantifier Elimination"
- pdf Ta Le Loi, "An Introduction to Semialgebraic Sets"
- pdf A Ghorbani, "The tame geometry of o-minimal structures"
- pdf C.Miller "Notes on tameness in model-theoretic structures"
- pdf N.S.Yanofsky, "A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points"
- pdf R.Diaconescu, "Axiom of choice and complementation"
- pdf H.Smessaert and L.Demey, "Visualizing the Boolean algebra B4 in 3D"
- pdf F.Pfennig, "A proof of the Curch-Rosser theorem and its representation in a logical framework"
- pdf A.Church, "An unsolvable problem of elementary number theory"
- pdf B.M.Bumpus, Z.A.Kocsis, "Degree of satisfiability in a Heyting algebra"
- pdf C.L.Mahany, "Elementary Topos theory and intuitionistic logic"
- pdf T.Leinster, "Rethinking set theory"
- pdf I.Tabakow, "An Introduction to Fuzzy Propositional Calculus Using Proofs from Assumptions"
- pdf A.Citkin, "An Algebraic Proof of the Nishimura Theorem"
- pdf A.Smith, "Universality of Wolfram's 2,3 Turing machine"
- pdf Yu.Rogozhin, "Small universal Turing machines"
- pdf E.Thormarker, "Chaitin's incompleteness theorem"
- pdf David O. Zisselman, "A proof of Goedel's incompleteness theorems using Chaitin's incompleteness theorem"
- pdf Raymond Hoofman, Harold Schelinx, "Models of the untypes lambda-calculus in semi Cartesian closed categories"
- pdf G.Manzonetto, "Models and theories of lambda-calculus"
- pdf A.M.Turing, "Computability and Lambda-definability"
- pdf F.W.Lawvere, "Functorial Semantics of Algebraic Theories"
- pdf R.A.G Seely, "Locally cartesian closed categories and type theory"
- pdf M. Hofmann, "On the Interpretation of Type Theory in Locally Cartesian Closed Categories"
- pdf S.Awodey, F.Rabe, "Kripke semantics for Martin-Lof extensional type theory
- pdf F.Lamarche, "Modeling Martin-Lof type theory in categories"
- pdf M.Lennon-Bertrand et al. "Martin-Lof a la Coq"
- pdf C.Williams, M.Stay, "Native type theory"
- pdf J.M.E.Hyland, "The effective topos"
- pdf A.Bauer et al. "The HoTT LIbrary. A formalization of homotopy type theory in Coq"
- pdf Floris van Doorn, Jakob von Raumer, and Ulrik Buchholtz, "Homotopy Type Theory in Lean"
- pdf Emily Riehl, "On the infty-topos semantics of homotopy tyep theory"
- pdf S.Awodey, "Type theory and homotopy"