Constructivism in Mathematics, Vol 2

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