Extensional realizability Original Research Article

Two straightforward “extensionalisations” of Kleeneʹs realizability are considered; denoted re and e. It is shown that these realizabilities are not equivalent. While the re-notion is (as a relation between numbers and sentences) a subset of Kleeneʹs realizability, the e-notion is not. The problem of an axiomatization of e-realizability is attacked and one arrives at an axiomatization over a conservative extension of arithmetic, in a language with variables for finite sets. A derived rule for arithmetic is obtained by the use of a q-variant of e-realizability; this rule subsumes the well-known Extended Churchʹs Rule. The second part of the paper focuses on toposes for these realizabilities. By a relaxation of the notion of partial combinatory algebra, a new class of realizability toposes emerges. Relationships between the various realizability toposes are given, and results analogous to Robinson and Rosoliniʹs characterization of the effective topos, are obtained for a topos generalizing e-realizability.