Practical Foundations of Mathematics: "Practical Foundations of Mathematics

Practical Foundations of Mathematics

Paul Taylor

Practical Foundations of Mathematics

Practical Foundations of Mathematics

Paul Taylor

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

Comments"