03. Logic and Foundations

Formal logic, set theory, computability, and the foundations of mathematics treated as a formal system.

95 items

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.

Chapter 2. First-Order Logic

This chapter extends propositional logic by introducing terms, predicates, quantifiers, and structures for interpreting mathematical statements.

Chapter 3. Proof Systems

This chapter studies formal systems for deriving conclusions, including natural deduction, sequent calculus, and Hilbert systems.

Part II. Model Theory

Chapter 4. Structures and Models

This chapter introduces formal structures, interpretations of languages, and methods for comparing mathematical models.

Chapter 5. Compactness and Completeness

This chapter develops compactness, completeness, and model existence results, together with their applications.

Chapter 6. Definability and Types

This chapter studies definable sets, types, saturation, and the beginnings of classification theory.

Part III. Set Theory

Chapter 7. Basic Set Theory

This chapter introduces sets, relations, functions, cardinality, ordinals, and the basic axioms of set theory.

Chapter 8. Axiomatic Systems

This chapter studies the Axiom of Choice, equivalent principles, constructibility, and independence results.

Chapter 9. Advanced Set Theory

This chapter introduces forcing, large cardinals, descriptive set theory, and advanced applications.

Part IV. Computability Theory

Chapter 10. Computable Functions

This chapter develops formal notions of computation, recursive functions, and equivalent computational models.

Chapter 11. Turing Machines

This chapter presents Turing machines, universal computation, and undecidability results.

Chapter 12. Degrees of Unsolvability

This chapter compares undecidable problems using reducibility and studies the structure of Turing degrees.

Part V. Proof Theory

Chapter 13. Formal Proof Systems

This chapter studies proofs as formal objects, including derivations, normalization, and complexity.

Chapter 14. Godel Theorems

This chapter presents the incompleteness theorems and their consequences for formal systems.

Chapter 15. Ordinal Analysis

This chapter studies the strength of theories using ordinals and transfinite methods.

Part VI. Type Theory and Constructive Logic

Chapter 16. Intuitionistic Logic

This chapter develops constructive logic, proof interpretation, and Kripke semantics.

Chapter 17. Type Theory

This chapter introduces type systems, dependent types, and the connection between proofs and programs.

Chapter 18. Homotopy Type Theory

This chapter presents types as spaces, equality as paths, and the univalence principle.

Part VII. Logic and Computer Science

Chapter 19. Formal Languages

This chapter studies grammars, automata, and language recognition.

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.

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.

Chapter 24. Limits of Formal Systems

This chapter studies incompleteness, undecidability, independence, and the boundaries of formal reasoning.

Appendix

Maths › 03. Logic and Foundations ›

Preface

Overview of mathematical logic, its scope, and the structure of the book.
logic foundations preface May 2, 2026
Maths › 03. Logic and Foundations ›

1. Propositional Logic

Foundations of propositional logic including syntax, semantics, equivalence, normal forms, and proof systems.
logic propositional logic foundations May 2, 2026
Maths › 03. Logic and Foundations ›

1.1 Syntax

Definition of propositional variables, logical connectives, and formation rules for well formed formulas.
logic propositional logic syntax formulas May 2, 2026
Maths › 03. Logic and Foundations ›

1.2 Semantics

Truth values, valuations, and evaluation of propositional formulas using truth tables.
logic propositional logic semantics truth tables May 2, 2026
Maths › 03. Logic and Foundations ›

1.3 Equivalence

Logical equivalence, truth preserving transformations, and basic laws for rewriting propositional formulas.
logic propositional logic equivalence boolean algebra May 2, 2026
Maths › 03. Logic and Foundations ›

1.4 Normal Forms

Conjunctive normal form, disjunctive normal form, and systematic conversion of propositional formulas.
logic propositional logic normal forms CNF DNF May 2, 2026
Maths › 03. Logic and Foundations ›

1.5 Soundness and Completeness

Soundness, completeness, and the relationship between semantic validity and formal provability.
logic propositional logic proof theory soundness completeness May 2, 2026
Maths › 03. Logic and Foundations ›

2. First-Order Logic

Extension of propositional logic with terms, predicates, quantifiers, structures, satisfaction, models, validity, and entailment.
logic first-order logic model theory foundations May 2, 2026
Maths › 03. Logic and Foundations ›

2.1 Terms, Predicates

Syntax of first order logic including terms, predicate symbols, and the formation of formulas.
logic first order logic syntax terms predicates May 2, 2026
Maths › 03. Logic and Foundations ›

2.2 Quantifiers

