Intuitionistically provable recursive well-orderings (Q1820780)

The authors extend their result in Adv. Math. 56, 283-294 (1985; Zbl 0585.03031) to a wider class of (formally) intuitionistic systems by means of a different proof. Let TI(P,R), for demonstrably primitive recursive R and a free predicate variable P, express transfinite induction on R applied to P. Then there is a specific arithmetic A independent of R s.t., if TI[P/A] is derivable in any of the systems considered, so is TI itself; thus R is in fact well-founded. The authors stress the striking contrast to the case of classical systems, which was topical 35 years ago. To the reviewer their result suggests so to speak new ''programs'' for (intuitionistic) logic, which has proved unrewarding for its own (foundational) aims, as follows. The formula A above is viewed as a kind of analogue to transcendental numbers \(\alpha\) in algebra, with the - class of - formulae TI(P,R) corresponding to equations, say, E, with variable x (and derivability to validity). Here E holds generally, if E[x/\(\alpha\) ] holds. The ''program'' looks for classes C of formulae F other than TI and some specific \(A_ c\) s.t., for F in C, F is derivable provided only \(F[P/A_ c]\) is; in the first place for intuitionistic logic, but perhaps also for classical logic (for suitable C). In their opening paragraph the authors say, perhaps fairly, that the (broad) issues of TI in classical arithmetic were discussed (adequately) in the old literature. But the particular results that they state were found by H. Friedman in the late sixties after he had been informed of those issues, and circulated (privately), but apparently not published.