Mathematical Logic

Covers statements, predicates, variables, scope, free and bound variables, and nested quantifiers. Practice focuses on writing definitions precisely and checking whether formal statements say what was intended.

Develops the mathematical structures used throughout logic: relations, functions, equivalence relations, partial orders, induction, and recursive definitions. Learners construct small examples and test their defining properties.

Presents direct proof, contradiction, contraposition, case analysis, induction, and counterexamples. Learners write proofs whose assumptions, steps, and conclusions can later be represented in formal systems.

Traces logic from Aristotle and the Stoics through Boole, Frege, Hilbert, Gödel, Turing, and modern formal methods. It connects major technical changes to foundational debates, computing, and machine-checked proof.

Defines propositional variables, logical connectives, formation rules, parse trees, and structural induction on formulas. Learners construct and analyze well-formed formulas without relying on ambiguous natural language.

Covers truth assignments, truth tables, satisfiability, validity, logical consequence, and semantic equivalence. Learners classify formulas and build countermodels to invalid arguments.

Introduces natural deduction, axiomatic systems, and formal derivations for propositional logic. Practice includes proving sequents and identifying the exact rule that licenses each step.

Proves soundness, completeness, consistency, and decidability for propositional systems. Learners separate claims made inside a formal system from metatheoretic claims about that system.

Connects formulas with Boolean algebras, normal forms, switching circuits, and functional completeness. Learners convert formulas to conjunctive and disjunctive normal forms and minimize small Boolean expressions.

Treats propositional satisfiability as both a logical problem and a computational task. Learners use DPLL, conflict-driven clause learning, watched literals, and modern SAT solvers to encode and solve constraint problems.

Defines constants, function symbols, predicate symbols, terms, atomic formulas, substitution, and variable capture. Learners design first-order languages for arithmetic, graphs, orders, and everyday rule systems.

Covers structures, interpretations, assignments, satisfaction, models, and semantic consequence. Learners evaluate formulas in finite structures and construct models or countermodels for quantified claims.

Develops natural deduction, Hilbert systems, and quantifier rules for first-order logic. Exercises emphasize safe substitution, eigenvariable conditions, equality reasoning, and formal derivations.

Establishes the relationship between formal derivability and semantic consequence. The chapter develops the Soundness and Completeness Theorems and shows how maximal consistent sets and term models support completeness proofs.

Studies the Compactness Theorem and the upward and downward Löwenheim–Skolem Theorems. Learners apply them to build nonstandard models, prove non-definability results, and recognize limits of first-order axiomatization.

Introduces theories, axiomatizations, elementary equivalence, elementary substructures, embeddings, diagrams, and test criteria such as Tarski–Vaught. Learners compare structures by the first-order sentences they satisfy.

Covers unification, substitution algorithms, Skolemization, Herbrand’s theorem, and resolution. Learners turn first-order formulas into clause form and build machine-oriented refutations.

Examines definability, quantifier elimination, model completeness, and decision procedures derived from normal forms. Case studies include dense linear orders, real closed fields, and Presburger arithmetic.

Introduces complete types, realized and omitted types, saturated models, and homogeneous models. Learners use types to describe possible elements and extensions that individual formulas cannot capture alone.

Covers categoricity, indiscernibles, stability, and the classification of first-order theories. The chapter shows how model theorists measure and control the diversity of models of an axiomatic theory.

Restricts model-theoretic questions to finite structures, where compactness and classical completeness techniques behave differently. Learners connect logical definability with database queries, games on structures, and computational complexity.

Connects logical languages with complexity classes through descriptive complexity. Learners use fragments of first-order and fixed-point logic to characterize computational resources and express graph properties.

Formalizes the natural numbers using Robinson arithmetic, Peano arithmetic, induction schemas, and definitions of arithmetic operations. Learners distinguish the standard natural numbers from nonstandard models of arithmetic.

Develops alphabets, strings, formal languages, Gödel numbering, and effective encodings of formulas and proofs. These tools make it possible for formal systems and machines to operate on descriptions of their own expressions.

Presents Turing machines, register machines, recursive functions, and the lambda calculus as models of effective computation. Learners implement small computations and compare the models through the Church–Turing thesis.

Covers decidable, recognizable, and noncomputable problems together with mapping and Turing reductions. Learners prove undecidability using diagonalization and reductions from the halting problem.

Introduces time and space complexity, tractability, nondeterminism, NP-completeness, and complexity reductions. Learners classify logical decision problems and analyze how representation affects computational cost.

Studies the arithmetical hierarchy, analytical hierarchy, Turing degrees, oracle computation, and relative computability. Learners classify sets by quantifier complexity and compare different degrees of unsolvability.

Develops representability, diagonalization, Gödel sentences, and the First and Second Incompleteness Theorems. It also separates incompleteness, undecidability, inconsistency, and ordinary limitations of a chosen axiom system.

Applies computability and incompleteness to arithmetic, group theory, first-order validity, and other formal theories. Learners use reductions and interpretability to show why no uniform decision method can settle every theory.

Represents proofs as trees of sequents and develops structural and logical inference rules. Learners construct derivations in classical and intuitionistic sequent calculi and track assumptions explicitly.

