Practical Foundations of Mathematics
Paul Taylor
Practical Foundations of Mathematics
Practical Foundations of Mathematics
Cambridge University Press
INTRODUCTION
I FIRST ORDER REASONING
- Introduction
- 1.1
- Substitution
- 1.2
- Denotation and Description
- 1.3
- Functions and Relations
- 1.4
- Direct Reasoning
- 1.5
- Proof Boxes
- 1.6
- Formal and Idiomatic Proof
- 1.7
- Automated Deduction
- 1.8
- Classical and Intuitionistic Logic
- Exercises I
II TYPES AND INDUCTION
- Introduction
- 2.1
- Constructing the Number Systems
- 2.2
- Sets (Zermelo Type Theory)
- 2.3
- Sums, Products and Function-Types
- 2.4
- Propositions as Types
- 2.5
- Induction and Recursion
- 2.6
- Constructions with Well Founded Relations
- 2.7
- Lists and Structural Induction
- 2.8
- Higher Order Logic
- Exercises II
III POSETS AND LATTICES
- Introduction
- 3.1
- Posets and Monotone Functions
- 3.2
- Meets, Joins and Lattices
- 3.3
- Fixed Points and Partial Functions
- 3.4
- Domains
- 3.5
- Products and Function-Spaces
- 3.6
- Adjunctions
- 3.7
- Closure Conditions and Induction
- 3.8
- Modalities and Galois Connections
- 3.9
- Constructions with Closure Conditions
- Exercises III
IV CARTESIAN CLOSED CATEGORIES
- Introduction
- 4.1
- Categories
- 4.2
- Actions and Sketches
- 4.3
- Categories for Formal Languages
- 4.4
- Functors
- 4.5
- A Universal Property: Products
- 4.6
- Algebraic Theories
- 4.7
- Interpretation of the Lambda Calculus
- 4.8
- Natural Transformations
- Exercises IV
V LIMITS AND COLIMITS
- Introduction
- 5.1
- Pullbacks and Equalisers
- 5.2
- Subobjects
- 5.3
- Partial and Conditional Programs
- 5.4
- Coproducts and Pushouts
- 5.5
- Extensive Categories
- 5.6
- Kernels, Quotients and Coequalisers
- 5.7
- Factorisation Systems
- 5.8
- Regular Categories
- Exercises V
VI STRUCTURAL RECURSION
- Introduction
- 6.1
- Free Algebras for Free Theories
- 6.2
- Well Formed Formulae
- 6.3
- The General Recursion Theorem
- 6.4
- Tail Recursion and Loop Programs
- 6.5
- Unification
- 6.6
- Finiteness
- 6.7
- The Ordinals
- Exercises VI
VII ADJUNCTIONS
- Introduction
- 7.1
- Examples of Universal Constructions
- 7.2
- Adjunctions
- 7.3
- General Limits and Colimits
- 7.4
- Finding Limits and Free Algebras
- 7.5
- Monads
- 7.6
- From Semantics to Syntax
- 7.7
- Gluing and Completeness
- Exercises VII
VIII ALGEBRA WITH DEPENDENT TYPES
- Introduction
- 8.1
- The Language
- 8.2
- The Category of Contexts
- 8.3
- Display Categories and Equality Types
- 8.4
- Interpretation
- Exercises VIII
IX THE QUANTIFIERS
- Introduction
- 9.1
- The Predicate Convention
- 9.2
- Indexed and Fibred Categories
- 9.3
- Sums and Existential Quantification
- 9.4
- Dependent Products
- 9.5
- Comprehension and Powerset
- 9.6
- Universes
- Exercises IX
BIBLIOGRAPHY
INDEX