Intuitionistically provable recursive well-orderings
Annals of Pure and Applied Logic 30 (2):165-171 (1986)
Abstract
We consider intuitionistic number theory with recursive infinitary rules . Any primitive recursive binary relation for which transfinite induction schema is provable is in fact well founded. Its ordinal is less than ε 0 if the transfinite induction schema is intuitionistically provable in elementary number theory. These results are provable intuitionistically. In fact, it suffices to consider transfinite induction with respect to one particular number-theoretic propertyDOI
10.1016/0168-0072(86)90004-7
My notes
Similar books and articles
A non-well-founded primitive recursive tree provably well-founded for co-r.e. sets.Arnold Beckmann - 2002 - Archive for Mathematical Logic 41 (3):251-257.
A construction for recursive linear orderings.C. J. Ash - 1991 - Journal of Symbolic Logic 56 (2):673-683.
Degrees of orderings not isomorphic to recursive linear orderings.Carl G. Jockusch & Robert I. Soare - 1991 - Annals of Pure and Applied Logic 52 (1-2):39-64.
Up to Equimorphism, Hyperarithmetic Is Recursive.Antonio Montalbán - 2005 - Journal of Symbolic Logic 70 (2):360 - 378.
A recursion principle for linear orderings.Juha Oikkonen - 1992 - Journal of Symbolic Logic 57 (1):82-96.
Recursive automorphisms of recursive linear orderings.Steven Schwarz - 1984 - Annals of Pure and Applied Logic 26 (1):69-73.
Some observations on intuitionistically elementary properties of linear orderings.Wim Veldman & Michaël Janssen - 1990 - Archive for Mathematical Logic 29 (3):171-185.
Some results on cut-elimination, provable well-orderings, induction and reflection.Toshiyasu Arai - 1998 - Annals of Pure and Applied Logic 95 (1-3):93-184.
Review: Toshiyasu Arai, Some Results on Cut-Elimination, Provable Well-Orderings, Induction and Reflection. [REVIEW]Jeremy Avigad - 2001 - Bulletin of Symbolic Logic 7 (1):77-78.
Arithmetical interpretations of dynamic logic.Petr Hájek - 1983 - Journal of Symbolic Logic 48 (3):704-713.
On provable recursive functions.H. B. Enderton - 1968 - Notre Dame Journal of Formal Logic 9 (1):86-88.
Recursive well-founded orderings.Keh-Hsun Chen - 1978 - Annals of Mathematical Logic 13 (2):117-147.
Analytics
Added to PP
2014-01-16
Downloads
10 (#890,924)
6 months
1 (#454,876)
2014-01-16
Downloads
10 (#890,924)
6 months
1 (#454,876)
Historical graph of downloads
Citations of this work
Well-foundedness in Realizability.M. Hofmann, J. van Oosten & T. Streicher - 2006 - Archive for Mathematical Logic 45 (7):795-805.
References found in this work
Metamathematical Investigation of Intuitionistic Arithmetic and Analysis.Anne S. Troelstra - 1973 - New York: Springer.
A variant to Hilbert's theory of the foundations of arithmetic.G. Kreisel - 1953 - British Journal for the Philosophy of Science 4 (14):107-129.
