Krivine's classical realisability from a categorical perspective

Autor:	Thomas Streicher
Rok vydání:	2013
Předmět:	Sequence Mathematics (miscellaneous) Forcing (recursion theory) Current (mathematics) Perspective (geometry) Interpretation (logic) Calculus Set theory Categorical variable Axiom Computer Science Applications Mathematics
Zdroj:	Mathematical Structures in Computer Science. 23:1234-1256
ISSN:	1469-8072 0960-1295
DOI:	10.1017/s0960129512000989
Popis:	In a sequence of papers (Krivine 2001; Krivine 2003; Krivine 2009), J.-L. Krivine introduced his notion of classical realisability for classical second-order logic and Zermelo–Fraenkel set theory. Moreover, in more recent work (Krivine 2008), he has considered forcing constructions on top of it with the ultimate aim of providing a realisability interpretation for the axiom of choice.The aim of the current paper is to show how Krivine's classical realisability can be understood as an instance of the categorical approach to realisability as started by Martin Hyland in Hyland (1982) and described in detail in van Oosten (2008). Moreover, we will give an intuitive explanation of the iteration of realisability as described in Krivine (2008).
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::c64a14b8e81a0f41a390d888a178c92f https://doi.org/10.1017/s0960129512000989 Zobrazit plný text záznamu