🚀 go-pugleaf

Date: Tue, 25 Aug 1992 18:06:22 +0200

The following book contains material which is possibly of interest to 
theoretical computer scientists, although it has not been written with 
the computer scientists in mind, but rather for logicians.
A paperback edition of volume I at largely reduced price is now available.

Title: Constructivism in Mathematics, an Introduction
Authors: A.S. Troelstra and D. van Dalen
Publisher: North-Holland Publ. Co., Amsterdam (= Elsevier Science Publishers)
Volume 1: xx + 342 + XIV pages,
	ISBN 0-444-70266-0 (hardback), listprice Dfl.175.-;
	ISBN 0-444-70506-6 (paperback), listprice Dfl.65.-;
Volume 2: xviii + 880 + LII pages,
	ISBN 0-444-70358-6 (hardback), listprice Dfl.175.-.

Contents volume 1:
1 INTRODUCTION
Constructivism - Constructivity - Weak counterexamples - A brief history of
constructivism - Notes - Exercises

2 LOGIC
Natural deduction - Logic with existence predicate - Relationships between
classical and intuitionistic logic - Hilbert-type systems - Kripke semantics -
Completeness for Kripke semantics - Definitional extensions - Notes -
Exercises

3 ARITHMETIC
Informal arithmetic and primitive recursive functions - Primitive recursive
arithmetic - Intuitionistic first-order arithmetic - Algorithms - Some
metamathematics of intuitionistic arithmetic - Elementary analysis and
elementary inductive definitions - Formalization of elementary recursion theory
- Intuitionistic second-order logic and arithmetic - Higher-order logic and
arithmetic - Notes - Exercises

4 NON-CLASSICAL AXIOMS
Preliminaries - Choice axioms - Church's thesis - Realizability - Markov's
principle - Choice sequences and continuity axioms - The fan theorem - Bar
induction and generalized inductive definitions - Uniformity principles and
Kripke's schema - Notes -Exercises

5 REAL NUMBERS
Introduction - Cauchy reals and their ordering - Arithmetic on the reals -
Completeness properties and relativization - Dedekind reals - 
Arithmetic of Dedekind reals and extended reals - Two metamathematical
digressions - Notes - Exercises

6 SOME ELEMENTARY ANALYSIS
Intermediate-value and supremum theorems - Differentiation and integration -
Consequences of continuity and fan theorem - Analysis in Constructive Recursive
Mathematics - Notes - Exercises

BIBLIOGRAPHY, INDEX, LIST OF SYMBOLS

Contents of Volume 2:

7 THE TOPOLOGY OF METRIC SPACES
Basic definitions - Complete,separable metric spaces - Located sets - Complete,
totally bounded spaces - Locally compact spaces - Notes - Exercises

8 ALGEBRA
Identity, apartness and order - Groups - Rings and modules - Linear algebra -
Plynomial rings - Fields and local rings - The fundamental theorem of algebra -
Notes - Exercises

9 FINITE-TYPE ARITHMETIC AND THEORIES OF OPERATORS
Intuitionistic finite-type arithmetic - Normalization, and a term model for
intuitionistic finite-type arithmetic - The theory APP - Models for APP -
Abstract realizability for APP Extensionality and choice - Some
metamathematical operations - Theories of operators and classes - Notes -
Exercises

10 PROOF THEORY OF INTUITIONISTIC LOGIC
Preliminaries - Normalization - The structure of normal derivations - The
dedidability of intuitionistic propositional logic - Other appliccations of
normalization - Conservative addition of predicative classes - Sequent calculi
- N-IQC as a calculus of terms - Notes - Exercises.

11 THE THEORY OF TYPES AND CONSTRUCTIVE SET THEORY
Towards a theory of types - The intensional arithmetical Martin-Loef theory -
Some alternative formulations - The types N_k and reformulation of the E-rules
- The extensional analogue - Embeddings into APP - Extensions of the
arithmetical Martin-Loef type theories - Constructive set theory - Notes
-Exercises

12 CHOICE SEQUENCES
Inroduction - Lawless sequences - The elimination translation - Other notions
of choice sequence - Notes - Exercises

13 SEMANTICAL COMPLETENESS
Beth models - Completeness for intuitionistic validity - Incompleteness results
- Lattices, Heyting algebras and complete Heyting algebras Algebraic semantics
- Omega-sets and structures - Validity as forcing - Postscript on realizability
- Notes - Exercises

14 SHEAVES, SITES AND HIGHER-ORDER LOGIC
Presheaves, sheaves and sheaf-completion - Omega-presheaf and )mega-sheaf
structures - Some notions from category theory - Forcing over sites - Sheaf
models for higher-order logic - Notes - Exercises

15 APPLICATIONS OF SHEAF MODELS
Interpretation of N, Q, Z, R etc. in the sheaves over a topological space - The
axiom of countable choice - Topologies in sheaves over a cHa - A derived rule
of local continuity - The monoid model for CS - A site model for LS - Notes -
Exercises

16 EPILOGUE
The role of language and "informal rigour" - Intuitionistic logic, formalisms,
and equality - Brouwer's theory of the creative subject - Dummett's
anti-realist argument

BIBLIOGRAPHY, INDEX, INDEX OF NAMES, LIST OF SYMBOLS