Minimal realizability of intuitionistic arithmetic and elementary analysis
Journal of Symbolic Logic 60 (4):1208-1241 (1995)
| Abstract | A new method of "minimal" realizability is proposed and applied to show that the definable functions of Heyting arithmetic (HA)--functions f such that HA $\vdash \forall x\exists!yA(x, y)\Rightarrow$ for all m, A(m, f(m)) is true, where A(x, y) may be an arbitrary formula of L(HA) with only x, y free--are precisely the provably recursive functions of the classical Peano arithmetic (PA), i.e., the $ -recursive functions. It is proved that, for prenex sentences provable in HA, Skolem functions may always be chosen to be $ -recursive. The method is extended to intuitionistic finite-type arithmetic, HA ω 0 , and elementary analysis. Generalized forms of Kreisel's characterization of the provably recursive functions of PA and of the no-counterexample-interpretation for PA are consequently derived | |||||||||
| Keywords | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,865 |
| External links |
|
| Through your library | Configure |
Ulrich Kohlenbach (1999). On the No-Counterexample Interpretation. Journal of Symbolic Logic 64 (4):1491-1511.
Daniel Dzierzgowski (1995). Models of Intuitionistic TT and N. Journal of Symbolic Logic 60 (2):640-653.
Stephen Bellantoni & Martin Hofmann (2002). A New "Feasible" Arithmetic. Journal of Symbolic Logic 67 (1):104-116.
M. Beeson & A. Ščedrov (1984). Church's Thesis, Continuity, and Set Theory. Journal of Symbolic Logic 49 (2):630-643.
Wolfgang Burr (2000). Fragments of Heyting Arithmetic. Journal of Symbolic Logic 65 (3):1223-1240.
Zlatan Damnjanovic (1994). Strictly Primitive Recursive Realizability, I. Journal of Symbolic Logic 59 (4):1210-1227.
Jaap Van Oosten (1990). Lifschitz' Realizability. Journal of Symbolic Logic 55 (2):805 - 821.
Zlatan Damnjanovic (1997). Elementary Realizability. Journal of Philosophical Logic 26 (3):311-339.
Monthly downloads |
Added to index2009-01-28Total downloads7 ( #134,900 of 556,808 )Recent downloads (6 months)0How can I increase my downloads? |

