Constructivism in Mathematics, Vol 2

Constructivism in Mathematics: Contents Preliminaries7. The Topology of Metric Spaces 1. Basic Definitions 2. Complete, Separable Metric Spaces 3. Located Sets 4. Complete, Totally Bounded Spaces 5. Locally Compact Spaces 6. Notes Exercises8. Algebra 1. Identity, Apartness and Order 2. Groups 3. Rings and Modules 4. Linear Algebra 5. Polynomial Rings 6. Fields and Local Rings 7. The Fundamental Theorem of Algebra 8. Notes Exercises9. Finite-Type Arithmetic and Theories of Operators 1. Intuitionistic Finite-Type Arithmetic 2. Normalization, and a Term Model For HA¿ 3. The Theory APP 4. Models for APP 5. Abstract Realizability in APP 6. Extensionality and Choice in APP and HA¿ 7. Some Metamathematical Applications 8. Theories of Operators and Classes 9. Notes Exercises10. Proof Theory of Intuitionistic Logic 1. Preliminaries 2. Normalization 3. The Structure of Normal Derivations of N-IQCE 4. The Decidability of IPC 5. Other Applications of Normalization 6. Conservative Addition of Predicative Classes 7. Sequent Calculi 8. N-IQC as a Calculus of Terms 9. Notes Exercises11. The Theory of Types and Constructive Set Theory 1. Towards a Theory of Types 2. The Theory MLi0 3. Some Alternative Formulations of MLi0 4. The Types Nk and Reformulation of the E-Rules 5. The Theory ML0 6. Embeddings into APP 7. Extensions of MLi0 and ML0 8. Constructive Set Theory 9. Notes Exercises12. Choice Sequences 1. Introduction 2. Lawless Sequences 3. The Elimination Translation for the Theory LS 4. Other Notions of Choice Sequence 5. Notes Exercises13. Semantical Completeness 1. Beth Models 2. Completeness for Intuitionistic Validity 3. Incompleteness Results 4. Lattices, Heyting Algebras and Complete Heyting Algebras 5. Algebraic Semantics for IPC 6. O-Sets and Structures 7. Validity as Forcing 8. Postscript on Realizability 9. Notes Exercises14. Sheaves, Sites and Higher-Order Logic 1. Presheaves, Sheaves and Sheaf-Completion 2. O-Presheaf and O-Sheaf Structures 3. Some Notions from Category Theory 4. Forcing Over Sites 5. Sheaf Models for Higher-Order Logic 6. Notes Exercises15. Applications of Sheaf Models 1. Interpretation of N, Q, Z, R,N in Sh(O(T)) 2. The Axiom of Countable Choice 3. Topologies in Sheaves Over a cHa 4. A Derived Rule of Local Continuity 5. The Monoid Model for CS 6. A Site Model for LS 7. Notes Exercises16. Epilogue 1. The Role of Language and "Informal Rigour" 2. Intuitionistic Logic, Formalisms, and Equality 3. Brouwer's Theory of the Creative Subject 4. Dummett's Anti-Realist ArgumentBibliographyIndexIndex of NamesList of Symbols