The Foundations of Intuitionistic Mathematics (Studies in Logic and the Foundations of Mathematics)North-Holland Pub. Co | 1965 | 206 pages | ISBN : B0006CJJ5Y | pdf | 9.2MB
Chapters I, II, and IV are by Kleene; Chapter III is by Vesley.
Chapter I is by far the best introduction to intuitionistic logic which is at present available for a mathematical logician. It deals with analysis, including (i) the axiom of choice (AC): $\forall x\exists yA(x,y)\supset\exists\alpha\forall xA[x,\alpha(x)]$ for arbitrary analytic $A$, (ii) the so-called bar theorem or bar induction (BI), which asserts essentially that for a partial ordering $<$, if $<$ is well founded in the sense that all descending sequences are finite, i.e., $\forall\alpha\exists x¬\alpha(x+1)<\alpha(x)$, then transfinite induction can be applied to $<$, and (iii), above all, the continuity principle (C, here called Brouwer's principle): for all analytic $A$, $\forall\alpha\exists xA(\alpha,x)\supset\forall\alpha\exists x\exists y\forall\beta\,[\overline\alpha(y)=\overline\beta(y)\supset A(\beta,x)]$. The function variables $\alpha$, $\beta$ are intended to be interpreted as free choice sequences of natural numbers. Whatever doubts one may have about the exact nature of these objects, it is clear that (C) and (AC) hold for them, and the author gives a clear enough explanation of (BI) to leave no doubt that it is worth considering. What makes analysis so much better an introduction than intuitionistic propositional or predicate logic is this: No subtle distinctions, far-fetched ``interpretations'', or dubious objections to classical mathematics are needed to explain its interest; (C) is simply false if the logical symbols are interpreted classically, e.g., if $A(\alpha,x)$ is $\alpha(x)=0\vee\forall y[\alpha(y)\neq 0]$, elaborate ``consistency'' proofs are needed, while the basic intuitionistic notions ensure consistency as swiftly as the notion of a set of natural numbers ensures the consistency of classical arithmetic. Incidentally, even if some pages, e.g., p. 27, do not look particularly attractive to the eye, mathematically the formal development is very economical and elegant.
Chapter II gives, essentially, reductions of the system of analysis to analysis without (C), in particular, to principles which are also valid for the classical interpretation of the logical symbols. Analogously to Kleene's original realisability interpretation [Introduction to metamathematics,\/ Van Nostrand, New York, 1952], with each formula $A$ are associated formulae $\exists\alpha A_1(\alpha)$, $\exists\alpha A_2(\alpha)$, respectively, where $A_1$, $A_2$ are built up from the predicates $R_1(\alpha)$ ($\alpha$ is a partial functional), $R_2{}^n(\alpha)$ ($\alpha$ is the representing function of a non-extensional continuous functional of type $n$, in the sense of the reviewer [J. Symbolic Logic 27 (1962), 139--158; MR0161796 (28 #5000)]) by means of the logical symbols $\forall$, $\supset$,&only, i.e., without $\exists$ and $\vee$. It is shown that the axioms of Chapter I hold not only for the intended interpretation, but for the associated translations too, and then without appeal to (C). The author's second translation of $A$ is introduced to establish that, even for primitive recursive $R$, $¬¬\exists xR(x)\supset\exists xR(x)$ is not generally derivable, as shown for a weaker system l.c. The underlying idea of the new realisability differs essentially from the old one: even if $\forall x\exists yA(x,y)$ contains no free variable, it is not required that there be a constructive function $f$ satisfying $\forall xA[x,f(x)]$, but only some $\alpha$. Consequently, on this interpretation one has no immediate reason to assert Church's thesis (T) in the form $\forall x\exists yA(x,y)\supset\exists e{R(e) &\,\forall xA[x,{e}(x)]}$, where $R(e)$ states that $e$ is the index of the recursive function ${e}$, and if the translations $\exists\alpha T_1(\alpha)$ or $\exists\alpha T_2(\alpha)$ of Church's thesis are interpreted classically, they are in general false. {It is, of course, interesting that intuitionistic analysis as formulated here formally leaves room for these various interpretations. But in the reviewer's opinion this interest is limited because the interpretations do not extend when the language of analysis is extended, for example, to include additional variables for constructive functions and evident axioms formulated in the extended language, e.g., 2.521 in the reviewer's book [Mathematical logic. Lectures on modern mathematics,\/ Vol. III, pp. 95--195, Wiley, New York, 1965; MR0177866 (31 #2124)]. Actually, proof-theoretically the author's interpretations have some defects even when applied to the restricted language, since certain underivability results, e.g., 11.10$^{\text C}$ on p. 131, are obtained by non-constructive means, though they hold intuitionistically (precisely, are provable in elementary arithmetic from the consistency of the author's system without C). Some results are unnecessarily crude, e.g., 9.12$^{\text C}$, p. 116; the system of analysis is interpreted with the fan theorem (FT) in place of (BI) by use of (the classical collection of) arithmetic functions, i.e., the first level of the ramified hierarchy, whose ordinal is $\varepsilon_1$ [Schütte, Beweistheorie,\/ Springer, Berlin, 1960; MR0118665 (22 #9438)]. But, in fact, (FT) is finitistically reducible to first order arithmetic whose ordinal is $\varepsilon_0$, by the reviewer's paper cited above. Oddly, the author nowhere proves the obvious fact that (BI) is stronger in the sense that induction up to $\varepsilon_0$ (and much larger ordinals) can be formally proved by (BI), though he refers to this fact on p. 120, l. 12.}
Chapter III carries out much of Brouwer's analysis within Kleene's system. By the nature of the operation a good deal of it is familiar. But, to the reviewer, it is an interesting empirical discovery that so much in Brouwer's publications is easily formulated within the restricted language considered. For instance, since the notion of constructive function is obviously a basic concept, it might have been necessary to use it explicitly in the formalisation. (It is of course possible, as happens often in formalisations, that minor results, which would need an extended language, or new axioms, have been ignored.)
In Chapter IV the author considers some more isolated results of Brouwer on order in the continuum which were in fact ignored in Chapter III. Writing $\xi\overset 0\to=0$ for (the real number) $\xi$ is $0$, and $\xi#0$ for $\exists n(|\xi|>n^{-1})$, Brouwer asserts $¬\forall\xi(¬\xi\overset 0\to=0\supset\xi#0)$. His argument is certainly formally weak, cf. top of p. 176. But the assertion is not too startling if one remembers the intended meaning, namely, the absurdity of assuming a constructive proof of $\forall\xi(¬\xi\overset 0\to=0\supset\xi#0)$, and of course not the existence of a counter-example. Further analysis of this intended meaning may show that Brouwer's argument is not altogether off the mark, contrary to the author's opinion (p. 175, ll. -9, -8). For instance, by the reviewer's book, 2.524, to establish Brouwer's assertion it would be more than sufficient to find a spread of real numbers in which all $\xi$ defined by a constructive law are #0, but not all free choice sequences $\xi$. The author shows that $\forall\xi(¬\xi\overset 0\to=0\supset\xi#0)$ is not derivable in his system (by essential use of the second realisability interpretation), but may be consistently added to it. Evidently this leaves untouched the question whether it may be so added to an extended system valid for the intended interpretation. Chapter IV contains an instructive analysis of several other results on order.
{In the reviewer's opinion, the only thing that is really wrong with this excellent book is its title. In it the authors formulate the formal principles of intuitionistic mathematics and say as little as possible about its foundations. Specifically, the logical operations are taken as primitive, at least $\forall$, $&$ and $\supset$, reducing $\exists$ to particular occurrences in $R_1$, $R_2{}^n$ above (and defining $\vee$ in terms of $\exists$ on p. 119). At the present time the main job of foundations of intuitionistic mathematics is to analyse the meanings of these operations (and other operations of higher type).
