Realizability and Kripke Forcing

Abstract

Realizability, developed by Stephen Kleene, is a type-free device for extracting computations from logical specifications. Realizability analyzes the computational content of reasoning: it models the universe of recursive mathematics. Kripke and associated Categorical interpretations give a broader, topological/algebraic semantics for constructive reasoning which is complete for intuitionistic logic. They are, therefore, a powerful and indispensable tool for modelling computationally meaningful formal systems. How are the two semantical paradigms related ? In this paper, we construct several Kripke and Categorical Models which are elementarily equivalent to Syntactic Realizability. By merging the two approaches we provide a new class of models and a framework for reasoning about computational evidence and the process of term extraction itself.