A General Notion of Realizability
Birkedal, Lars
Bull. Symbolic Logic, Tome 8 (2002) no. 1, p. 266-282 / Harvested from Project Euclid
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.
Publié le : 2002-06-15
Classification: 
@article{1182353873,
     author = {Birkedal, Lars},
     title = {A General Notion of Realizability},
     journal = {Bull. Symbolic Logic},
     volume = {8},
     number = {1},
     year = {2002},
     pages = { 266-282},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1182353873}
}
Birkedal, Lars. A General Notion of Realizability. Bull. Symbolic Logic, Tome 8 (2002) no. 1, pp.  266-282. http://gdmltest.u-ga.fr/item/1182353873/