Universal and existential quantifiers, scope, free variables, bound variables, and variable capture.
logic first order logic quantifiers scope variables May 2, 2026
Maths › 03. Logic and Foundations ›

2.3 Structures

Structures, domains, and interpretations of symbols in first order logic.
logic first order logic structures interpretations models May 2, 2026
Maths › 03. Logic and Foundations ›

2.4 Satisfaction

Satisfaction, truth in a structure, models of sentences, and theories in first order logic.
logic first order logic satisfaction models theories May 2, 2026
Maths › 03. Logic and Foundations ›

2.5 Validity and Entailment

Validity, semantic entailment, satisfiability, countermodels, and logical consequence in first order logic.
logic first order logic validity entailment models May 2, 2026
Maths › 03. Logic and Foundations ›

3. Proof Systems

Formal systems for deriving logical conclusions including natural deduction, sequent calculus, Hilbert systems, and proof transformations.
logic proof theory formal systems May 2, 2026
Maths › 03. Logic and Foundations ›

3.1 Natural Deduction

Introduction to natural deduction, inference rules, and structured proofs for propositional logic.
logic proof systems natural deduction May 2, 2026
Maths › 03. Logic and Foundations ›

3.2 Sequent Calculus

Sequents, structural rules, and introduction rules for logical connectives in the sequent calculus.
logic proof systems sequent calculus May 2, 2026
Maths › 03. Logic and Foundations ›

3.3 Hilbert Systems

Hilbert style proof systems, axioms, and derivations using a minimal set of inference rules.
logic proof systems hilbert systems May 2, 2026
Maths › 03. Logic and Foundations ›

3.4 Proof Transformations

Transformations of proofs, normalization, and structural properties of derivations.
logic proof systems proof theory normalization May 2, 2026
Maths › 03. Logic and Foundations ›

3.5 Cut Elimination

The cut rule, its elimination, and consequences for consistency and normalization.
logic proof systems sequent calculus cut elimination May 2, 2026
Maths › 03. Logic and Foundations ›

4. Structures and Models

Basic model theoretic notions including languages, signatures, substructures, embeddings, elementary equivalence, isomorphism, and examples.
logic model theory structures models May 2, 2026
Maths › 03. Logic and Foundations ›

4.1 Languages

Formal languages, signatures, and symbols used to describe structures in first order logic.
logic model theory languages signatures May 2, 2026
Maths › 03. Logic and Foundations ›

4.2 Substructures

Substructures, generated substructures, homomorphisms, embeddings, and preservation of atomic formulas.
logic model theory substructures embeddings May 2, 2026
Maths › 03. Logic and Foundations ›

4.3 Elementary Equivalence

Elementary equivalence, theories of structures, and preservation of first order sentences.
logic model theory elementary equivalence theories May 2, 2026
Maths › 03. Logic and Foundations ›

4.4 Isomorphism

Isomorphisms of first order structures, structural invariants, and properties preserved by isomorphism.
logic model theory isomorphism invariants May 2, 2026
Maths › 03. Logic and Foundations ›

4.5 Examples

Examples of first order structures from algebra, order theory, graph theory, and geometry.
logic model theory structures algebra geometry May 2, 2026
Maths › 03. Logic and Foundations ›

5. Compactness and Completeness

Compactness, completeness, Lowenheim-Skolem theorems, nonstandard models, and limitations of first order logic.
logic model theory compactness completeness May 2, 2026
Maths › 03. Logic and Foundations ›

5.1 Compactness

Detailed development of the compactness theorem, its proof via completeness, and fundamental applications in model theory.
logic model theory compactness first order logic May 2, 2026
Maths › 03. Logic and Foundations ›

5.2 Lowenheim Skolem

Downward and upward Lowenheim Skolem theorems and their consequences for model sizes in first order logic.
logic model theory lowenheim skolem cardinality May 2, 2026
Maths › 03. Logic and Foundations ›

5.3 Applications

Applications of compactness and Lowenheim Skolem to algebraic structures and existence results.
logic model theory algebra compactness applications May 2, 2026
Maths › 03. Logic and Foundations ›

5.4 Nonstandard Models

Construction and properties of nonstandard models using compactness and Lowenheim Skolem.
logic model theory nonstandard models compactness May 2, 2026
Maths › 03. Logic and Foundations ›

5.5 Limitations

Expressive limitations of first order logic, including inexpressibility of finiteness and categoricity issues.
logic model theory limitations expressiveness May 2, 2026
Maths › 03. Logic and Foundations ›

6. Definability and Types

Definable sets, definable functions, types, realizations, saturated models, stability theory, and classification programs.
logic model theory definability types May 2, 2026
Maths › 03. Logic and Foundations ›

