Practical Foundations of Mathematics

Cover......Page C1
Backcover......Page C4
Title Page......Page iii
Contents......Page v
Introduction......Page viii
Advice to the reader......Page ix
Acknowledgements......Page x
Financial......Page xi
I. First Order Reasoning......Page 1
1.1 Substitution......Page 2
Structural recursion......Page 3
Terms and substitution......Page 6
Quantification......Page 7
Bound variables......Page 8
Substitution and variable-binding......Page 9
1.2 Denotation and Description......Page 11
Platonism and Formalism......Page 12
Laws as reduction rules......Page 13
Equivalence relations......Page 14
Confluence......Page 15
Theory of Descriptions......Page 17
Synonyms......Page 18
1.3 Functions and Relations......Page 20
Arity, source and target......Page 22
Semantics......Page 23
Relational calculus......Page 24
1.4 Direct Reasoning......Page 25
The language of predicate calculus......Page 26
The direct logical rules......Page 27
The provability relation......Page 28
Sequent presentation......Page 29
1.5 Proof Boxes......Page 30
The indirect rules......Page 31
Hypotheses and generic elements......Page 32
β-reduction of proofs......Page 34
Proof boxes delimited by keywords......Page 35
Importing and exporting formulae......Page 37
Open-ended boxes......Page 38
Declaration and assignment......Page 39
Alternative methods......Page 41
Model theory......Page 42
1.7 Automated Deduction......Page 44
Theoretical basis......Page 45
Resolution......Page 46
Unification......Page 48
Box-proof heuristics......Page 50
Excluded Middle......Page 52
The Sheffer stroke......Page 54
Intuitionism......Page 55
The axiom of choice......Page 57
Logic in a topos......Page 59
Exercises I......Page 60
II. Types and Induction......Page 65
The real numbers......Page 67
Functions and equivalence classes......Page 69
Unions and intersections......Page 70
Singletons and the empty set......Page 71
Singleton and product......Page 72
Comprehension and powerset......Page 73
Notation......Page 75
Parametric sets......Page 76
Historical comments......Page 77
Function (λ) abstraction......Page 81
Normalisation......Page 82
Contexts for the λ-calculus......Page 83
The sum type......Page 85
2.4 Propositions as Types......Page 87
Numerals and combinators......Page 88
The correspondence......Page 89
Programs out of proofs......Page 90
The constructive existential quantifier......Page 91
The existence and disjunction properties......Page 92
Classical logic......Page 93
The Cn notation......Page 94
2.5 Induction and Recursion......Page 95
Induction......Page 96
Minimal counterexamples......Page 99
Descending chains......Page 100
Proof trees......Page 101
2.6 Constructions with Well Founded Relations......Page 102
Complexity measures......Page 103
Products......Page 104
Induction for numbers and lists......Page 106
Concatenation......Page 108
Predecessor and pattern matching......Page 110
Type-theoretic rules for lists......Page 111
2.8 Higher Order Logic......Page 112
The type of propositions......Page 113
Definability of the connectives......Page 114
Cantor’s diagonalisation theorem......Page 115
Second order types......Page 116
Impredicativity......Page 118
Exercises II......Page 119
III. Posets and Lattices......Page 125
3.1 Posets and Monotone Functions......Page 126
Monotone functions......Page 128
Representation of orders by subset-inclusion......Page 129
Meets and joins......Page 131
Diagrams......Page 133
Lattices......Page 134
3.3 Fixed Points and Partial Functions......Page 136
The poset of partial functions......Page 137
The fixed point theorem......Page 139
Directed diagrams......Page 140
Posets with directed joins......Page 141
The Scott topology......Page 142
Products of posets, domains, lattices and diagrams......Page 144
Pointwise meets and joins......Page 146
Joint continuity......Page 148
Scott’s thesis......Page 149
3.6 Adjunctions......Page 151
Order, composition and equivalence......Page 152
The adjoint function theorem......Page 153
Frames and Heyting algebras......Page 155
3.7 Closure Conditions and Induction......Page 156
Closure conditions......Page 157
Induction on closures......Page 158
Modal logic......Page 161
The transitive closure......Page 163
Modal logic for preorders......Page 164
Galois connections......Page 166
The Lindenbaum algebra for conjunction......Page 169
Algebraic lattices......Page 171
Adding and preserving joins......Page 172
Joins with are stable under meet......Page 173
Generalising from propositions to types......Page 174
Exercises III......Page 175
IV. Cartesian Closed Categories......Page 183
4.1 Categories......Page 184
Categories as congregations......Page 185
Categories as structures......Page 186
Size issues......Page 189
Actions with a single sort......Page 190
Sketches......Page 192
Generating a category......Page 195
Operational interpretation......Page 197
Logical interpretation......Page 199
Normal forms......Page 200
The category of contexts and substitutions......Page 202
Terms as sections......Page 204
Use of variables......Page 205
4.4 Functors......Page 206
Constructions as functors......Page 207
A classifying category......Page 208
The force of functoriality......Page 209
Full and faithful......Page 210
4.5 A Universal Property: Products......Page 212
The terminal object......Page 213
Unique up to unique isomorphism......Page 215
Products......Page 216
Preservation and creation of products......Page 217
Using the existence of products......Page 218
Universal properties give functors......Page 219
All universal properties are terminal objects......Page 220
4.6 Algebraic Theories......Page 222
Examples......Page 223
Semantics of expressions......Page 225
The classifying category......Page 227
4.7 Interpretation of the Lambda Calculus......Page 228
The raw calculus......Page 229
Interpretation......Page 231
The β- and η-rules......Page 232
The universal property......Page 233
Cartesian closed categories of domains......Page 234
4.8 Natural Transformations......Page 235
Composition......Page 238
Equivalences......Page 240
Functor categories......Page 241
The Yoneda Lemma......Page 242
2-Categories......Page 243
Exercises IV......Page 244
V. Limits and Colimits......Page 250
5.1 Pullbacks and Equalisers......Page 251
Applications......Page 252
Slices......Page 254
5.2 Subobjects......Page 255
The lattice of subobjects......Page 257
Sets of solutions of equations......Page 258
5.3 Partial and Conditional Programs......Page 261
Partial morphisms......Page 264
Conditionals......Page 265
5.4 Coproducts and Pushouts......Page 268
Abelian categories......Page 269
Stone duality......Page 271
Free (co)products and van Kampen’s theorem......Page 272
Distributivity......Page 274
Extensive categories......Page 276
Stable disjoint sums......Page 277
Interpretation of theories with disjunction......Page 279
Kernels......Page 280
Congruences......Page 281
Quotients......Page 282
General coequalisers......Page 284
Colimits by duality......Page 285
5.7 Factorisation Systems......Page 286
Image factorisation......Page 288
Properties of factorisation systems......Page 289
Finding factorisations......Page 291
5.8 Regular Categories......Page 292
Stable image factorisation......Page 294
Relations......Page 295
Stable unions......Page 297
Exercises V......Page 298
VI. Structural Recursion......Page 306
6.1 Free Algebras for Free Theories......Page 307
Infinitary algebraic theories without laws......Page 308
Natural numbers......Page 311
Infinitary conjunction and disjunction......Page 312
Existence of equationally free models......Page 314
Recursive covers......Page 315
Variables......Page 317
Many-sorted theories......Page 318
Formation rules in type theories......Page 319
Infinitary operations......Page 320
6.3 The General Recursion Theorem......Page 322
Well founded coalgebras......Page 323
The recursion scheme......Page 325
The general recursion theorem......Page 327
6.4 Tail Recursion and Loop Programs......Page 329
Semantics......Page 330
Transitive closure......Page 333
The recursion and induction schemes......Page 335
Partial correcteness......Page 337
Discussion......Page 338
6.5 Unification......Page 339
Unification......Page 340
6.6 Finiteness......Page 343
Three definitions by counting......Page 345
The ability to count......Page 346
Finite subsets......Page 348
Finiteness and Scott-continuity......Page 350
6.7 The Ordinals......Page 352
Transfinite recursion......Page 353
Arithmetic......Page 355
Classical applications......Page 357
Axiomatisation......Page 358
Exercises VI......Page 360
VII. Adjunctions......Page 367
7.1 Examples of Universal Constructions......Page 368
Colimits......Page 369
Completions......Page 370
Co-universal properties......Page 371
Classifying categories......Page 373
7.2 Adjunctions......Page 375
Applications......Page 377
Proof of the equivalence......Page 380
Reflections and representables......Page 381
7.3 General Limits and Colimits......Page 382
Adjoints preserve co(limits)......Page 386
Comma categories......Page 388
Equivalent colimits......Page 389
The general adjoint functor theorem......Page 390
Limits and colimits in topology and order theory......Page 391
Generators and relations......Page 393
Computing colimits......Page 395
Treating relations as another theory......Page 396
7.5 Monads......Page 397
The Kleisli and Eilenberg-Moore categories......Page 398
Beck’s theorem......Page 400
Applications......Page 402
7.6 From Semantics to Syntax......Page 404
Encoding operations......Page 405
Canonical language......Page 407
The equivalence......Page 409
Conservativity by normalisation......Page 411
7.7 Gluing and Completeness......Page 412
The gluing construction......Page 413
Conservativity......Page 415
Existence and disjunction properties......Page 418
Exponentials......Page 419
Exercises VII......Page 420
VIII. Algebra with Dependent Types......Page 426
8.1 The Language......Page 429
Terms......Page 431
Equality of terms......Page 432
Equality of types......Page 433
The object-language......Page 435
8.2 The Category of Contexts......Page 437
Objects......Page 438
Display maps......Page 439
Cuts......Page 440
Laws......Page 441
Normal forms for morphisms......Page 444
Substitution by pullback......Page 447
8.3 Display Categories and Equality Types......Page 449
Display maps......Page 450
Products and equality types......Page 452
Display maps in topology and elsewhere......Page 453
Relative slices......Page 455
Derivation histories in normal form......Page 456
Canonical language......Page 460
Completeness......Page 463
Type-theoretic notation in categories......Page 466
Exercises VIII......Page 467
IX. The Quantifiers......Page 469
9.1 The Predicate Convention......Page 470
Fibrations......Page 472
The quantifier formation rules......Page 473
Adjointness in foundations......Page 474
The recursive definition of interpretations......Page 475
9.2 Indexed and Fibred Categories......Page 476
Separating propositions from types......Page 477
Fibrations......Page 481
Models......Page 484
Coherence issues......Page 485
Dependent sums and composition......Page 487
Unsubstituted weak sums and the adjunction......Page 488
Substitution and the Beck-Chevalley condition......Page 490
Semantics and open maps......Page 492
Strong sums......Page 493
9.4 Dependent Products......Page 495
Application and abstraction......Page 496
The adjunction, Beck-Chevalley condition and other forms......Page 497
Local cartesian closure......Page 498
Partial products......Page 500
Partial products suffice......Page 503
Comprehension......Page 506
The type of propositions......Page 508
Gödel’s incompleteness theorem......Page 512
Full internal subcategories......Page 514
Russell’s paradox......Page 516
The axiom-scheme of replacement......Page 518
Infinite limits and colimits......Page 519
Transfinite iteration and fixed points of functors......Page 520
Exercises IX......Page 523
B......Page 530
C......Page 533
D......Page 534
E......Page 535
F......Page 536
G......Page 537
H......Page 539
J......Page 540
K......Page 541
L......Page 542
M......Page 544
N......Page 546
P......Page 547
R......Page 548
S......Page 549
T......Page 550
V......Page 551
Z......Page 552
A......Page 553
C......Page 554
D......Page 557
E......Page 558
F......Page 559
H......Page 561
I......Page 562
L......Page 563
M......Page 564
O......Page 565
P......Page 566
Q......Page 567
R......Page 568
S......Page 569
U......Page 571
Z......Page 572