10.5 Equivalence of Models
Detailed equivalence proofs between Turing machines, recursive functions, and lambda calculus, with explicit constructions and simulations.
Tag
Logic
120 notes
10.2 Partial vs Total Functions
Distinction between partial and total computable functions, undefined values, domains of definition, and the role of nontermination.
10.1 Recursive Functions
Primitive recursive functions, general recursive functions, minimization, and the formal construction of computable numerical functions.
9.2 Large Cardinals
An introduction to large cardinal axioms, inaccessible cardinals, measurable cardinals, elementary embeddings, and consistency strength.
9.1 Forcing
An introduction to forcing, generic filters, forcing names, the forcing relation, and the basic extension theorem.
8.3 Constructible Universe (L)
The constructible universe, definable subsets, the hierarchy L_alpha, and the axiom of constructibility.
8.2 Equivalent Formulations
Equivalent forms of the axiom of choice, including Zorn's lemma, the well ordering theorem, maximal principles, and right inverses of surjections.
8.1 Axiom of Choice
The axiom of choice, choice functions, indexed families, and first consequences in axiomatic set theory.
7.4 Arithmetic of Cardinals
Cardinal addition, multiplication, exponentiation, finite and infinite cardinal arithmetic, and basic comparison laws.
7.1 Sets, Relations, Functions
Basic set theoretic language, including sets, membership, subsets, operations, relations, equivalence relations, order relations, and functions.
6.2 Types and Realizations
Definition of complete and partial types, realization of types in structures, examples, consistency, and basic properties.
4.4 Isomorphism and Invariants
Isomorphisms of first order structures, structural invariants, and properties preserved by isomorphism.
4.2 Substructures and Embeddings
Substructures, generated substructures, homomorphisms, embeddings, and preservation of atomic formulas.
14.3 Second Incompleteness Theorem
Proof that no sufficiently strong consistent system can prove its own consistency.
14.1 Arithmetization of Syntax
Encoding symbols, formulas, and proofs as natural numbers to allow arithmetic to reason about its own syntax.
Preface
Overview of mathematical logic, its scope, and the structure of the book.
Chapter 24. Limits of Formal Systems
Incompleteness, undecidability, independence, practical implications, and future directions in logic and foundations.
Chapter 22. Foundations Programs
Logicism, formalism, intuitionism, structuralism, and modern perspectives on the foundations of mathematics.
Chapter 22. Foundations Programs
Logicism, formalism, intuitionism, structuralism, and modern perspectives on the foundations of mathematics.
Chapter 20. Logic in Programming
Logic programming, type systems, verification, model checking, and program synthesis.
Chapter 20. Logic in Programming
Logic programming, type systems, verification, model checking, and program synthesis.
Chapter 19. Formal Languages
Grammars, syntax, automata theory, regular and context free languages, parsing, recognition, and applications in compilers.
Chapter 17. Type Theory
Simple type theory, dependent types, Curry-Howard correspondence, proof assistants, and formalized mathematics.
Chapter 17. Type Theory
Simple type theory, dependent types, Curry-Howard correspondence, proof assistants, and formalized mathematics.
Chapter 16. Intuitionistic Logic
Constructive semantics, proof interpretation, differences from classical logic, Kripke models, and applications in computation.
Chapter 15. Ordinal Analysis
Proof theoretic ordinals, transfinite induction, strength of theories, applications to arithmetic, and limits of formal strength.
14.5 Extensions and Refinements
Stronger forms of incompleteness, Rosser’s improvement, Löb’s theorem, and connections to computability.
14.4 Implications for Formal Systems
Consequences of incompleteness for truth, provability, independence, and the structure of formal systems.
14.2 First Incompleteness Theorem
Construction of a true but unprovable statement using diagonalization and self-reference.
Chapter 14. Godel Theorems
Arithmetization of syntax, the first and second incompleteness theorems, implications for formal systems, and refinements.
13.5 Proof Length and Complexity
Quantitative study of proofs, including proof size, efficiency, and connections to computational complexity.
13.4 Consistency Proofs
Methods for proving consistency of formal systems, including syntactic and semantic approaches.
13.3 Normal Forms
Normalization of proofs, elimination of detours, and structural simplification of derivations.
13.2 Derivability
Formal notion of deriving formulas from assumptions, including structural properties and inference behavior.
13.1 Syntax of Proofs
Formal structure of proofs, including derivations, inference rules, axioms, and proof representations.
Chapter 13. Formal Proof Systems
Syntax of proofs, derivability, normal forms, consistency proofs, proof length, and proof complexity.
12.5 Structure of Degrees
Global properties of the Turing degrees including incomparability, density, and jump structure.
Chapter 12. Degrees of Unsolvability
Reducibility, Turing degrees, recursively enumerable sets, Post's problem, and the structure of degrees.
11.5 Undecidability Results
Extensions of undecidability using reductions and general results such as Rice’s theorem.
11.4 Halting Problem
The undecidable problem of determining whether a Turing machine halts on a given input.
Chapter 11. Turing Machines
Turing machine definitions, computation traces, universal machines, the halting problem, and undecidability results.
10.4 Formal Models of Computation
Turing machines, register machines, lambda calculus, recursive functions, and the precise mathematical models used to define computation.
10.3 Church Turing Thesis
The Church Turing thesis, formal models of computation, equivalence of models, and the distinction between mathematical theorem and foundational principle.
Chapter 10. Computable Functions
Recursive functions, partial and total functions, the Church-Turing thesis, formal models of computation, and equivalence of models.
9.5 Applications in Analysis and Topology
Applications of advanced set theory to analysis and topology, including regularity properties, Banach spaces, measure theory, and topological classification.
9.4 Determinacy Principles
An introduction to infinite games, determined games, the axiom of determinacy, projective determinacy, and consequences for sets of reals.
9.3 Descriptive Set Theory
An introduction to Polish spaces, Borel sets, analytic sets, projective sets, regularity properties, and the role of definability in set theory.
Chapter 9. Advanced Set Theory
Forcing, large cardinals, descriptive set theory, determinacy principles, and applications in analysis and topology.
8.5 Independence Phenomena
Independence results in set theory, including the axiom of choice and the continuum hypothesis, and the methods used to establish independence.
8.4 Consistency Results
Relative consistency, inner models, constructibility, and the role of consistency results in axiomatic set theory.
Chapter 8. Axiomatic Systems
Axiom of Choice, equivalent formulations, constructible universe, consistency results, and independence phenomena.
7.5 Zermelo Fraenkel Axioms (ZF, ZFC)
The axioms of Zermelo Fraenkel set theory, the role of choice, and the use of axioms as a foundation for mathematics.
7.3 Ordinals and Well Ordering
Well ordered sets, order isomorphisms, ordinals, successor ordinals, limit ordinals, and transfinite induction.
7.2 Cardinality and Countability
Cardinality, finite and infinite sets, countable sets, uncountable sets, and Cantor diagonal arguments.
Chapter 7. Basic Set Theory
Basic set theoretic notions including sets, relations, functions, cardinality, ordinals, well ordering, cardinal arithmetic, and the ZF and ZFC axioms.
6.5 Classification Programs
Detailed overview of classification theory, dividing lines such as stability, simplicity, and NIP, and the structural analysis of first order theories.
6.4 Stability Theory Overview
Detailed introduction to stability theory, counting types, order property, definability of types, and structural consequences.
6.3 Saturated Models
Saturated models, realization of types, and their role in controlling definability and extensions.
6.1 Definable Sets and Functions
Definition of definable sets and functions in first order structures, with parameters, examples, closure properties, and proofs.
Chapter 6. Definability and Types
Definable sets, definable functions, types, realizations, saturated models, stability theory, and classification programs.
5.5 Limitations of First Order Logic
Expressive limitations of first order logic, including inexpressibility of finiteness and categoricity issues.
5.4 Nonstandard Models
Construction and properties of nonstandard models using compactness and Lowenheim Skolem.
5.3 Applications to Algebra
Applications of compactness and Lowenheim Skolem to algebraic structures and existence results.
5.2 Lowenheim Skolem Theorems
Downward and upward Lowenheim Skolem theorems and their consequences for model sizes in first order logic.
5.1 Compactness Theorem
Detailed development of the compactness theorem, its proof via completeness, and fundamental applications in model theory.
Chapter 5. Compactness and Completeness
Compactness, completeness, Lowenheim-Skolem theorems, nonstandard models, and limitations of first order logic.
4.5 Examples Across Algebra and Geometry
Examples of first order structures from algebra, order theory, graph theory, and geometry.
4.3 Elementary Equivalence
Elementary equivalence, theories of structures, and preservation of first order sentences.
4.1 Languages and Signatures
Formal languages, signatures, and symbols used to describe structures in first order logic.
Chapter 4. Structures and Models
Basic model theoretic notions including languages, signatures, substructures, embeddings, elementary equivalence, isomorphism, and examples.
3.5 Cut Elimination
The cut rule, its elimination, and consequences for consistency and normalization.
3.4 Proof Transformations
Transformations of proofs, normalization, and structural properties of derivations.
3.3 Hilbert Systems
Hilbert style proof systems, axioms, and derivations using a minimal set of inference rules.
3.2 Sequent Calculus
Sequents, structural rules, and introduction rules for logical connectives in the sequent calculus.
3.1 Natural Deduction
Introduction to natural deduction, inference rules, and structured proofs for propositional logic.
Chapter 3. Proof Systems
Formal systems for deriving logical conclusions including natural deduction, sequent calculus, Hilbert systems, and proof transformations.
2.25 Common Proof Mistakes and Debugging
Lean proofs fail in predictable ways.
2.24 Simplification and Automation
Lean provides automation to reduce routine proof steps.
2.23 Rewriting Strategies
Rewriting with equality is one of the most frequent operations in Lean.
2.22 Backward Reasoning
Backward reasoning starts from the goal and reduces it to simpler subgoals.
2.21 Forward Reasoning
Forward reasoning starts from the assumptions in the local context and derives new facts until the goal becomes immediate.
2.20 Using Assumptions Effectively
An assumption is a local term that Lean may use to solve the current goal or produce another proof.
2.19 Local Context Management
The local context is the list of variables, hypotheses, instances, and intermediate facts available at a point in a proof.
2.18 Naming Conventions
Names in Lean carry meaning.
2.17 Proof Structuring Patterns
A Lean proof should expose the shape of the argument.
2.16 Introduction and Elimination Rules
Every logical connective in Lean has two sides.
2.15 Case Analysis
Case analysis is the proof pattern for using data that has more than one possible constructor.
2.14 Proof by Contradiction
Proof by contradiction is a classical proof pattern.
2.13 Classical vs Constructive Logic
Lean is constructive by default.
2.12 Universal Quantifiers
A universal statement asserts that a property holds for every element of a type.
2.11 Existential Quantifiers
An existential statement says that some object exists with a given property.
2.10 Symmetry and Transitivity
Equality supports two structural operations: reversing direction (symmetry) and chaining steps (transitivity).
2.9 Rewriting with Equality
Rewriting is the main way to use equality in Lean.
2.8 Equality Basics
Equality expresses that two terms are identical.
2.7 True and Trivial Proofs
`True` is the proposition that always has a proof.
2.6 False and Contradiction
`False` is the proposition with no constructors.
2.5 Examples Across Fields
How truth, provability, consistency, completeness, and independence appear across major branches of mathematics.
2.5 Validity and Entailment
Validity, semantic entailment, satisfiability, countermodels, and logical consequence in first order logic.
2.5 Negation
Negation represents "not".
2.4 Independence Phenomena
Statements that cannot be proved or refuted from a chosen axiom system, and what independence means in mathematical practice.
2.4 Satisfaction and Models
Satisfaction, truth in a structure, models of sentences, and theories in first order logic.
2.4 Disjunction
Disjunction represents "or".
2.3 Consistency and Completeness
Core meta-properties of formal systems: avoiding contradiction and deciding statements.
2.3 Structures and Interpretations
Structures, domains, and interpretations of symbols in first order logic.
2.3 Conjunction
Conjunction represents "and".
2.2 Formal Systems and Semantics
Syntax, axioms, inference rules, and the semantic interpretation of mathematical languages.
2.2 Quantifiers and Scope
Universal and existential quantifiers, scope, free variables, bound variables, and variable capture.
2.2 Implication and Functions
Implication is the first logical connective to understand in Lean because it is also the ordinary function type.
2.1 Truth vs Provability
Distinction between semantic truth and syntactic provability, with examples and limits.
2.1 Terms, Predicates, Formulas
Syntax of first order logic including terms, predicate symbols, and the formation of formulas.
2.1 Propositions as Types
Lean identifies propositions with types and proofs with terms.
Chapter 2. Mathematical Truth
Overview of truth, provability, formal systems, and independence in mathematics.
Chapter 2. First-Order Logic
Extension of propositional logic with terms, predicates, quantifiers, structures, satisfaction, models, validity, and entailment.
1.5 Soundness and Completeness
Soundness, completeness, and the relationship between semantic validity and formal provability.
1.4 Normal Forms
Conjunctive normal form, disjunctive normal form, and systematic conversion of propositional formulas.
1.3 Logical Equivalence
Logical equivalence, truth preserving transformations, and basic laws for rewriting propositional formulas.
1.2 Semantics: Truth Tables
Truth values, valuations, and evaluation of propositional formulas using truth tables.
1.1 Syntax: Variables, Connectives
Definition of propositional variables, logical connectives, and formation rules for well formed formulas.
Chapter 1. Propositional Logic
Foundations of propositional logic including syntax, semantics, equivalence, normal forms, and proof systems.
03. Logic and Foundations
Formal logic, set theory, computability, and the foundations of mathematics treated as a formal system.