6.1 Definable Sets

Definition of definable sets and functions in first order structures, with parameters, examples, closure properties, and proofs.
logic model theory definability first order logic May 2, 2026
Maths › 03. Logic and Foundations ›

6.2 Types and Realizations

Definition of complete and partial types, realization of types in structures, examples, consistency, and basic properties.
logic model theory types realizations May 2, 2026
Maths › 03. Logic and Foundations ›

6.3 Saturated Models

Saturated models, realization of types, and their role in controlling definability and extensions.
logic model theory saturated models types May 2, 2026
Maths › 03. Logic and Foundations ›

6.4 Stability

Detailed introduction to stability theory, counting types, order property, definability of types, and structural consequences.
logic model theory stability types May 2, 2026
Maths › 03. Logic and Foundations ›

6.5 Classification

Detailed overview of classification theory, dividing lines such as stability, simplicity, and NIP, and the structural analysis of first order theories.
logic model theory classification theory stability May 2, 2026
Maths › 03. Logic and Foundations ›

7. Basic Set Theory

Basic set theoretic notions including sets, relations, functions, cardinality, ordinals, well ordering, cardinal arithmetic, and the ZF and ZFC axioms.
logic set theory cardinality ordinals zfc May 2, 2026
Maths › 03. Logic and Foundations ›

7.1 Sets, Relations, Functions

Basic set theoretic language, including sets, membership, subsets, operations, relations, equivalence relations, order relations, and functions.
logic set theory sets relations functions May 2, 2026
Maths › 03. Logic and Foundations ›

7.2 Cardinality and Countability

Cardinality, finite and infinite sets, countable sets, uncountable sets, and Cantor diagonal arguments.
logic set theory cardinality countability infinity May 2, 2026
Maths › 03. Logic and Foundations ›

7.3 Ordinals and Well Ordering

Well ordered sets, order isomorphisms, ordinals, successor ordinals, limit ordinals, and transfinite induction.
logic set theory ordinals well ordering transfinite induction May 2, 2026
Maths › 03. Logic and Foundations ›

7.4 Arithmetic of Cardinals

Cardinal addition, multiplication, exponentiation, finite and infinite cardinal arithmetic, and basic comparison laws.
logic set theory cardinals cardinal arithmetic infinity May 2, 2026
Maths › 03. Logic and Foundations ›

7.5 ZF and ZFC

The axioms of Zermelo Fraenkel set theory, the role of choice, and the use of axioms as a foundation for mathematics.
logic set theory ZF ZFC axioms May 2, 2026
Maths › 03. Logic and Foundations ›

8. Axiomatic Systems

Axiom of Choice, equivalent formulations, constructible universe, consistency results, and independence phenomena.
logic set theory axioms choice independence May 2, 2026
Maths › 03. Logic and Foundations ›

8.1 Axiom of Choice

The axiom of choice, choice functions, indexed families, and first consequences in axiomatic set theory.
logic set theory axiom of choice ZFC May 2, 2026
Maths › 03. Logic and Foundations ›

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.
logic set theory axiom of choice zorn lemma well ordering May 2, 2026
Maths › 03. Logic and Foundations ›

8.3 Constructible Universe

The constructible universe, definable subsets, the hierarchy L_alpha, and the axiom of constructibility.
logic set theory constructible universe inner models May 2, 2026
Maths › 03. Logic and Foundations ›

8.4 Consistency Results

Relative consistency, inner models, constructibility, and the role of consistency results in axiomatic set theory.
logic set theory consistency inner models constructibility May 2, 2026
Maths › 03. Logic and Foundations ›

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.
logic set theory independence forcing constructibility May 2, 2026
Maths › 03. Logic and Foundations ›

9. Advanced Set Theory

Forcing, large cardinals, descriptive set theory, determinacy principles, and applications in analysis and topology.
logic set theory forcing large cardinals descriptive set theory May 2, 2026
Maths › 03. Logic and Foundations ›

9.1 Forcing

An introduction to forcing, generic filters, forcing names, the forcing relation, and the basic extension theorem.
logic set theory forcing independence May 2, 2026
Maths › 03. Logic and Foundations ›

9.2 Large Cardinals

An introduction to large cardinal axioms, inaccessible cardinals, measurable cardinals, elementary embeddings, and consistency strength.
logic set theory large cardinals foundations May 2, 2026
Maths › 03. Logic and Foundations ›

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.
logic set theory descriptive set theory definability May 2, 2026
Maths › 03. Logic and Foundations ›

