Practical Foundations of Mathematics

by Paul Taylor

• ISBN13: 9780521631075
• ISBN10: 0521631076
• Format: Hardcover
• Copyright: 1999-05-13
• Publisher: Cambridge University Press

Summary

Practical Foundations collects the methods of construction of the objects of twentieth century mathematics. Although it is mainly concerned with a framework essentially equivalent to intuitionistic Zermelo-Fraenkel logic, the book looks forward to more subtle bases in categorical type theory and the machine representation of mathematics. Each idea is illustrated by wide-ranging examples, and followed critically along its natural path, transcending disciplinary boundaries between universal algebra, type theory, category theory, set theory, sheaf theory, topology and programming. Students and teachers of computing, mathematics and philosophy will find this book both readable and of lasting value as a reference work.

Table of Contents

Introduction	viii
First Order Reasoning	1	(64)
Substitution	2	(9)
Denotation and Description	11	(9)
Functions and Relations	20	(5)
Direct Reasoning	25	(5)
Proof Boxes	30	(5)
Formal and Idiomatic Proof	35	(9)
Automated Deduction	44	(8)
Classical and Intuitionistic Logic	52	(8)
Exercises I	60	(5)
Types and Induction	65	(60)
Constructing the Number Systems	67	(5)
Sets (Zermelo Type Theory)	72	(9)
Sums, Products and Function-Types	81	(6)
Propositions as Types	87	(8)
Induction and Recursion	95	(7)
Constructions with Well Founded Relations	102	(4)
Lists and Structural Induction	106	(6)
Higher Order Logic	112	(7)
Exercises II	119	(6)
Posets and Lattices	125	(58)
Posets and Monotone Functions	126	(5)
Meets, Joins and Lattices	131	(5)
Fixed Points and Partial Functions	136	(4)
Domains	140	(4)
Products and Function-Spaces	144	(7)
Adjunctions	151	(5)
Closure Conditions and Induction	156	(5)
Modalities and Galois Connections	161	(8)
Constructions with Closure Conditions	169	(6)
Exercises III	175	(8)
Cartesian Closed Categories	183	(67)
Categories	184	(6)
Actions and Sketches	190	(7)
Categories for Formal Languages	197	(9)
Functors	206	(6)
A Universal Property: Products	212	(10)
Algebraic Theories	222	(6)
Interpretation of the Lambda Calculus	228	(7)
Natural Transformations	235	(9)
Exercises IV	244	(6)
Limits and Colimits	250	(56)
Pullbacks and Equalisers	251	(4)
Subobjects	255	(6)
Partial and Conditional Programs	261	(7)
Coproducts and Pushouts	268	(6)
Extensive Categories	274	(6)
Kernels, Quotients and Coequalisers	280	(6)
Factorisation Systems	286	(6)
Regular Categories	292	(6)
Exercises V	298	(8)
Structural Recursion	306	(61)
Free Algebras for Free Theories	307	(8)
Well Formed Formulae	315	(7)
The General Recursion Theorem	322	(7)
Tail Recursion and Loop Programs	329	(10)
Unification	339	(4)
Finiteness	343	(9)
The Ordinals	352	(8)
Exercises VI	360	(7)
Adjunctions	367	(59)
Examples of Universal Constructions	368	(7)
Adjunctions	375	(7)
General Limits and Colimits	382	(9)
Finding Limits and Free Algebras	391	(6)
Monads	397	(7)
From Semantics to Syntax	404	(8)
Gluing and Completeness	412	(8)
Exercises VII	420	(6)
Algebra with Dependent Types	426	(43)
The Language	429	(8)
The Category of Contexts	437	(12)
Display Categories and Equality Types	449	(7)
Interpretation	456	(11)
Exercises VIII	467	(2)
The Quantifiers	469	(61)
The Predicate Convention	470	(6)
Indexed and Fibred Categories	476	(11)
Sums and Existential Quantification	487	(8)
Dependent Products	495	(11)
Comprehension and Powerset	506	(6)
Universes	512	(11)
Exercises IX	523	(7)
Bibliography	530	(23)
Index	553