self-contained vs. non-self-contained notions of realizability

140 Views Asked by At

There seem to be two notions of realizability in literature, where in one case the realization of a formula is fully self-contained with respect to providing a proof object for the given formula, while in the other case it is incomplete and requires some characteristics to be present in the realizability structure where it is taken from.

For example, in McCarty (Realizability and Recursive Mathematics, 1985, Section 2.7), the pairing axiom $\forall a b. \exists c. a \in c \wedge b \in c$ is realized by $p (p 0 i) (p 0 i)$, which is also exactly the realization of any formula $a \in c \wedge b \in c$ without quantification. The quantification is made possible by requiring that the underlying realizability structure globally contains a $c = \{ \langle 0,a\rangle,\langle 0,b\rangle \}$ for every $a$ and $b$. So, the realization is not self-contained because it would only realize the formulas if the realizability structure contains the corresponding set $c$. Rathjen (Realizability for Constructive Zermelo-Fraenkel Set Theory, 2004) uses the term "realization" in a similar fashion.

On the other hand, Schwichtenberg (Realizability Interpretation of Proofs in Constructive Analysis, 2006, Section 1.5) or Troelstra (Realizability, 1998, Section 1) realize existential and universal quantifications by encoding the quantifying relation in the realization itself. This way, the realization contains all the information necessary to check the realization.

I think the difference is important for some applications of realizability, for example extracting algorithms from realizations.

So, are the two notions (self-contained vs. non-self-contained) of realizability equivalent in the sense that there could somehow be converted between both of them?

Addendum 1:

Obviously, a non-self-contained realization $A$ within a realizability structure $B$ could be made self-contained by encoding a tuple $\langle A, B\rangle$. But usually $B$ will not be finite. So, I would like to refine my question in a manner where only finite realizations for individual formulas are expected. This is also the case for the self-contained examples of realizability notions I gave.

Addendum 2:

I did some further research which might prove helpful if someone has an idea for solving this question. The non-self-contained notion seems to go back to a work by Kreisel and Troelstra (Formal systems for some branches of intuitionistic analysis, 1969). More interestingly, while the aforementioned work by Rathjen uses non-self-contained realizers for unbounded quantifiers, it encodes the quantifying relation in the realizer for bounded quantifiers. While a reason for making this qualitative distinction was not given, I do now wonder whether it may be even impossible to do a similar thing for unbounded quantifiers because of limitations in the expressiveness of the underlying axiomatic set theory. Might it be possible that there would be no sound definition for the set of realizers then, considering that constructing it might require working with the universal set which does not exist?