Constructivism in Mathematics, Vol 2 (eBook)

Front Cover 1
Constructivism in Mathematics: An Introduction 4
Copyright Page 5
Table of Contents 10
Dedication 6
Constructivism in Mathematics: Contents 8
Preliminaries 14
Chapter 7. The topology of metric spaces 20
1. Basic definitions 20
2. Complete, separable metric spaces 25
3. Located sets 33
4. Complete, totally bounded spaces 38
5. Locally compact spaces 46
6. Notes 51
Exercises 54
Chapter 8. Algebra 58
1. Identity, apartness and order 58
2. Groups 63
3. Rings and modules 74
4. Linear algebra 82
5. Polynomial rings 90
6. Fields and local rings 105
7. The fundamental theorem of algebra 109
8. Notes 113
Exercises 114
Chapter 9. Finite-type arithmetic and theories of operators 118
1. Intuitionistic finite-type arithmetic 119
2. Normalization, and a term model for HA. 133
3. The theory APP 147
4. Models for APP 155
5. Abstract realizability in APP 166
6. Extensionality and choice in APP and HA. 170
7. Some metamathematical applications 176
8. Theories of operators and classes 187
9. Notes 192
Exercises 195
Chapter 10. Proof theory of intuitionistic logic 202
1. Preliminaries 202
2. Normalization 207
3. The structure of normal derivations of N-IQCE 213
4. The decidability of IPC 216
5. Other applications of normalization 219
6. Conservative addition of predicative classes 223
7. Sequent calculi 225
8. N-IQC as a calculus of terms 231
9. Notes 238
Exercises 240
Chapter 11. The theory of types and constructive set theory 246
1. Towards a theory of types 246
2. The theory MVio 250
3. Some alternative formulations of MVio 264
4. The types Nk and reformulation of the E-rules 267
5. The theory MLo 278
6. Embeddings into APP 283
7. Extensions of MLiq and MLo 286
8. Constructive set theory 294
9. Notes 307
Exercises 310
Chapter 12. Choice sequences 314
1. Introduction 314
2. Lawless sequences 320
3. The elimination translation for the theory LS 333
4. Other notions of choice sequence 340
5. Notes 347
Exercises 349
Chapter 13. Semantical completeness 352
1. Beth models 352
2. Completeness for intuitionistic validity 360
3. Incompleteness results 369
4. Lattices, Heyting algebras and complete Heyting algebras 375
5. Algebraic semantics for IPC 380
6. .-sets and structures 384
7. Validity as forcing 394
8. Postscript on realizability 399
9. Notes 404
Exercises 408
Chapter 14. Sheaves, sites and higher-order logic 412
1. Presheaves, sheaves and sheaf-completion 413
2. .-presheaf and .-sheaf structures 422
3. Some notions from category theory 426
4. Forcing over sites 434
5. Sheaf models for higher-order logic 442
6. Notes 450
Exercises 452
Chapter 15. Applications of sheaf models 456
1. Interpretation of N,Q,Z,R,N. in Sh(Q(T)) 457
2. The axiom of countable choice 461
3. Topologies in sheaves over a cHa 464
4. A derived rule of local continuity 480
5. The monoid model for CS 483
6. A site model for LS 495
7. Notes 500
Exercises 502
Chapter 16. Epilogue 506
1. The role of language and "informal rigour" 506
2. Intuitionistic logic, formalisms, and equality 510
3. Brouwer's theory of the creative subject 517
4. Dummett's anti-realist argument 521
Bibliography 528
Index 556
Index of names 582
List of symbols 592