Preface
This monograph grew out of lectures I gave at the universities of Aarhus and Stockholm in the period 1966-1968. The aim of these lectures was to introduce mathematicians with no background in logic into the circle of ideas which are known as intuitionistic or constructive and also to present some work of my own. I have added an introduction where I describe in logical terms the constructive attitude I have taken. It may equally well be read as an appendix.
Author(s): Per Martin-Löf
Publisher: Almqvist & Wiksell
Year: 1970
Language: English
Pages: 109
Title page
Preface
Contents
Introduction
Chapter 1. Recursive functions
1. Constructive objects
2. Canonical systems
3. Recursively enumerable sets and relations
4. The equation calculus
5. Turing machines
6. Church’s thesis
7. The universal system
8. Enumeration theorem for partial recursive functions
9. Iteration theorems
10. Recursive inseparability
11. Kleene’s fixed point theorem
Chapter 2. Elementary constructive analysis
12. Neighbourhoods, approximations and constructive points
13. Richard’s paradox and the non enumerability of the continuum
14. Computable real numbers
15. Undecidability results for computable real numbers
16. Specker’s sequence
17. Open and closed sets
18. Heine-Borel covering theorem
19. Located closed sets
20. Inner and outer limit sets
21. Baire’s category theorem
22. Partial recursive functionals
23. Maximal recursive functionals
24. Two theorems of classical function theory
Chapter 3. Ordinal numbers and Borel sets
25. Definition of the ordinals of the second number class
26. Equality and order relations between ordinal numbers
27. Non enumerability of the second number class
28. Open sets in the Baire space
29. Brouwer’s fan theorem
30. Borel sets
31. A constructive version of Gödel’s completeness theorem
32. Completeness of second order logic with cut
Chapter 4. Measure theory
33. Extension of a measure and its basic properties
34. Measurable and non measurable open sets. Brouwer’s theorem
35. Sets of measure zero
References
Index
