(Note: Volume 2 is NOT contained in this eBook.)
These two volumes cover the principal approaches to constructivism in mathematics. They present a thorough, up-to-date introduction to the metamathematics of constructive mathematics, paying special attention to Intuitionism, Markov's constructivism and Martin-Lof's type theory with its operational semantics. A detailed exposition of the basic features of constructive mathematics, with illustrations from analysis, algebra and topology, is provided, with due attention to the metamathematical aspects. Volume 1 is a self-contained introduction to the practice and foundations of constructivism, and does not require specialized knowledge beyond basic mathematical logic. Volume 2 contains mainly advanced topics of a proof-theoretical and semantical nature.
Author(s): Anne S. Troelstra, Dirk van Dalen
Series: Studies in Logic and the Foundations of Mathematics 121
Publisher: North-Holland
Year: 1988
Language: English
Pages: 361
Preface......Page 4
Preliminaries......Page 7
Contents......Page 12
1. Constructivism......Page 13
2. Constructivity......Page 17
3. Weak counterexamples......Page 20
4. A brief history of counstructivism......Page 28
5. Notes......Page 42
Exercises......Page 44
2. Logic......Page 46
1. Natural deduction......Page 47
2. Logic with existence predicate......Page 61
3. Relationships between classical and intuitionistic logic......Page 67
4. Hilbert-type systems......Page 79
5. Kripke semantics......Page 86
6. Completeness for Kripke semantics......Page 98
7. Definitional extensions......Page 104
8. Notes......Page 111
Exercises......Page 114
3. Arithmetic......Page 123
1. Informal arithmetic and primitive recursive functions......Page 124
2. Primitive recursive arithmetic PRA......Page 130
3. Intuitionistic first-order arithmetic HA......Page 136
4. Algorithms......Page 141
5. Some metamathematics of HA......Page 146
6. Elementary analysis and elementary inductive definitions......Page 154
7. Formalization of elementary recursion theory......Page 162
8. Intuitionistic second-order logic and arithmetic......Page 170
9. Higher-order logic and arithmetic......Page 178
10. Notes......Page 184
Exercises......Page 187
4. Non-Classical Axioms......Page 194
1. Preliminaries......Page 195
2. Choice axioms......Page 198
3. Church's thesis......Page 201
4. Realizability......Page 204
5. Markov's principle......Page 212
6. Choice sequences and continuity axioms......Page 215
7. The fan theorem......Page 226
8. Bar induction and generalized inductive definitions......Page 232
9. Uniformity principles and Kripke's schema......Page 243
10. Notes......Page 247
Exercises......Page 251
1. Introduction......Page 259
2. Cauchy reals and their ordering......Page 261
3. Arithmetic on R......Page 268
4. Completeness properties and relativization......Page 274
5. Dedekind reals......Page 278
6. Arithmetic of Dedekind reals and extended reals......Page 285
7. Two metamathematical digressions......Page 288
8. Notes......Page 292
Exercises......Page 294
1. Intermediate-value and supremum theorems......Page 298
2. Differentiation and integration......Page 302
3. Consequences of WC-N and FAN......Page 310
4. Analysis in CRM: consequences of CT_0, ECT_0, MP......Page 314
5. Notes......Page 327
Exercises......Page 329
Bibliography......Page 333
Index......Page 349
List of Symbols......Page 358
