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)|
|Through your library||Configure|
Similar books and articles
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.
Added to index2009-01-28
Total downloads7 ( #134,900 of 556,808 )
Recent downloads (6 months)0
How can I increase my downloads?