After a long story of dancing around the effective topos $ \mathcal{Eff}$, I finally resolved to get to the bottom of it. To this effect, working as it were backward, I ended up revisiting Kleene's original definition of realizability for Heyting Arithmetic (1949), the "Mother of all realizabilities" .
To my surprise, I found something which makes me a bit uneasy. The definition for connectives and quantifiers are what one would expect, keeping in mind the so-called $\mathbf{BHK} $interpretation.
However, here is the definition of ground zero realizability, ie how a number realizes a basic sentence:
A number $n$ realizes an atomic formula $s=t$ if and only if $s=t$ is true.
Thus every number realizes a true equation, and no number realizes a false equation.
You might ask: what is wrong with that? The answer is, obviously nothing. A definition is a definition.
However, keeping in mind the overarching goal, which is to create a constructive semantics, it makes me balk a little. Say that you have two (closed ) terms in the language of $\mathbf{HA}$, and you intend to show that they denote the same number. What do you do? You calculate. In other words, you reduce the first to the second, by either appealing to direct calculation, or some short cuts. Thus, this calculation, suitably encoded, is a realizer for the equality. Appealing to "truth " in $N$ goes against the spirit of realizability. Even if you are not a skeptic of crystal clear $N$, in this era of $\mathbf{HoTT}$, infinity groupoids, and generally replacing deprecated equality for equivalences, one would hope for an amendment of the above.
If you like, an "homotopical realizability", where the above gets morphed into something like
$e$ realizes $t=s$ iff $e$ is the code of a reduction path from t to $s$.
Questions:
- Does there exist already some kind of modified realizability in the lines mentioned above?
- Assuming the first answer is yes, how does this reflects within the toposophical standpoint?
Comment: it is clear that if we work with homotopical realizability, the truth value of $t=s$ is not the entire set of natural numbers, but rather the set of coded paths between the two terms (their path space). Thus, even not jumping directly into realizability topoi, and assuming some more simple minded approach like the category of assemblies, adjustments have to be made. Very curious to know which ones.
ADDENDUM
Reflecting a bit further, and also after the little exchange with Andreas, I have realized a few things:
- if one swaps KLeene's with my proposed realizability, the topos remains exactly the same. Why? because the realizability topos depends exclusively on the partial combinatory algebra, which in this case is still what it was before. The two notions of realizability change only the way sentences are evaluated, the truth values, nothing else.
- Thus, the only major change is this: in the Effective topos we have of course the internal language, and when it is applied to the Natural Number Object, it maps precisely Kleene's. It is a theorem, which for instance is proved in Vermeeren, 2009.
- What next? Well, the obvious question is, is there another object in the topos such that its internal logic corresponds to the realizability I have sketched? Open question, though I do have a hunch…
Best Answer
The reference to "truth in $\mathbb{N}$" is a mirage. As Andreas Blass points out, there is a computable procedure that determines whether $s = t$ holds for closed term $s$ and $t$ of HA. One needs only run a certain algorithm to find out whether $s = t$, there is no "faith in the model".
And because equality is decidable, nothing is gained by providing a realizer of $s = t$. (We can just throw it away and reconstruct it at will whenever needed.)
In my opinion you have gone too far back in history. Kleene's work was about first-order arithmetic, and since equality of natural numbers is decidable in HA, nothing interesting can be discovered by considering its realizers.
The right historical moment to pay attention to is the invention of the effective topos, because that is the first realizability model with effective quotients. There equality does in general have computational content and so is informative. (For example, a realizer of equality of truth values $p, q \in \Omega$ is a pair $\langle a, b \rangle$ such that $a$ realizers $p \Rightarrow q$ and $b$ realizers $q \Rightarrow p$.)
We can conjure up an object of the effective topos in which a realizer of $s = t$ does in fact encode a "path" or a "reduction sequence", but for such an example to be non-trivial, the reduction sequence must not be computable from $s$ and $t$ alone (otherwise it will end up being $\lnot\lnot$-stable).
P.S. There is homotopical realizability, but it may not be what you asked for. See Uemura's cubical assemblies.
Addendum
We may indeed define an object in the effective topos such that equality is realized by (encodings of) reduction sequences. Note that any such object, in order not to be isomorphic to one whose equality has trivial realizers, must not be an assembly. This rules out any notion of reduction for which the predicate "$p$ is (the code of) a reduction step from $s$ to $t$" is decidable. Indeed, if such a predicate is decidable, then we may reconstruct a reduction sequence from $s$ to $t$ whenever it exists, by simply enumerating all possibilities and looking for one that works. Consequently, the resulting equality relation will be $\lnot\lnot$-stable, and the object isomorphic to one with trivial realizers of equality.