Switch to: References

Add citations

You must login to add citations.
  1. Elementary Realizability.Zlatan Damnjanovic - 1997 - Journal of Philosophical Logic 26 (3):311-339.
    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 (...)
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • 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.
    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 (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Polynomially Bounded Recursive Realizability.Saeed Salehi - 2005 - Notre Dame Journal of Formal Logic 46 (4):407-417.
    A polynomially bounded recursive realizability, in which the recursive functions used in Kleene's realizability are restricted to polynomially bounded functions, is introduced. It is used to show that provably total functions of Ruitenburg's Basic Arithmetic are polynomially bounded (primitive) recursive functions. This sharpens our earlier result where those functions were proved to be primitive recursive. Also a polynomially bounded schema of Church's Thesis is shown to be polynomially bounded realizable. So the schema is consistent with Basic Arithmetic, whereas it is (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation