Realizability in ordered combinatory algebras with adjunction

摘要

In this work, we continue our consideration of the constructions presented in the paper Krivine's Classical Realizability from a Categorical Perspective by Thomas Streicher. Therein, the author points towards the interpretation of the classical realizability of Krivine as an instance of the categorical approach started by Hyland. The present paper continues with the study of the basic algebraic set-up underlying the categorical aspects of the theory. Motivated by the search of a full adjunction, we introduce a new closure operator on the subsets of the stacks of an abstract Krivine structure that yields an adjunction between the corresponding application and implication operations. We show that all the constructions from ordered combinatory algebras to triposes presented in our previous work can be implemented, mutatis mutandis, in the new situation and that all the associated triposes are equivalent. We finish by proving that the whole theory can be developed using the ordered combinatory algebras with full adjunction or strong abstract Krivine structures as the basic set-up.