Studies proof reduction through normalization, cut elimination, subformula properties, and proof search. Learners simplify derivations and use structural results to establish consistency and decidability consequences.

Uses ordinal notation and transfinite induction to measure the strength of formal theories. The chapter develops consistency arguments and explains what proof-theoretic ordinals reveal about arithmetic systems.

Asks which axioms are required to prove ordinary mathematical theorems. Learners work with subsystems of second-order arithmetic and the major equivalence classes known as the Big Five.

Builds set theory from extensionality, pairing, union, power set, separation, replacement, foundation, and infinity. Learners derive standard constructions while tracking which ZF or ZFC axioms each argument uses.

Develops well-orders, transfinite induction, ordinal arithmetic, cardinality, and cardinal arithmetic. Learners compare infinite sizes and carry out recursive definitions across transfinite stages.

Studies equivalent forms of the Axiom of Choice, including well-ordering and Zorn’s Lemma. Applications and counterexamples show where choice enters algebra, analysis, topology, and infinite combinatorics.

Constructs Gödel’s universe of constructible sets and examines inner models. Learners see how relative consistency proofs organize the study of propositions that ordinary ZFC cannot decide.

Develops forcing through partial orders, names, generic filters, and forcing relations. The main applications are independence results such as the Continuum Hypothesis and the independence of selected combinatorial statements.

Introduces inaccessible, measurable, supercompact, and related large cardinals as measures of set-theoretic strength. It connects them with consistency strength, inner models, reflection principles, and the boundaries of current knowledge.

Studies infinite games, determinacy principles, and their consequences for definable sets of real numbers. Learners compare determinacy with choice and see how regularity properties depend on foundational assumptions.

Replaces unrestricted classical reasoning with proof-centered semantics and constructive existence. Learners work with intuitionistic natural deduction, Kripke semantics, Heyting algebras, and constructive counterexamples.

Connects propositions with types and proofs with programs through the Curry–Howard correspondence. Learners translate natural-deduction proofs into typed lambda terms and use normalization as computation.

Extends simple types with dependent functions, dependent pairs, inductive families, universes, and identity types. Learners encode specifications whose types carry precise mathematical guarantees.

Treats equality through paths, higher-dimensional structure, and the univalence principle. The chapter develops core ideas of homotopy type theory and shows how they change formal reasoning about equivalence.

Adds operators for necessity and possibility and studies systems such as K, T, S4, and S5. Learners use Kripke frames, correspondence results, and canonical models to test modal arguments.

Formalizes claims about time, state changes, actions, and programs. Learners work with linear and branching temporal logics, dynamic logic, transition systems, and temporal specifications.

Allows more than two truth values and examines degrees of truth, uncertainty, and vagueness. Learners compare finite-valued logics, infinite-valued systems, and fuzzy inference without confusing truth degree with probability.

Studies systems designed to reason without explosion or to require meaningful connections between premises and conclusions. Learners compare paraconsistent and relevance semantics with classical consequence.

Expresses logical systems through categories, functors, adjunctions, fibrations, and topoi. The chapter connects syntax and semantics at a structural level and relates categorical logic to type theory and geometry.

Turns declarative rules into executable searches using Horn clauses, backward chaining, and fixed-point semantics. Learners write small Prolog and Datalog programs and diagnose termination, ordering, and negation issues.

Develops concept languages, role restrictions, subsumption, and ontology reasoning. Learners model a small knowledge domain and run consistency and classification checks using description-logic principles.

Combines propositional search with decision procedures for arithmetic, arrays, bit vectors, equality, and other theories. Learners encode verification and planning problems for SMT solvers and interpret satisfying models and unsatisfiable cores.

Covers term indexing, proof search, equality reasoning, superposition, tableaux, and automated premise selection. Learners configure an automated prover, inspect generated proofs, and distinguish a timeout from a genuine counterexample.

Uses proof assistants to turn definitions, statements, and proofs into machine-checked artifacts. Learners formalize a small theorem in a modern dependent-type or higher-order system and manage libraries, tactics, and trusted kernels.

Applies temporal logic and state-space search to hardware, protocols, and concurrent systems. Learners specify invariants, run explicit or symbolic model checking, analyze counterexample traces, and address state explosion.

Connects logical specifications with program correctness through Hoare logic, weakest preconditions, contracts, refinement, and separation logic. Learners verify a small program and document the assumptions that make its proof valid.

Covers large shared theorem libraries, reproducible builds, proof maintenance, and collaborative review. Learners contribute a reusable formal result and handle dependencies, naming, documentation, and changes to upstream libraries.

Examines neural premise selection, proof generation, autoformalization, reinforcement-guided search, and language-model assistance. Learners evaluate generated steps with a trusted checker and identify failure modes such as invalid translation, hidden assumptions, and benchmark leakage.

Follows a real task from an informal claim through language design, axioms, model selection, proof or solver choice, validation, and communication of results. Learners deliver a checked argument together with counterexample tests, tool output, assumptions, and limitations.

Maps routes into mathematical research, theoretical computer science, formal verification, solver engineering, knowledge representation, and formalized mathematics. It covers portfolio artifacts, graduate-study expectations, relevant certifications where applicable, open-source contribution paths, conferences, journals, and reliable ways to track new results.