Uniform Realizability Interpretations

TL;DR

This paper introduces a unified framework called uniform realizability that generalizes various logical realizability interpretations, accommodating different treatments of atomic formulas and quantifiers in classical and modern contexts.

Contribution

It proposes a novel, abstract notion of uniform realizability that unifies and extends existing realizability interpretations across different logical frameworks.

Findings

Unified treatment of classical and modern realizability interpretations

Application to various interpretations of Heyting arithmetic

Framework accommodates different atomic formula treatments

Abstract

This work introduces a novel framework of uniform realizability that unifies and generalizes various realizability interpretations of logic, particularly focussing on the treatment of atomic formulas and quantifiers. Traditional realizability interpretations (such as Kleene's number realizability) require explicit witnesses for existential quantifiers. In contrast, newer approaches, such as in the first author's uniform Heyting arithmetic, Herbrand realizability of non-standard arithmetic, or in the "classical" realizability of arithmetic, (some) quantifiers, are treated uniformly. The proposed notion of uniform realizability abstracts these differences, parametrising the interpretation by a given treatment of atomic formulas, accounting for both classical and modern variants. The approach is illustrated using several realizability interpretations of Heyting arithmetic.