Switch to: Citations

References in:

Polynomially Bounded Recursive Realizability

Notre Dame Journal of Formal Logic 46 (4):407-417 (2005)

Add references

You must login to add references.

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.details The notion of strictly primitive recursive realizability is further investigated, and the realizable prenex sentences, which coincide with primitive recursive truths of classical arithmetic, are characterized as precisely those provable in transfinite progressions over a fragment of intuitionistic arithmetic. The progressions are based on uniform reflection principles of bounded complexity iterated along initial segments of a primitive recursively formulated system of notations for constructive ordinals. A semiformal system closed under a primitive recursively restricted -rule is described and proved equivalent to (...) Download Export citation Bookmark 2 citations
How to extend the semantic tableaux and cut-free versions of the second incompleteness theorem almost to Robinson's arithmetic Q.Dan E. Willard - 2002 - Journal of Symbolic Logic 67 (1):465-496.details Let us recall that Raphael Robinson's Arithmetic Q is an axiom system that differs from Peano Arithmetic essentially by containing no Induction axioms [13], [18]. We will generalize the semantic-tableaux version of the Second Incompleteness Theorem almost to the level of System Q. We will prove that there exists a single rather long Π 1 sentence, valid in the standard model of the Natural Numbers and denoted as V, such that if α is any finite consistent extension of Q + (...) Download Export citation Bookmark 12 citations
Elementary realizability.Zlatan Damnjanovic - 1997 - Journal of Philosophical Logic 26 (3):311-339.details A realizability notion that employs only Kalmar elementary functions is defined, and, relative to it, the soundness of EA-(Π₁⁰-IR), a fragment of Heyting Arithmetic (HA) with names and axioms for all elementary functions and induction rule restricted to Π₁⁰ formulae, is proved. As a corollary, it is proved that the provably recursive functions of EA-(Π₁⁰-IR) are precisely the elementary functions. Elementary realizability is proposed as a model of strict arithmetic constructivism, which allows only those constructive procedures for which the amount (...) Download Export citation Bookmark 3 citations
Strictly primitive recursive realizability, I.Zlatan Damnjanovic - 1994 - Journal of Symbolic Logic 59 (4):1210-1227.details A realizability notion that employs only primitive recursive functions is defined, and, relative to it, the soundness of the fragment of Heyting Arithmetic (HA) in which induction is restricted to Σ 0 1 formulae is proved. A dual concept of falsifiability is proposed and an analogous soundness result is established for a further restricted fragment of HA. Download Export citation Bookmark 4 citations
On the scheme of induction for bounded arithmetic formulas.A. J. Wilkie & J. B. Paris - 1987 - Annals of Pure and Applied Logic 35 (C):261-302.details Download Export citation Bookmark 96 citations
Minimal realizability of intuitionistic arithmetic and elementary analysis.Zlatan Damnjanovic - 1995 - Journal of Symbolic Logic 60 (4):1208-1241.details 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 (...) Download Export citation Bookmark 4 citations
Basic Predicate Calculus.Wim Ruitenburg - 1998 - Notre Dame Journal of Formal Logic 39 (1):18-46.details We establish a completeness theorem for first-order basic predicate logic BQC, a proper subsystem of intuitionistic predicate logic IQC, using Kripke models with transitive underlying frames. We develop the notion of functional well-formed theory as the right notion of theory over BQC for which strong completeness theorems are possible. We also derive the undecidability of basic arithmetic, the basic logic equivalent of intuitionistic Heyting Arithmetic and classical Peano Arithmetic. Download Export citation Bookmark 17 citations
Provably total functions of Basic Arithemtic.Saeed Salehi - 2003 - Mathematical Logic Quarterly 49 (3):316.details It is shown that all the provably total functions of Basic Arithmetic BA, a theory introduced by Ruitenburg based on Predicate Basic Calculus, are primitive recursive. Along the proof a new kind of primitive recursive realizability to which BA is sound, is introduced. This realizability is similar to Kleene's recursive realizability, except that recursive functions are restricted to primitive recursives. Download Export citation Bookmark 3 citations
Arithmetic complexity of the predicate logics of certain complete arithmetic theories.Valery Plisko - 2001 - Annals of Pure and Applied Logic 113 (1-3):243-259.details It is proved in this paper that the predicate logic of each complete constructive arithmetic theory T having the existential property is Π1T-complete. In this connection, the techniques of a uniform partial truth definition for intuitionistic arithmetic theories is used. The main theorem is applied to the characterization of the predicate logic corresponding to certain variant of the notion of realizable predicate formula. Namely, it is shown that the set of irrefutable predicate formulas is recursively isomorphic to the complement of (...) Download Export citation Bookmark 5 citations

1