Bulletin of Symbolic Logic 8 (2):266-282 (2002)
We present a general notion of realizability encompassing both standard Kleene style realizability over partial combinatory algebras and Kleene style realizability over more general structures, including all partial cartesian closed categories. We shown how the general notion of realizability can be used to get models of dependent predicate logic, thus obtaining as a corollary (the known result) that the category Equ of equilogical spaces models dependent predicate logic. Moreover, we characterize when the general notion of realizability gives rise to a topos, i.e., a model of impredicative intuitionistic higher-order logic
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
On the Interpretation of Intuitionistic Number Theory.S. C. Kleene - 1945 - Journal of Symbolic Logic 10 (4):109-124.
Colimit Completions and the Effective Topos.Edmund Robinson & Giuseppe Rosolini - 1990 - Journal of Symbolic Logic 55 (2):678-699.
Citations of this work BETA
No citations found.
Similar books and articles
A Liberal Conception of Multiple Realizability.Eric Funkhouser - 2007 - Philosophical Studies 132 (3):467-494.
A Survey of Propositional Realizability Logic.Valery Plisko - 2009 - Bulletin of Symbolic Logic 15 (1):1-42.
Local Realizability Toposes and a Modal Logic for Computability.Steve Awodey, Lars Birkedal & Dana Scott - unknown
Extension of Lifschitz' Realizability to Higher Order Arithmetic, and a Solution to a Problem of F. Richman.Oosten Jaap Van - 1991 - Journal of Symbolic Logic 56 (3):964 - 973.
Partial Combinatory Algebras of Functions.Jaap van Oosten - 2011 - Notre Dame Journal of Formal Logic 52 (4):431-448.
Bounded Modified Realizability.Fernando Ferreira & Ana Nunes - 2006 - Journal of Symbolic Logic 71 (1):329 - 346.
Added to index2009-01-28
Total downloads9 ( #458,269 of 2,158,886 )
Recent downloads (6 months)1 ( #354,157 of 2,158,886 )
How can I increase my downloads?