Formal logic, set theory, computability, and the foundations of mathematics treated as a formal system.
This volume develops formal logic, set theory, computability, and the foundations of mathematics in a unified way, where syntax, semantics, proof, and computation are treated as precise mathematical objects.
Part I. Propositional and First-Order Logic
Chapter 1. Propositional Logic
This chapter introduces the basic language of propositional logic, its semantics, equivalence laws, normal forms, and the relation between proof and truth.
- 1.1 Syntax: Variables, Connectives
- 1.2 Semantics: Truth Tables
- 1.3 Logical Equivalence
- 1.4 Normal Forms
- 1.5 Soundness and Completeness
Chapter 2. First-Order Logic
This chapter extends propositional logic by introducing terms, predicates, quantifiers, and structures for interpreting mathematical statements.
- 2.1 Terms, Predicates, Formulas
- 2.2 Quantifiers and Scope
- 2.3 Structures and Interpretations
- 2.4 Satisfaction and Models
- 2.5 Validity and Entailment
Chapter 3. Proof Systems
This chapter studies formal systems for deriving conclusions, including natural deduction, sequent calculus, and Hilbert systems.
- 3.1 Natural Deduction
- 3.2 Sequent Calculus
- 3.3 Hilbert Systems
- 3.4 Proof Transformations
- 3.5 Cut Elimination
Part II. Model Theory
Chapter 4. Structures and Models
This chapter introduces formal structures, interpretations of languages, and methods for comparing mathematical models.
- 4.1 Languages and Signatures
- 4.2 Substructures and Embeddings
- 4.3 Elementary Equivalence
- 4.4 Isomorphism and Invariants
- 4.5 Examples Across Algebra and Geometry
Chapter 5. Compactness and Completeness
This chapter develops compactness, completeness, and model existence results, together with their applications.
- 5.1 Compactness Theorem
- 5.2 Lowenheim Skolem Theorems
- 5.3 Applications to Algebra
- 5.4 Nonstandard Models
- 5.5 Limitations of First Order Logic
Chapter 6. Definability and Types
This chapter studies definable sets, types, saturation, and the beginnings of classification theory.
- 6.1 Definable Sets and Functions
- 6.2 Types and Realizations
- 6.3 Saturated Models
- 6.4 Stability Theory Overview
- 6.5 Classification Programs
Part III. Set Theory
Chapter 7. Basic Set Theory
This chapter introduces sets, relations, functions, cardinality, ordinals, and the basic axioms of set theory.
- 7.1 Sets, Relations, Functions
- 7.2 Cardinality and Countability
- 7.3 Ordinals and Well Ordering
- 7.4 Arithmetic of Cardinals
- 7.5 Zermelo Fraenkel Axioms
Chapter 8. Axiomatic Systems
This chapter studies the Axiom of Choice, equivalent principles, constructibility, and independence results.
- 8.1 Axiom of Choice
- 8.2 Equivalent Formulations
- 8.3 Constructible Universe
- 8.4 Consistency Results
- 8.5 Independence Phenomena
Chapter 9. Advanced Set Theory
This chapter introduces forcing, large cardinals, descriptive set theory, and advanced applications.
- 9.1 Forcing
- 9.2 Large Cardinals
- 9.3 Descriptive Set Theory
- 9.4 Determinacy Principles
- 9.5 Applications in Analysis and Topology
Part IV. Computability Theory
Chapter 10. Computable Functions
This chapter develops formal notions of computation, recursive functions, and equivalent computational models.
- 10.1 Recursive Functions
- 10.2 Partial and Total Functions
- 10.3 Church Turing Thesis
- 10.4 Formal Models of Computation
- 10.5 Equivalence of Models
Chapter 11. Turing Machines
This chapter presents Turing machines, universal computation, and undecidability results.
- 11.1 Machine Definitions
- 11.2 Computation Traces
- 11.3 Universal Machines
- 11.4 Halting Problem
- 11.5 Undecidability Results
Chapter 12. Degrees of Unsolvability
This chapter compares undecidable problems using reducibility and studies the structure of Turing degrees.
- 12.1 Reducibility
- 12.2 Turing Degrees
- 12.3 Recursively Enumerable Sets
- 12.4 Posts Problem
- 12.5 Structure of Degrees
Part V. Proof Theory
Chapter 13. Formal Proof Systems
This chapter studies proofs as formal objects, including derivations, normalization, and complexity.
- 13.1 Syntax of Proofs
- 13.2 Derivability
- 13.3 Normal Forms
- 13.4 Consistency Proofs
- 13.5 Proof Length and Complexity
Chapter 14. Godel Theorems
This chapter presents the incompleteness theorems and their consequences for formal systems.
- 14.1 Arithmetization of Syntax
- 14.2 First Incompleteness Theorem
- 14.3 Second Incompleteness Theorem
- 14.4 Implications for Formal Systems
- 14.5 Extensions and Refinements
Chapter 15. Ordinal Analysis
This chapter studies the strength of theories using ordinals and transfinite methods.
- 15.1 Proof Theoretic Ordinals
- 15.2 Transfinite Induction
- 15.3 Strength of Theories
- 15.4 Applications to Arithmetic
- 15.5 Limits of Formal Strength
Part VI. Type Theory and Constructive Logic
Chapter 16. Intuitionistic Logic
This chapter develops constructive logic, proof interpretation, and Kripke semantics.
- 16.1 Constructive Semantics
- 16.2 Proof Interpretation
- 16.3 Differences from Classical Logic
- 16.4 Kripke Models
- 16.5 Applications in Computation
Chapter 17. Type Theory
This chapter introduces type systems, dependent types, and the connection between proofs and programs.
- 17.1 Simple Type Theory
- 17.2 Dependent Types
- 17.3 Curry Howard Correspondence
- 17.4 Proof Assistants
- 17.5 Formalized Mathematics
Chapter 18. Homotopy Type Theory
This chapter presents types as spaces, equality as paths, and the univalence principle.
- 18.1 Types as Spaces
- 18.2 Equality as Paths
- 18.3 Univalence Principle
- 18.4 Higher Structures
- 18.5 Foundations Perspective
Part VII. Logic and Computer Science
Chapter 19. Formal Languages
This chapter studies grammars, automata, and language recognition.
- 19.1 Grammars and Syntax
- 19.2 Automata Theory
- 19.3 Regular and Context Free Languages
- 19.4 Parsing and Recognition
- 19.5 Applications in Compilers
Chapter 20. Logic in Programming
This chapter studies the role of logic in programming languages, verification, and synthesis.
Chapter 21. Complexity Theory
This chapter studies computational complexity, reductions, and limits of efficient computation.
- 21.1 Time and Space Complexity
- 21.2 Complexity Classes
- 21.3 Reductions and Completeness
- 21.4 Limits of Efficient Computation
- 21.5 Open Problems
Part VIII. Foundations of Mathematics
Chapter 22. Foundations Programs
This chapter surveys major foundational views such as logicism, formalism, and intuitionism.
Chapter 23. Philosophy and Interpretation
This chapter studies truth, existence, and the interpretation of formal systems.
- 23.1 Meaning of Truth
- 23.2 Mathematical Existence
- 23.3 Platonism vs Constructivism
- 23.4 Role of Formal Systems
- 23.5 Practice vs Theory
Chapter 24. Limits of Formal Systems
This chapter studies incompleteness, undecidability, independence, and the boundaries of formal reasoning.
- 24.1 Incompleteness
- 24.2 Undecidability
- 24.3 Independence
- 24.4 Practical Implications
- 24.5 Future Directions
Appendix
1. Propositional LogicFoundations of propositional logic including syntax, semantics, equivalence, normal forms, and proof systems.
1.1 SyntaxDefinition of propositional variables, logical connectives, and formation rules for well formed formulas.
1.2 SemanticsTruth values, valuations, and evaluation of propositional formulas using truth tables.
1.3 EquivalenceLogical equivalence, truth preserving transformations, and basic laws for rewriting propositional formulas.
1.4 Normal FormsConjunctive normal form, disjunctive normal form, and systematic conversion of propositional formulas.
1.5 Soundness and CompletenessSoundness, completeness, and the relationship between semantic validity and formal provability.
2. First-Order LogicExtension of propositional logic with terms, predicates, quantifiers, structures, satisfaction, models, validity, and entailment.
2.1 Terms, PredicatesSyntax of first order logic including terms, predicate symbols, and the formation of formulas.
2.2 QuantifiersUniversal and existential quantifiers, scope, free variables, bound variables, and variable capture.
2.3 StructuresStructures, domains, and interpretations of symbols in first order logic.
2.4 SatisfactionSatisfaction, truth in a structure, models of sentences, and theories in first order logic.
2.5 Validity and EntailmentValidity, semantic entailment, satisfiability, countermodels, and logical consequence in first order logic.
3. Proof SystemsFormal systems for deriving logical conclusions including natural deduction, sequent calculus, Hilbert systems, and proof transformations.
3.1 Natural DeductionIntroduction to natural deduction, inference rules, and structured proofs for propositional logic.
3.2 Sequent CalculusSequents, structural rules, and introduction rules for logical connectives in the sequent calculus.
3.3 Hilbert SystemsHilbert style proof systems, axioms, and derivations using a minimal set of inference rules.
3.4 Proof TransformationsTransformations of proofs, normalization, and structural properties of derivations.
3.5 Cut EliminationThe cut rule, its elimination, and consequences for consistency and normalization.
4. Structures and ModelsBasic model theoretic notions including languages, signatures, substructures, embeddings, elementary equivalence, isomorphism, and examples.
4.1 LanguagesFormal languages, signatures, and symbols used to describe structures in first order logic.
4.2 SubstructuresSubstructures, generated substructures, homomorphisms, embeddings, and preservation of atomic formulas.
4.3 Elementary EquivalenceElementary equivalence, theories of structures, and preservation of first order sentences.
4.4 IsomorphismIsomorphisms of first order structures, structural invariants, and properties preserved by isomorphism.
4.5 ExamplesExamples of first order structures from algebra, order theory, graph theory, and geometry.
5. Compactness and CompletenessCompactness, completeness, Lowenheim-Skolem theorems, nonstandard models, and limitations of first order logic.
5.1 CompactnessDetailed development of the compactness theorem, its proof via completeness, and fundamental applications in model theory.
5.2 Lowenheim SkolemDownward and upward Lowenheim Skolem theorems and their consequences for model sizes in first order logic.
5.3 ApplicationsApplications of compactness and Lowenheim Skolem to algebraic structures and existence results.
5.4 Nonstandard ModelsConstruction and properties of nonstandard models using compactness and Lowenheim Skolem.
5.5 LimitationsExpressive limitations of first order logic, including inexpressibility of finiteness and categoricity issues.
6. Definability and TypesDefinable sets, definable functions, types, realizations, saturated models, stability theory, and classification programs.
6.1 Definable SetsDefinition of definable sets and functions in first order structures, with parameters, examples, closure properties, and proofs.
6.2 Types and RealizationsDefinition of complete and partial types, realization of types in structures, examples, consistency, and basic properties.
6.3 Saturated ModelsSaturated models, realization of types, and their role in controlling definability and extensions.
6.4 StabilityDetailed introduction to stability theory, counting types, order property, definability of types, and structural consequences.
6.5 ClassificationDetailed overview of classification theory, dividing lines such as stability, simplicity, and NIP, and the structural analysis of first order theories.
7. Basic Set TheoryBasic set theoretic notions including sets, relations, functions, cardinality, ordinals, well ordering, cardinal arithmetic, and the ZF and ZFC axioms.
7.1 Sets, Relations, FunctionsBasic set theoretic language, including sets, membership, subsets, operations, relations, equivalence relations, order relations, and functions.
7.2 Cardinality and CountabilityCardinality, finite and infinite sets, countable sets, uncountable sets, and Cantor diagonal arguments.
7.3 Ordinals and Well OrderingWell ordered sets, order isomorphisms, ordinals, successor ordinals, limit ordinals, and transfinite induction.
7.4 Arithmetic of CardinalsCardinal addition, multiplication, exponentiation, finite and infinite cardinal arithmetic, and basic comparison laws.
7.5 ZF and ZFCThe axioms of Zermelo Fraenkel set theory, the role of choice, and the use of axioms as a foundation for mathematics.
8. Axiomatic SystemsAxiom of Choice, equivalent formulations, constructible universe, consistency results, and independence phenomena.
8.1 Axiom of ChoiceThe axiom of choice, choice functions, indexed families, and first consequences in axiomatic set theory.
8.2 Equivalent FormulationsEquivalent forms of the axiom of choice, including Zorn's lemma, the well ordering theorem, maximal principles, and right inverses of surjections.
8.3 Constructible UniverseThe constructible universe, definable subsets, the hierarchy L_alpha, and the axiom of constructibility.
8.4 Consistency ResultsRelative consistency, inner models, constructibility, and the role of consistency results in axiomatic set theory.
8.5 Independence PhenomenaIndependence results in set theory, including the axiom of choice and the continuum hypothesis, and the methods used to establish independence.
9. Advanced Set TheoryForcing, large cardinals, descriptive set theory, determinacy principles, and applications in analysis and topology.
9.1 ForcingAn introduction to forcing, generic filters, forcing names, the forcing relation, and the basic extension theorem.
9.2 Large CardinalsAn introduction to large cardinal axioms, inaccessible cardinals, measurable cardinals, elementary embeddings, and consistency strength.
9.3 Descriptive Set TheoryAn introduction to Polish spaces, Borel sets, analytic sets, projective sets, regularity properties, and the role of definability in set theory.
9.4 DeterminacyAn introduction to infinite games, determined games, the axiom of determinacy, projective determinacy, and consequences for sets of reals.
9.5 ApplicationsApplications of advanced set theory to analysis and topology, including regularity properties, Banach spaces, measure theory, and topological classification.
10. Computable FunctionsRecursive functions, partial and total functions, the Church-Turing thesis, formal models of computation, and equivalence of models.
10.1 Recursive FunctionsPrimitive recursive functions, general recursive functions, minimization, and the formal construction of computable numerical functions.
10.2 Partial vs TotalDistinction between partial and total computable functions, undefined values, domains of definition, and the role of nontermination.
10.3 Church TuringThe Church Turing thesis, formal models of computation, equivalence of models, and the distinction between mathematical theorem and foundational principle.
10.4 Formal ModelsTuring machines, register machines, lambda calculus, recursive functions, and the precise mathematical models used to define computation.
10.5 EquivalenceDetailed equivalence proofs between Turing machines, recursive functions, and lambda calculus, with explicit constructions and simulations.
11. Turing MachinesTuring machine definitions, computation traces, universal machines, the halting problem, and undecidability results.
11.1 Machine DefinitionsFormal definition of Turing machines, including states, tape, alphabets, and transition functions.
11.2 Computation TracesStep-by-step evolution of Turing machine configurations and how computations are represented as traces.
11.3 Universal MachinesMachines that simulate any other Turing machine, establishing the concept of programmable computation.
11.4 Halting ProblemThe undecidable problem of determining whether a Turing machine halts on a given input.
11.5 Undecidability ResultsExtensions of undecidability using reductions and general results such as Rice’s theorem.
12. Degrees of UnsolvabilityReducibility, Turing degrees, recursively enumerable sets, Post's problem, and the structure of degrees.
12.1 ReducibilityFormal methods for comparing decision problems using many-one and Turing reducibility.
12.2 Turing DegreesEquivalence classes of sets under Turing reducibility and the ordering of computational power.
12.3 Recursively Enumerable SetsSets that can be enumerated by algorithms and their role in semi-decidability and computability theory.
12.4 Post’s ProblemExistence of intermediate degrees between computable sets and the halting problem.
12.5 Structure of DegreesGlobal properties of the Turing degrees including incomparability, density, and jump structure.
13. Formal Proof SystemsSyntax of proofs, derivability, normal forms, consistency proofs, proof length, and proof complexity.
13.1 Syntax of ProofsFormal structure of proofs, including derivations, inference rules, axioms, and proof representations.
13.2 DerivabilityFormal notion of deriving formulas from assumptions, including structural properties and inference behavior.
13.3 Normal FormsNormalization of proofs, elimination of detours, and structural simplification of derivations.
13.4 Consistency ProofsMethods for proving consistency of formal systems, including syntactic and semantic approaches.
13.5 Proof Length and ComplexityQuantitative study of proofs, including proof size, efficiency, and connections to computational complexity.
14. Godel TheoremsArithmetization of syntax, the first and second incompleteness theorems, implications for formal systems, and refinements.
14.1 ArithmetizationEncoding symbols, formulas, and proofs as natural numbers to allow arithmetic to reason about its own syntax.
14.2 First IncompletenessConstruction of a true but unprovable statement using diagonalization and self-reference.
14.3 Second IncompletenessProof that no sufficiently strong consistent system can prove its own consistency.
14.4 ImplicationsConsequences of incompleteness for truth, provability, independence, and the structure of formal systems.
14.5 ExtensionsStronger forms of incompleteness, Rosser’s improvement, Löb’s theorem, and connections to computability.
15. Ordinal AnalysisProof theoretic ordinals, transfinite induction, strength of theories, applications to arithmetic, and limits of formal strength.
16. Intuitionistic LogicConstructive semantics, proof interpretation, differences from classical logic, Kripke models, and applications in computation.
17. Type TheorySimple type theory, dependent types, Curry-Howard correspondence, proof assistants, and formalized mathematics.
17. Type TheorySimple type theory, dependent types, Curry-Howard correspondence, proof assistants, and formalized mathematics.
19. Formal LanguagesGrammars, syntax, automata theory, regular and context free languages, parsing, recognition, and applications in compilers.
20. Logic in ProgrammingLogic programming, type systems, verification, model checking, and program synthesis.
20. Logic in ProgrammingLogic programming, type systems, verification, model checking, and program synthesis.
22. Foundations ProgramsLogicism, formalism, intuitionism, structuralism, and modern perspectives on the foundations of mathematics.
22. Foundations ProgramsLogicism, formalism, intuitionism, structuralism, and modern perspectives on the foundations of mathematics.
24. Limits of Formal SystemsIncompleteness, undecidability, independence, practical implications, and future directions in logic and foundations.
PrefaceOverview of mathematical logic, its scope, and the structure of the book.