9.4 Determinacy

An introduction to infinite games, determined games, the axiom of determinacy, projective determinacy, and consequences for sets of reals.
logic set theory determinacy descriptive set theory May 2, 2026
Maths › 03. Logic and Foundations ›

9.5 Applications

Applications of advanced set theory to analysis and topology, including regularity properties, Banach spaces, measure theory, and topological classification.
logic set theory analysis topology applications May 2, 2026
Maths › 03. Logic and Foundations ›

10. Computable Functions

Recursive functions, partial and total functions, the Church-Turing thesis, formal models of computation, and equivalence of models.
logic computability recursive functions computation May 2, 2026
Maths › 03. Logic and Foundations ›

10.1 Recursive Functions

Primitive recursive functions, general recursive functions, minimization, and the formal construction of computable numerical functions.
logic computability recursive functions primitive recursion May 2, 2026
Maths › 03. Logic and Foundations ›

10.2 Partial vs Total

Distinction between partial and total computable functions, undefined values, domains of definition, and the role of nontermination.
logic computability partial functions total functions May 2, 2026
Maths › 03. Logic and Foundations ›

10.3 Church Turing

The Church Turing thesis, formal models of computation, equivalence of models, and the distinction between mathematical theorem and foundational principle.
logic computability church turing thesis turing machines recursive functions May 2, 2026
Maths › 03. Logic and Foundations ›

10.4 Formal Models

Turing machines, register machines, lambda calculus, recursive functions, and the precise mathematical models used to define computation.
logic computability formal models turing machines lambda calculus May 2, 2026
Maths › 03. Logic and Foundations ›

10.5 Equivalence

Detailed equivalence proofs between Turing machines, recursive functions, and lambda calculus, with explicit constructions and simulations.
logic computability equivalence turing machines recursive functions May 2, 2026
Maths › 03. Logic and Foundations ›

11. Turing Machines

Turing machine definitions, computation traces, universal machines, the halting problem, and undecidability results.
logic computability turing machines undecidability May 2, 2026
Maths › 03. Logic and Foundations ›

11.1 Machine Definitions

Formal definition of Turing machines, including states, tape, alphabets, and transition functions.
turing machines formal models computation automata theory May 2, 2026
Maths › 03. Logic and Foundations ›

11.2 Computation Traces

Step-by-step evolution of Turing machine configurations and how computations are represented as traces.
turing machines computation traces configurations algorithms May 2, 2026
Maths › 03. Logic and Foundations ›

11.3 Universal Machines

Machines that simulate any other Turing machine, establishing the concept of programmable computation.
turing machines universality simulation programs computation May 2, 2026
Maths › 03. Logic and Foundations ›

11.4 Halting Problem

The undecidable problem of determining whether a Turing machine halts on a given input.
halting problem undecidability computability logic theory May 2, 2026
Maths › 03. Logic and Foundations ›

11.5 Undecidability Results

Extensions of undecidability using reductions and general results such as Rice’s theorem.
undecidability reductions rice theorem computability logic May 2, 2026
Maths › 03. Logic and Foundations ›

12. Degrees of Unsolvability

Reducibility, Turing degrees, recursively enumerable sets, Post's problem, and the structure of degrees.
logic computability turing degrees reducibility recursively enumerable sets May 2, 2026
Maths › 03. Logic and Foundations ›

12.1 Reducibility

Formal methods for comparing decision problems using many-one and Turing reducibility.
computability reducibility decision problems turing machines May 2, 2026
Maths › 03. Logic and Foundations ›

12.2 Turing Degrees

Equivalence classes of sets under Turing reducibility and the ordering of computational power.
computability turing degrees oracle computation degree theory May 2, 2026
Maths › 03. Logic and Foundations ›

12.3 Recursively Enumerable Sets

Sets that can be enumerated by algorithms and their role in semi-decidability and computability theory.
computability recursively enumerable semi-decidable halting problem May 2, 2026
Maths › 03. Logic and Foundations ›

12.4 Post’s Problem

Existence of intermediate degrees between computable sets and the halting problem.
computability post problem priority method turing degrees May 2, 2026
Maths › 03. Logic and Foundations ›

12.5 Structure of Degrees

Global properties of the Turing degrees including incomparability, density, and jump structure.
computability degree structure turing degrees logic May 2, 2026
Maths › 03. Logic and Foundations ›

13. Formal Proof Systems

Syntax of proofs, derivability, normal forms, consistency proofs, proof length, and proof complexity.
logic proof theory formal proofs derivability proof complexity May 2, 2026
Maths › 03. Logic and Foundations ›

