Intuitionistically provable recursive well-orderings
type: Item
instance of: scholarly article
title: Intuitionistically provable recursive well-orderings
zbMATH Open document ID: 0615.03046
DOI: 10.1016/0168-0072(86)90004-7
author: Harvey M. Friedman
author: Andre Scedrov
published in: Annals of Pure and Applied Logic
publication date: 1986-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F55
Mathematics Subject Classification ID: 03F30
zbMATH DE Number: 3995670
zbMATH Keywords: intuitionistic number theory with recursive infinitary rules
zbMATH Keywords: \(HA^ *\)
zbMATH Keywords: transfinite induction
zbMATH Keywords: well-founded
reviewed by: Georg Kreisel
MaRDI profile type: Publication
full work available at URL: 0168-0072(86)90004-7
OpenAlex ID: W2068211235
cites work: Q4179016
cites work: Arithmetic transfinite induction and recursive well-orderings
cites work: Q3659778
cites work: Degrees of Unsolvability. (AM-55)
cites work: Q5183475
Recommended article: Q3801546
Recommended article: Well-Ordering Principles in Proof Theory and Reverse Mathematics
Recommended article: Proof-theoretic strengths of the well-ordering principles
Recommended article: Arithmetic transfinite induction and recursive well-orderings
Recommended article: Q5403201
Recommended article: Q4844236
Recommended article: AN AXIOMATIC THEORY OF WELL-ORDERINGS
Recommended article: Well ordering principles for iterated \(\Pi^1_1\)-comprehension
Recommended article: A Note on (Meta)predicative Wellordering Proofs
Recommended article: Takeuti's Well-ordering Proof
description: scientific article; zbMATH DE number 3995670