Advanced Topics: Logic

These specialization tracks are designed for independent learners who have mastered the Core Undergraduate Curriculum in formal logic, proof systems, and introductory metatheory. You are expected to choose one or two tracks aligned with your specific intellectual interests or technical applications, rather than completing every track.

Mathematical Logic & Foundational Systems

Explores advanced pure logic through mathematical structures, relative consistency proofs, axiomatic calibration of mathematical theorems, and generalized computability.

Model Theory: Model Theory: An Introduction (David Marker / Springer) - Explores definable sets, quantifier elimination, type spaces, and Morley's categorization theorem, bridging formal logic with abstract algebra.

Axiomatic Set Theory & Independence: Set Theory (Kenneth Kunen / College Publications) - Develops combinatorial set theory, Martin's axiom, Gödel's constructible universe, and Cohen forcing to establish the independence of the Continuum Hypothesis.

Proof Theory & Reverse Mathematics: Subsystems of Second Order Arithmetic (Stephen G. Simpson / Cambridge University Press) - Analyzes the exact axiomatic strength necessary to prove core theorems across analysis, algebra, and topology using the Big Five subsystems of second-order arithmetic.

Computability & Degree Theory: Turing Computability: Theory and Applications (Robert I. Soare / Springer) - Investigates relative computability, the lattice of computably enumerable sets, finite and infinite injury priority arguments, and the structural complexity of Turing degrees.

Philosophical Logic & Non-Classical Logics

Investigates formal deductive systems that depart from classical truth conditions, modeling modalities, constructive proof requirements, information sensitivity, and rational multi-agent interaction.

Modal Logic & Relational Semantics: Boxes and Diamonds: An Open Introduction to Modal Logic (Richard Zach / Open Logic Project) - An open-access textbook covering propositional modal systems, Kripke relational semantics, frame correspondence theory, and Henkin-style completeness proofs.

Modal Logic & Relational Semantics: Modal Logic (MIT OpenCourseWare / Stephen Yablo) - Complementary university course providing advanced lecture notes and problem sets on possible-world semantics, modal predicate logic, and counterpart theory.

Intuitionistic & Constructive Logic: Elements of Intuitionism (Michael Dummett / Oxford University Press) - The definitive philosophical and logical treatise analyzing the rejection of the principle of excluded middle, proof-conditional semantics, and constructive analysis.

Many-Valued & Substructural Logics: An Introduction to Non-Classical Logic: From If to Is (Graham Priest / Cambridge University Press) - A unified, tableau-driven presentation of many-valued logics, paraconsistency, relevance logics, and conditional logics for philosophical analysis.

Epistemic & Multi-Agent Logic: Reasoning About Knowledge (Ronald Fagin, Joseph Y. Halpern, Yoram Moses, & Moshe Y. Vardi / MIT Press) - The canonical interdisciplinary text establishing modal epistemic logics, common knowledge, distributed protocols, and multi-agent information update.

Computational Logic, Automated Reasoning & Verification

Focuses on the algorithmic automation of logical reasoning, automated satisfiability decision procedures, formal hardware and software verification, and declarative problem-solving.

Automated Reasoning & Decision Procedures: Automated Reasoning: Satisfiability (Coursera / Eindhoven University of Technology) - An interactive MOOC covering practical algorithmic solving, including resolution, the CDCL framework, simplex for linear inequalities, and SMT encoding.

Automated Reasoning & Decision Procedures: Decision Procedures: An Algorithmic Point of View (Daniel Kroening & Ofer Strichman / Springer) - A textbook companion detailing the underlying theory of Nelson-Oppen theory combinations, equality with uninterpreted functions, and bit-vector decision algorithms.

Temporal Logic & Model Checking: Principles of Model Checking (Christel Baier & Joost-Pieter Katoen / MIT Press) - The comprehensive standard text covering transition systems, omega-automata, LTL, CTL, fairness constraints, and probabilistic verification algorithms.

Interactive Theorem Proving: Software Foundations (University of Pennsylvania / Benjamin C. Pierce et al.) - An open-access, machine-checked course series that teaches functional programming, formal logic, and software verification using the Coq/Rocq proof assistant.

Logic Programming & Answer Set Solving: Answer Set Solving in Practice (Martin Gebser, Roland Kaminski, Benjamin Kaufmann, & Torsten Schaub / Springer) - Examines declarative problem-solving under stable model semantics, covering language constructs, non-monotonic reasoning, and Boolean constraint solving algorithms.

Categorical Logic, Type Theory & Formal Foundations

Unifies structural algebra, type systems, topos theory, and univalent homotopy foundations to articulate modern structural alternatives to traditional set-theoretic foundations.

Category Theory for Logicians: Category Theory (Steve Awodey / Oxford University Press) - Introduces categories, functors, natural transformations, limits, and adjoints, emphasizing connections to logic, universal algebra, and cartesian closed categories.

Type Theory & Lambda Calculi: Types and Programming Languages (Benjamin C. Pierce / MIT Press) - A systematic exposition of typed lambda calculi, operational semantics, subtyping, and the Curry-Howard correspondence relating propositions to types and proofs to programs.

Categorical Logic & Topos Theory: Topoi: The Categorial Analysis of Logic (Robert Goldblatt / Dover Publications) - An accessible introduction to elementary toposes as generalized universes of sets endowed with internal intuitionistic logic, connecting category theory with model theory.

Homotopy Type Theory & Univalent Foundations: Homotopy Type Theory: Univalent Foundations of Mathematics (The Univalent Foundations Program / Institute for Advanced Study) - The foundational open-access text establishing the synthesis of intensional type theory, higher category theory, and abstract homotopy theory via the Univalence Axiom.