Intuitionistically provable recursive well-orderings

&
Annals of Pure and Applied Logic 30 (2):165-171 (1986)
  Copy   BIBTEX

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 property

Categories

Keywords

Reprint years

DOI

10.1016/0168-0072(86)90004-7

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 100,793

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

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.
Ordinal analyses for monotone and cofinal transfinite inductions.Kentaro Sato - 2020 - Archive for Mathematical Logic 59 (3-4):277-291.
Markov's Rule revisited.Daniel Leivant - 1990 - Archive for Mathematical Logic 30 (2):125-127.
Provable equality in primitive recursive arithmetic with and without induction.Harvey Friedman - 1975 - Pacific Journal of Mathematics 57 (2):379-392.
Elementary descent recursion and proof theory.Harvey Friedman & Michael Sheard - 1995 - Annals of Pure and Applied Logic 71 (1):1-45.
Variation on a theme of Schutte.D. Probst & G. Jager - 2004 - Mathematical Logic Quarterly 50 (3):258.
Transfinite induction within Peano arithmetic.Richard Sommer - 1995 - Annals of Pure and Applied Logic 76 (3):231-289.
Strictly Primitive Recursive Realizability, II. Completeness with Respect to Iterated Reflection and a Primitive Recursive $\omega$ -Rule.Zlatan Damnjanovic - 1998 - Notre Dame Journal of Formal Logic 39 (3):363-388.
Generalizations of the Kruskal-Friedman theorems.L. Gordeev - 1990 - Journal of Symbolic Logic 55 (1):157-181.
Induction rules, reflection principles, and provably recursive functions.Lev D. Beklemishev - 1997 - Annals of Pure and Applied Logic 85 (3):193-242.

Analytics

Added to PP
2014-01-16

Downloads
25 (#864,595)

6 months
8 (#528,772)

Historical graph of downloads
How can I increase my 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.

Add more citations

References found in this work

Degrees of Unsolvability.Gerald E. Sacks - 1966 - Princeton University Press.
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.

Add more references