Practical foundations of mathematics

Description

Practical Foundations of Mathematics explains the basis of mathematical reasoning both in pure mathematics itself (algebra and topology in particular) and in computer science. In addition to the formal logic, this volume examines the relationship between computer languages and "plain English" mathematical proofs. The book introduces the reader to discrete mathematics, reasoning, and categorical logic. It offers a new approach to term algebras, induction and recursion and proves in detail the equivalence of types and categories. Each idea is illustrated by wide-ranging examples, and followed critically along its natural path, transcending disciplinary boundaries across 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. Cover......Page 1 BackCover......Page 2 Title......Page 5 Contents......Page 7 Introduction......Page 10 I. FIRST ORDER REASONING......Page 15 1-1 Substitution......Page 16 1 1-2 Denotation and Description......Page 25 1-3 Functions and Relations......Page 34 1-4 Direct Reasoning......Page 39 1-5 Proof Boxes......Page 44 1-6 Formal and Idiomatic Proof......Page 49 1-7 Automated Deduction......Page 58 1-8 Classical and Intuitionistic Logic......Page 66 Exercises I......Page 74 II. TYPES AND INDUCTION......Page 79 2-1 Constructing the Number Systems......Page 81 2-2 Sets (Zermelo Type Theory)......Page 86 2-3 Sums, Products and Function-Types......Page 95 2.4 Propositions as Types......Page 101 2-5 Induction and Recursion......Page 109 2-6 Constructions with Well Founded Relations......Page 116 2-7 Lists and Structural Induction......Page 120 2-8 Higher Order Logic......Page 126 Exercises II......Page 133 III. POSETS AND LATTICES......Page 139 3-1 Posets and Monotone Functions......Page 140 3-2 Meets, Joins and Lattices......Page 145 3-3 Fixed Points and Partial Functions......Page 150 3-4 Domains......Page 154 3-5 Products and Function-Spaces......Page 158 3-6 Adjunctions......Page 165 3-7 Closure Conditions and Induction......Page 170 3-8 Modalities and Galois Connections......Page 175 3-9 Constructions with Closure Conditions......Page 183 Exercises III......Page 189 IV. CARTESIAN CLOSED CATEGORIES......Page 197 4-1 Categories......Page 198 4-2 Actions and Sketches......Page 204 4-3 Categories for Formal Languages......Page 211 4-4 Functors......Page 220 4-5 A Universal Property: Products......Page 226 4-6 Algebraic Theories......Page 236 4-7 Interpretation of the Lambda Calculus......Page 242 4-8 Natural Transformations......Page 249 Exercises IV......Page 258 V. LIMITS AND COLIMITS......Page 264 5-1 Pullbacks and Equalisers......Page 265 5-2 Subobjects......Page 269 5-3 Partial and Conditional Programs......Page 275 5-4 Coproducts and Pushouts......Page 282 5-5 Extensive Categories......Page 288 5-6 Kernels, Quotients and Coequalisers......Page 294 5-7 Factorisation Systems......Page 300 5-8 Regular Categories......Page 306 Exercises V......Page 312 VI. STRUCTURAL RECURSION......Page 320 6-1 Free Algebras for Free Theories......Page 321 6-2 Well Formed Formulae......Page 329 6-3 The General Recursion Theorem......Page 336 6-4 Tail Recursion and Loop Programs......Page 343 6-5 Unification......Page 353 6-6 Finiteness......Page 357 6-7 The Ordinals......Page 366 Exercises VI......Page 374 VII_ ADJUNCTIONS......Page 381 7-1 Examples of Universal Constructions......Page 382 7-2 Adjunctions......Page 389 7-3 General Limits and Colimits......Page 396 7-4 Finding Limits and Free Algebras......Page 405 7-5 Monads......Page 411 7-6 From Semantics to Syntax......Page 418 7-7 Gluing and Completeness......Page 426 Exercises VII......Page 434 VIII. ALGEBRA WITH DEPENDENT TYPES......Page 440 8-1 The Language......Page 443 8-2 The Category of Contexts......Page 451 8-3 Display Categories and Equality Types......Page 463 8-4 Interpretation......Page 470 Exercises VIII......Page 481 IX. THE QUANTIFIERS......Page 483 9-1 The Predicate Convention......Page 484 9-2 Indexed and Fibred Categories......Page 490 9-3 Sums and Existential Quantification......Page 501 9-4 Dependent Products......Page 509 9-5 Comprehension and Powerset......Page 520 9-6 Universes......Page 526 Exercises IX......Page 537 BIBLIOGRAPHY......Page 544 INDEX......Page 567