Classical and Relative Realizability

TL;DR

This paper demonstrates how all abstract Krivine structures can be derived from filtered opcas within the framework of relative realizability toposes, revealing new Boolean subtoposes of the Kleene-Vesley topos.

Contribution

It establishes a method to obtain any abstract Krivine structure from filtered opcas and characterizes the resulting toposes as Booleanizations of subtoposes.

Findings

Every abstract Krivine structure corresponds to a filtered opca.

The topos is a Booleanization of a subtopos of RT(A',A).

Identifies non-localic Boolean subtoposes of the Kleene-Vesley topos.

Abstract

We show that every abstract Krivine structure in the sense of Streicher can be obtained, up to equivalence of the resulting tripos, from a filtered opca (A,A') and a subobject of 1 in the relative realizability topos RT(A',A); the topos is always a Booleanization of a closed subtopos of RT(A',A). We exhibit a range of non-localic Boolean subtoposes of the Kleene-Vesley topos.