A general notion of realizability

Bulletin of Symbolic Logic 8 (2):266-282 (2002)
  Copy   BIBTEX

Abstract

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

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,612

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Herbrandized modified realizability.Gilda Ferreira & Paulo Firmino - 2024 - Archive for Mathematical Logic 63 (5):703-721.
Extensional realizability.Jaap van Oosten - 1997 - Annals of Pure and Applied Logic 84 (3):317-349.
Partial Combinatory Algebras of Functions.Jaap van Oosten - 2011 - Notre Dame Journal of Formal Logic 52 (4):431-448.
Relative and modified relative realizability.Lars Birkedal & Jaap van Oosten - 2002 - Annals of Pure and Applied Logic 118 (1-2):115-132.
Lifschitz' realizability.Jaap van Oosten - 1990 - Journal of Symbolic Logic 55 (2):805-821.
Realizing Brouwer's sequences.Richard E. Vesley - 1996 - Annals of Pure and Applied Logic 81 (1-3):25-74.
Linear realizability and full completeness for typed lambda-calculi.Samson Abramsky & Marina Lenisa - 2005 - Annals of Pure and Applied Logic 134 (2-3):122-168.

Analytics

Added to PP
2009-01-28

Downloads
41 (#112,661)

6 months
16 (#899,032)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

Introduction to Higher Order Categorical Logic.J. Lambek & P. J. Scott - 1989 - Journal of Symbolic Logic 54 (3):1113-1114.
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.

Add more references