Troelstra / Dalen Constructivism in Mathematics, Vol 2

1. Auflage 2014
ISBN: 978-0-08-095510-0
Verlag: Elsevier Science & Techn.
Format: PDF
Kopierschutz: 1 - PDF Watermark

E-Book, Englisch, Band Volume 123, 140 Seiten, Web PDF

Reihe: Studies in Logic and the Foundations of Mathematics

Studies in Logic and the Foundations of Mathematics, Volume 123: Constructivism in Mathematics: An Introduction, Vol. II focuses on various studies in mathematics and logic, including metric spaces, polynomial rings, and Heyting algebras. The publication first takes a look at the topology of metric spaces, algebra, and finite-type arithmetic and theories of operators. Discussions focus on intuitionistic finite-type arithmetic, theories of operators and classes, rings and modules, linear algebra, polynomial rings, fields and local rings, complete separable metric spaces, and located sets. The text then examines proof theory of intuitionistic logic, theory of types and constructive set theory, and choice sequences. The book elaborates on semantical completeness, sheaves, sites, and higher-order logic, and applications of sheaf models. Topics include a derived rule of local continuity, axiom of countable choice, forcing over sites, sheaf models for higher-order logic, and complete Heyting algebras. The publication is a valuable reference for mathematicians and researchers interested in mathematics and logic.

Autoren/Hrsg.

Troelstra, A. S.

Dalen, D. van

Inhaltsverzeichnis

1;Front Cover;1
2;Constructivism in Mathematics: An Introduction;4
3;Copyright Page;5
4;Table of Contents;10
5;Dedication;6
6;Constructivism in Mathematics: Contents;8
7;Preliminaries;14
8;Chapter 7. The topology of metric spaces;20
8.1;1. Basic definitions;20
8.2;2. Complete, separable metric spaces;25
8.3;3. Located sets;33
8.4;4. Complete, totally bounded spaces;38
8.5;5. Locally compact spaces;46
8.6;6. Notes;51
8.7;Exercises;54
9;Chapter 8. Algebra;58
9.1;1. Identity, apartness and order;58
9.2;2. Groups;63
9.3;3. Rings and modules;74
9.4;4. Linear algebra;82
9.5;5. Polynomial rings;90
9.6;6. Fields and local rings;105
9.7;7. The fundamental theorem of algebra;109
9.8;8. Notes;113
9.9;Exercises;114
10;Chapter 9. Finite-type arithmetic and theories of operators;118
10.1;1. Intuitionistic finite-type arithmetic;119
10.2;2. Normalization, and a term model for HA.;133
10.3;3. The theory APP;147
10.4;4. Models for APP;155
10.5;5. Abstract realizability in APP;166
10.6;6. Extensionality and choice in APP and HA.;170
10.7;7. Some metamathematical applications;176
10.8;8. Theories of operators and classes;187
10.9;9. Notes;192
10.10;Exercises;195
11;Chapter 10. Proof theory of intuitionistic logic;202
11.1;1. Preliminaries;202
11.2;2. Normalization;207
11.3;3. The structure of normal derivations of N-IQCE;213
11.4;4. The decidability of IPC;216
11.5;5. Other applications of normalization;219
11.6;6. Conservative addition of predicative classes;223
11.7;7. Sequent calculi;225
11.8;8. N-IQC as a calculus of terms;231
11.9;9. Notes;238
11.10;Exercises;240
12;Chapter 11. The theory of types and constructive set theory;246
12.1;1. Towards a theory of types;246
12.2;2. The theory MVio;250
12.3;3. Some alternative formulations of MVio;264
12.4;4. The types Nk and reformulation of the E-rules;267
12.5;5. The theory MLo;278
12.6;6. Embeddings into APP;283
12.7;7. Extensions of MLiq and MLo;286
12.8;8. Constructive set theory;294
12.9;9. Notes;307
12.10;Exercises;310
13;Chapter 12. Choice sequences;314
13.1;1. Introduction;314
13.2;2. Lawless sequences;320
13.3;3. The elimination translation for the theory LS;333
13.4;4. Other notions of choice sequence;340
13.5;5. Notes;347
13.6;Exercises;349
14;Chapter 13. Semantical completeness;352
14.1;1. Beth models;352
14.2;2. Completeness for intuitionistic validity;360
14.3;3. Incompleteness results;369
14.4;4. Lattices, Heyting algebras and complete Heyting algebras;375
14.5;5. Algebraic semantics for IPC;380
14.6;6. .-sets and structures;384
14.7;7. Validity as forcing;394
14.8;8. Postscript on realizability;399
14.9;9. Notes;404
14.10;Exercises;408
15;Chapter 14. Sheaves, sites and higher-order logic;412
15.1;1. Presheaves, sheaves and sheaf-completion;413
15.2;2. .-presheaf and .-sheaf structures;422
15.3;3. Some notions from category theory;426
15.4;4. Forcing over sites;434
15.5;5. Sheaf models for higher-order logic;442
15.6;6. Notes;450
15.7;Exercises;452
16;Chapter 15. Applications of sheaf models;456
16.1;1. Interpretation of N,Q,Z,R,N. in Sh(Q(T));457
16.2;2. The axiom of countable choice;461
16.3;3. Topologies in sheaves over a cHa;464
16.4;4. A derived rule of local continuity;480
16.5;5. The monoid model for CS;483
16.6;6. A site model for LS;495
16.7;7. Notes;500
16.8;Exercises;502
17;Chapter 16. Epilogue;506
17.1;1. The role of language and "informal rigour";506
17.2;2. Intuitionistic logic, formalisms, and equality;510
17.3;3. Brouwer's theory of the creative subject;517
17.4;4. Dummett's anti-realist argument;521
18;Bibliography;528
19;Index;556
20;Index of names;582
21;List of symbols;592