13.1 Syntax of Proofs

Formal structure of proofs, including derivations, inference rules, axioms, and proof representations.
logic proof theory syntax derivations May 2, 2026
Maths › 03. Logic and Foundations ›

13.2 Derivability

Formal notion of deriving formulas from assumptions, including structural properties and inference behavior.
logic proof theory derivability inference May 2, 2026
Maths › 03. Logic and Foundations ›

13.3 Normal Forms

Normalization of proofs, elimination of detours, and structural simplification of derivations.
logic proof theory normalization structure May 2, 2026
Maths › 03. Logic and Foundations ›

13.4 Consistency Proofs

Methods for proving consistency of formal systems, including syntactic and semantic approaches.
logic proof theory consistency foundations May 2, 2026
Maths › 03. Logic and Foundations ›

13.5 Proof Length and Complexity

Quantitative study of proofs, including proof size, efficiency, and connections to computational complexity.
logic proof theory complexity computation May 2, 2026
Maths › 03. Logic and Foundations ›

14. Godel Theorems

Arithmetization of syntax, the first and second incompleteness theorems, implications for formal systems, and refinements.
logic proof theory godel theorems incompleteness formal systems May 2, 2026
Maths › 03. Logic and Foundations ›

14.1 Arithmetization

Encoding symbols, formulas, and proofs as natural numbers to allow arithmetic to reason about its own syntax.
logic godel numbering arithmetization syntax foundations May 2, 2026
Maths › 03. Logic and Foundations ›

14.2 First Incompleteness

Construction of a true but unprovable statement using diagonalization and self-reference.
logic godel incompleteness diagonalization proof theory May 2, 2026
Maths › 03. Logic and Foundations ›

14.3 Second Incompleteness

Proof that no sufficiently strong consistent system can prove its own consistency.
logic godel consistency incompleteness foundations May 2, 2026
Maths › 03. Logic and Foundations ›

14.4 Implications

Consequences of incompleteness for truth, provability, independence, and the structure of formal systems.
logic foundations incompleteness philosophy mathematics May 2, 2026
Maths › 03. Logic and Foundations ›

14.5 Extensions

Stronger forms of incompleteness, Rosser’s improvement, Löb’s theorem, and connections to computability.
logic godel proof theory computability foundations May 2, 2026
Maths › 03. Logic and Foundations ›

15. Ordinal Analysis

Proof theoretic ordinals, transfinite induction, strength of theories, applications to arithmetic, and limits of formal strength.
logic proof theory ordinal analysis transfinite induction formal systems May 2, 2026
Maths › 03. Logic and Foundations ›

16. Intuitionistic Logic

Constructive semantics, proof interpretation, differences from classical logic, Kripke models, and applications in computation.
logic intuitionistic logic constructive logic kripke models computation May 2, 2026
Maths › 03. Logic and Foundations ›

17. Type Theory

Simple type theory, dependent types, Curry-Howard correspondence, proof assistants, and formalized mathematics.
logic type theory dependent types proof assistants formalized mathematics May 2, 2026
Maths › 03. Logic and Foundations ›

17. Type Theory

Simple type theory, dependent types, Curry-Howard correspondence, proof assistants, and formalized mathematics.
logic type theory dependent types proof assistants formalized mathematics May 2, 2026
Maths › 03. Logic and Foundations ›

19. Formal Languages

Grammars, syntax, automata theory, regular and context free languages, parsing, recognition, and applications in compilers.
logic computer science formal languages automata compilers May 2, 2026
Maths › 03. Logic and Foundations ›

20. Logic in Programming

Logic programming, type systems, verification, model checking, and program synthesis.
logic computer science programming languages verification program synthesis May 2, 2026
Maths › 03. Logic and Foundations ›

20. Logic in Programming

Logic programming, type systems, verification, model checking, and program synthesis.
logic computer science programming languages verification program synthesis May 2, 2026
Maths › 03. Logic and Foundations ›

22. Foundations Programs

Logicism, formalism, intuitionism, structuralism, and modern perspectives on the foundations of mathematics.
logic foundations logicism formalism intuitionism structuralism May 2, 2026
Maths › 03. Logic and Foundations ›

22. Foundations Programs

Logicism, formalism, intuitionism, structuralism, and modern perspectives on the foundations of mathematics.
logic foundations logicism formalism intuitionism structuralism May 2, 2026
Maths › 03. Logic and Foundations ›

24. Limits of Formal Systems

Incompleteness, undecidability, independence, practical implications, and future directions in logic and foundations.
logic foundations incompleteness undecidability independence May 2, 2026