Uniform Realizability Interpretations

1. Problem Statement

Realizability interpretations are a cornerstone of constructive logic, providing a method to extract computational content (witnesses) from proofs. Since Kleene's original number realizability (1945), numerous variants have been developed, including Kreisel's modified realizability, Herbrand realizability, classical realizability, and learning realizability.

However, these variants suffer from a lack of unification regarding how they treat quantifiers:

• Traditional approaches (e.g., Kleene) require realizers for existential quantifiers ($\exists x A(x)$) to explicitly provide a witness $x$ and a realizer for $A(x)$. Universal quantifiers ($\forall x A(x)$) require a function that produces a realizer for every $x$.
• Modern approaches (e.g., Herbrand realizability, Uniform Heyting Arithmetic) treat quantifiers uniformly. In these systems, a realizer for $\exists x A(x)$ does not necessarily explicitly contain the witness $x$; rather, it uniformly realizes $A(x)$ for some $x$. Similarly, a realizer for $\forall x A(x)$ must work uniformly for all $x$ without necessarily depending on $x$ in a specific way.

The paper identifies a gap: there is no single framework that abstracts these differences, parametrizing the interpretation by the treatment of atomic formulas while treating quantifiers uniformly across all variants.

2. Methodology

The authors propose a Uniform Realizability Interpretation framework. The core methodology involves:

1. Distinction between Quantifier Types:

   • Unqualified (Uniform) Quantifiers: $\exists x A(x)$ and $\forall x A(x)$. These are always interpreted uniformly.
   • Qualified (Typed) Quantifiers: $\exists^B x A(x)$ and $\forall^B x A(x)$. These are treated as syntactic abbreviations for $\exists x (B(x) \land A(x))$ and $\forall x (B(x) \to A(x))$. This reduces the problem to interpreting the predicate $B(x)$ and the unqualified quantifiers.

2. Parametrized Base Interpretation:
   The framework separates the interpretation of atomic predicates from the logical connectives.

   • A Base Interpretation maps an $n$-ary predicate $P$ of the source theory $S$ to an $(n+m)$-ary relation $x \triangleright_P a$ in a target theory $T$. Here, $x$ represents the arguments of the predicate, and $a$ represents the tuple of realizers (witnesses).
   • The relation $x \triangleright_P a$ is read as "$x$ is $P$-bounded by $a$."

3. Inductive Definition of Uniform Realizability:
   Using the base interpretation, the authors define the uniform realizability relation $a \text{ ur } A$ for all formulas $A$:

   • Atomic: $a \text{ ur } P(x) \iff x \triangleright_P a$.
   • Conjunction: $a, b \text{ ur } A \land B \iff (a \text{ ur } A) \land (b \text{ ur } B)$.
   • Implication: $f \text{ ur } A \to B \iff \forall a ((a \text{ ur } A) \to (f(a)\downarrow \land f(a) \text{ ur } B))$.
   • Existential: $a \text{ ur } \exists x A(x) \iff \exists x (a \text{ ur } A(x))$. (Note: The realizer $a$ does not explicitly contain $x$; it uniformly realizes the formula for some $x$).
   • Universal: $a \text{ ur } \forall x A(x) \iff \forall x (a \text{ ur } A(x))$. (Note: The same realizer $a$ must work for all $x$).

4. Target Theory Requirements:
   The target theory $T$ must support intuitionistic logic, function application, and $\lambda$-abstraction. It may be typed or untyped.

3. Key Contributions

A. Unification of Realizability Variants

The primary contribution is showing that five distinct realizability interpretations are instances of this single uniform framework, differing only in their base interpretation of atomic predicates ($\bot$, $=$, and $N(n)$):

1. Kleene Realizability:

   • Base: $N(n)$ is interpreted precisely ($n \triangleright_N m \iff n=m$). $\bot$ is empty.
   • Result: Recovers standard Kleene number realizability where realizers are natural numbers providing explicit witnesses.

2. Kreisel Modified Realizability:

   • Base: Same as Kleene, but realizers are total functionals (System T).
   • Result: Recovers Kreisel's modified realizability, which validates the Independence of Premise schema.

3. Herbrand Realizability (Non-standard Arithmetic):

   • Base: $N(n)$ is interpreted uniformly ($n \triangleright_N \langle\rangle \iff \text{true}$). External quantifiers (standard numbers) are interpreted via finite sets ($n \triangleright_{st} S \iff n \in S$).
   • Result: Recovers Herbrand realizability where existential quantifiers do not require explicit witnesses in the realizer, but rather a uniform proof.

4. Classical Realizability (Friedman-Dragalin):

   • Base: $\bot$ is interpreted via a predicate $P(a)$ (e.g., $P(a)$ represents a contradiction). Equality is interpreted as $(n=m) \lor P(a)$.
   • Result: Allows extracting computational content from negated formulas in classical logic by treating falsity as a computational state.

5. Aschieri-Berardi Learning Realizability:

   • Base: Introduces a "state" type $S$. Equality and falsity depend on whether a state transformer $\gamma$ reaches a fixed point ($\gamma(s)=s$).
   • Result: Models proofs as state-updating transformers, allowing the interpretation of the Law of Excluded Middle for $\Sigma^0_1$ formulas.

B. General Soundness Theorem

The authors prove a General Soundness Theorem (Theorem 2.7).

• Statement: If all non-logical axioms of a source theory $S$ are realizable under a specific base interpretation, then all theorems of $S$ are realizable.
• Significance: This decouples the proof of soundness from the specific logical connectives. One only needs to verify that the specific axioms of the theory (e.g., Peano axioms, induction) are realizable under the chosen atomic interpretation. The uniform treatment of quantifiers ensures that logical rules (like $\exists$-introduction) hold automatically.

C. Handling Induction

The paper provides a detailed analysis of how induction is realized under different interpretations of $N(n)$:

• Precise ($n=m$): Realized by primitive recursion.
• Approximate ($n \leq m$ or $n \in S$): Realized by iterating a "join" operation (upper bound) to ensure the realizer works uniformly for all $n$ up to a bound.

4. Results

• Formal Equivalence: The paper establishes formal equivalences between the proposed uniform definitions and the standard definitions of the five realizability variants mentioned above.
• Soundness Verification: The soundness of all five variants is derived as a corollary of the general Soundness Theorem, provided their respective non-logical axioms are realizable.
• Handling of Falsity: The framework successfully integrates interpretations where falsity ($\bot$) carries computational content (Classical and Learning realizability) alongside those where it does not (Kleene and Modified).

5. Significance

• Conceptual Unification: The paper resolves the fragmentation in the realizability literature by demonstrating that the differences between "witness-based" and "uniform" interpretations are not fundamental logical differences but rather variations in how atomic predicates are modeled.
• Modularity: By parametrizing the interpretation via the base relation, researchers can easily design new realizability interpretations by simply defining a new base relation for atomic formulas, without re-proving the soundness of the logical rules.
• Extension to Classical Logic: The framework naturally accommodates classical logic principles (via Friedman-Dragalin translation or state-based learning) within a uniform realizability setting, bridging the gap between constructive and classical realizability.
• Future Directions: The authors note that while the framework unifies first-order theories, it raises questions about conservativity when extending the language to include both qualified and unqualified quantifiers, and how it might extend to higher-order types or intersection types.

In summary, Berger and Oliva provide a powerful meta-theoretical tool that abstracts the mechanics of realizability, allowing for a systematic comparison and generation of realizability interpretations across diverse logical landscapes.