Incompleteness in intuitionistic metamathematics (Q1182705)

This leisurely article is of interest to at least 2 classes of readers. (1) Those committed to the author's (philosophical) tradition will welcome his truly philosophical exposition of some metamathematical results, which have been available for some 30 years, but not (presented) in his style. This views (in)completeness as a fundamental property; with the (tacit) assumption that study of such properties is a \textit{substitute} for ordinary knowledge of the area concerned, here, of reasoning for which the rules considered are (in)complete. Fittingly, a particular set of (logical) rules and a particular, model-theoretic semantics are privileged, and pursued relentlessly. (2) Those --- not committed to, but --- interested in (1) can use the author's presentation to examine alternatives; for example, the rule of thumb that, generally, (philosophically) fundamental properties are foundational in the sense of contemporary mathematics: They are to be remembered, but \textit{not} to be belaboured (theoretically or otherwise; elaboration running the risk of distracting from their most rewarding uses). Thus, quite rough knowledge of (in)completeness is enough for the following: (a) Analogies, transfer principles, come with completeness; cf. generalizations of first-order theorems \(T\) about \(\mathbb{R}\) to all real closed fields, where \(T\) may be proved by, say, (incomplete!) topological methods. (b) Incompleteness of rules \(\rho\) is a prerequisite for a general answer to the question: What more do we know from provability by means of \(\rho\) than from (mere) truth? Whether or not the risk mentioned actually occurs is, of course, a matter of experience, and the present paper settles this (positively). -- - More specifically, for (2), the or, at least, a first order of business is to determine limitations, if any, on the tacit assumptions in (1) of (i) some overall need for any (explicit) semantics or (ii) its focus on particular privileged (= intuitionistic) rules. As to (i), the material at the end of \S3 on p. 339 has long been seen as an example of --- using basis results for --- conclusive (in)completeness results without any explicit semantics at all; fittingly, the author's presentation is clumsy. As to (ii), on pp. 329-330 he ignores the single most compelling contribution of logic to the common-or-garden variety of construtive concerns, namely, the unwinding of \textit{classical} proofs of \(\Sigma^ 0_ 1\) theorems [cf. p. 507 of Bull. Lond. Math. Soc. 22 (1990)], an application, by this reviewer, of (2) to the work of \textit{A. S. Troelstra} and \textit{D. van Dalen} [Constructivism in mathematics: an introduction (1988; Zbl 0653.03040 and Zbl 0661.03047)].