It is a well-known fact that given a first-order sentence $\psi$ in prenex normal form $\forall x\_1 \exists y\_1 \forall x\_2 \exists y\_2 \dots \forall x\_n \exists y\_n \theta(x\_1,\dots,x\_n,y\_1,\dots,y\_n)$ (i.e., $\theta$ is quantifier free or at least $\Delta^0\_0$ in the appropriate sense), the truth of $\psi$ in a given structure $M$ can be understood in terms of a game in which two players ($\forall$ and $\exists$) alternatively choose elements of $M$ corresponding to the bound variables of $\psi$, with $\forall$ choosing for the variables $x\_i$ and $\exists$ choosing for the variables $y\_i$. $\exists$ wins if and only if at the end the resulting variable assignment makes $\theta$ true in $M$. The characterization is of course that $M \models \psi$ if and only if $\exists$ has a winning strategy for this game.


Such a strategy can be understood as a series of Skolem functions $f\_1(x\_1),f\_2(x\_1,x\_2),\dots,f\_n(x\_1,x\_2,\dots,x\_n)$ on $M$ with the property that (after expanding $M$ with the $f\_i$'s), $M \models \forall x\_1\dots x\_n \theta(x\_1,\dots,x\_n,f\_1(x\_1),\dots,f\_n(x\_1,\dots,x\_n))$. In the specific case of arithmetic (i.e., the structure $(\mathbb{N},0,+,\cdot)$), these functions are closely related to the idea of realizability. If $\psi$ is provable in Heyting arithmetic, for instance, then one can extract computable functions $f\_1,f\_2,\dots,f\_n$ giving a winning strategy for $\exists$.


Kreisel showed that an analogous weaker statement is true of Peano arithmetic. A proof of $\psi$ in Peano arithmetic gives $\exists$ a computable procedure for beating any particular strategy for $\forall$, provided that $\exists$ is given $\forall$'s strategy in advance. More formally, given a proof of $\psi$ in Peano arithmetic, we can computably extract Turing indices $e\_1,\dots,e\_n$ such that for any functions $g\_1 : \mathbb{N}^0 \to \mathbb{N}$, $g\_2 : \mathbb{N}^1 \to \mathbb{N}$, $\dots$, $g\_n : \mathbb{N}^{n-1} \to \mathbb{N}$, we have that
$ \mathbb{N} \models \theta(a\_0,\dots,a\_n,b\_0,\dots,b\_n), $
where $$a\_i = g\_i(b\_1,\dots,b\_{i-1})$$ and $$b\_i = \Phi\_{e\_i}^{g\_1\dots g\_n}(a\_1,\dots,a\_{i})$$ for each $i \in [1,n]$. ($\Phi\_e^X(n)$ is of course the $e$th Turing functional applied to $n$ given $X$ as an oracle. Assume that we're using some fixed computable tupling function.) This fact is often called Kreisel's 'no-counterexample interpretation' of Peano arithmetic.


Let's say that $\bar{e} = (e\_1,\dots,e\_n)$ is a *weak classical realizer* of $\psi$ if the above condition holds. (I don't know if this concept has an established name.) For the sake of this question, we'll write $\bar{e} \Vdash \psi$ to mean that $\bar{e}$ is a weak classical realizer of $\psi$. (Note that $(\exists \bar{e})\bar{e}\Vdash \psi$ is a lightface $\Pi^1\_1$ condition on $\psi$.) I believe that the commonly studied notions of classical realizers for arithmetic (e.g., realizability in the sense of Krivine) are a priori stronger than this in that while they allow a certain amount of probing of $\forall$'s stragey, they do not necessarily allow arbitrary computation from it.


We can now cosmetically restate Kreisel's result as saying that if $\mathsf{PA} \vdash \psi$, then $(\exists \bar{e})\bar{e} \Vdash \psi$. It's also not too hard to show that if $(\exists \bar{e})\bar{e} \Vdash \psi$, then $\mathbb{N} \models \psi$. (No amount of prep work can beat an unbeatable strategy.)


I'm curious about the extent to which the conditions $\mathsf{PA} \vdash \psi$, $(\exists \bar{e})\bar{e} \Vdash \psi$, and $\mathbb{N} \models \psi$ differ. One immediate observation is that if $\psi$ is a true $\Pi^0\_1$-sentence, then $(\exists \bar{e})\bar{e} \Vdash \psi$ (somewhat trivially), which means that there are many examples of $\mathsf{PA}$-unprovable sentences with weak classical realizers (a Gödel sentence for instance). This leads to a somewhat more nuanced question.



> 
> **Question 1.** Is there a sentence $\psi$ such that $(\exists \bar{e})\bar{e} \Vdash \psi$, yet $\mathsf{PA} \cup \{\chi: \mathbb{N}\models\chi,~\chi\text{ a }\Pi^0\_1\text{ sentence}\} \not \vdash \psi$?
> 
> 
> 


In the other direction, there is basically no way that $\mathbb{N} \models \psi$ implies $(\exists \bar{e})\bar{e} \Vdash \psi$, but finding an explicit example of this seems difficult. The theory of $\mathbb{N}$ is lightface $\Delta^1\_1$, which is simpler than the apparent complexity of the set of sentences with weak classical realizers (lightface $\Pi^1\_1$).



> 
> **Question 2.** Is there a sentence $\psi$ such that $\mathbb{N} \models \psi$, yet $\neg (\exists \bar{e}) \bar{e} \Vdash \psi$?
> 
> 
> 



Which arithmetical sentences have no counterexamples in the sense of Kreisel?
In fact all true arithmetical sentences have weak classical realizers. Namely, a true arithmetical sentence $\psi$ $$\forall x\_1\exists y\_1 \ldots \forall x\_n\exists y\_n \theta(x\_1,\ldots,x\_n,y\_1,\ldots,y\_n)$$
is weakly realized by $(e\_1,\ldots,e\_n)$, where $\Phi\_{e\_i}^{\vec{g}}(y\_1,\ldots,y\_{i-1})$ performs an unbounded search for a tuple $(y\_i,\ldots,y\_n)$ such that $\theta(g\_0(),\ldots,g\_n(y\_1,\ldots,y\_n),y\_1,\ldots,y\_n)$ is true and then outputs $y\_i$ from the first found tuple. This works since for any $g\_1\colon\mathbb{N}^0\to\mathbb{N},\ldots,g\_n\colon \mathbb{N}^{n-1}\to\mathbb{N}$ the sentence $\exists y\_1,\ldots, y\_n \theta(g\_0(),\ldots,g\_n(y\_1,\ldots,y\_n),y\_1,\ldots,y\_n)$ is true.


