$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$This is a follow up to Kleene realizability in Peano arithmetic.

We can summarize the results from this answer as follows:

$$T_1 = \{ \phi : \exists n. \T{PA} \vdash \overline n \kr \phi \} = \T{HA+ECT_0+MP}$$ $$T_3 = \{ \phi : \T{PA} \vdash \exists n. n \kr \phi \} = \T{HA+ECT_0+MP+SLEM}$$

Where $\T{SLEM}$ is excluded middle for sentences.

My question is about finding a third theory, one for which PA can find a bound on the realizer (but not necessarily the exact value).

$$T_2 = \{ \phi : \exists k. \T{PA} \vdash \exists n < \overline k. n \kr \phi \} = \T{?}$$

Clearly we have $T_1 \subseteq T_2 \subseteq T_3$. We can also show that they are distinct.

$T_2$ proves excluded middle for all negated sentences, but $T_1$ does not. In particular, $T_2 \vdash \lnot Con(\T{PA}) \lor \lnot \lnot Con(\T{PA})$.

For any numeral $n$, $T_3$ can prove that the $n$th busy beaver number $BB(n)$ exists because $\T{PA}$ proves it exists and knows how to turn it into a realizer (a different realizer for each $n$). $T_2$ is unable to prove this when $n$ is sufficiently large (say, 8000 or more) because for any numeral $k$, PA can't prove that $BB(n) < k$.

So, what is $T_2$?

$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$This is a follow up to Kleene realizability in Peano arithmetic.

We can summarize the results from Emil Jeřábek's answer as follows:

\begin{gather*} T_1 = \{ \phi : \exists n. \T{PA} \vdash \overline n \kr \phi \} = \T{HA}+\T{ECT}_0+\T{MP} \\ T_3 = \{ \phi : \T{PA} \vdash \exists n. n \kr \phi \} = \T{HA}+\T{ECT}_0+\T{MP}+\T{SLEM} \end{gather*}

where $\T{SLEM}$ is excluded middle for sentences.

My question is about finding a third theory, one for which PA can find a bound on the realizer (but not necessarily the exact value).

$$T_2 = \{ \phi : \exists k. \T{PA} \vdash \exists n < \overline k. n \kr \phi \} = \T{?}$$

Clearly we have $T_1 \subseteq T_2 \subseteq T_3$. We can also show that they are distinct.

$T_2$ proves excluded middle for all negated sentences, but $T_1$ does not. In particular, $T_2 \vdash \lnot \operatorname{Con}(\T{PA}) \lor \lnot \lnot \operatorname{Con}(\T{PA})$.

For any numeral $n$, $T_3$ can prove that the $n$th busy beaver number $\operatorname{BB}(n)$ exists because $\T{PA}$ proves it exists and knows how to turn it into a realizer (a different realizer for each $n$). $T_2$ is unable to prove this when $n$ is sufficiently large (say, 8000 or more) because for any numeral $k$, PA can't prove that $\operatorname{BB}(n) < k$.

So, what is $T_2$?

$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$

This is a follow up to Kleene realizability in Peano arithmetic.

We can summarize the results from this answer as follows:

$$T_1 = \{ \phi : \exists n. \T{PA} \vdash \overline n \kr \phi \} = \T{HA+ECT_0+MP}$$ $$T_3 = \{ \phi : \T{PA} \vdash \exists n. n \kr \phi \} = \T{HA+ECT_0+MP+SLEM}$$

Where $\T{SLEM}$ is excluded middle for sentences.

My question is about finding a third theory, one for which PA can find a bound on the realizer (but not necessarily the exact value).

$$T_2 = \{ \phi : \exists k. \T{PA} \vdash \exists n < \overline k. n \kr \phi \} = \T{?}$$

Clearly we have $T_1 \subseteq T_2 \subseteq T_3$. We can also show that they are distinct.

$T_2$ proves excluded middle for all negated sentences, but $T_1$ does not. In particular, $T_2 \vdash \lnot Con(\T{PA}) \lor \lnot \lnot Con(\T{PA})$.

For any numeral $n$, $T_3$ can prove that the $n$th busy beaver number $BB(n)$ exists because $\T{PA}$ proves it exists and knows how to turn it into a realizer (a different realizer for each $n$). $T_2$ is unable to prove this when $n$ is sufficiently large (say, 8000 or more) because for any numeral $k$, PA can't prove that $BB(n) < k$.

So, what is $T_2$?

$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$This is a follow up to Kleene realizability in Peano arithmetic.

We can summarize the results from this answer as follows:

$$T_1 = \{ \phi : \exists n. \T{PA} \vdash \overline n \kr \phi \} = \T{HA+ECT_0+MP}$$ $$T_3 = \{ \phi : \T{PA} \vdash \exists n. n \kr \phi \} = \T{HA+ECT_0+MP+SLEM}$$

Where $\T{SLEM}$ is excluded middle for sentences.

My question is about finding a third theory, one for which PA can find a bound on the realizer (but not necessarily the exact value).

$$T_2 = \{ \phi : \exists k. \T{PA} \vdash \exists n < \overline k. n \kr \phi \} = \T{?}$$

Clearly we have $T_1 \subseteq T_2 \subseteq T_3$. We can also show that they are distinct.

$T_2$ proves excluded middle for all negated sentences, but $T_1$ does not. In particular, $T_2 \vdash \lnot Con(\T{PA}) \lor \lnot \lnot Con(\T{PA})$.

For any numeral $n$, $T_3$ can prove that the $n$th busy beaver number $BB(n)$ exists because $\T{PA}$ proves it exists and knows how to turn it into a realizer (a different realizer for each $n$). $T_2$ is unable to prove this when $n$ is sufficiently large (say, 8000 or more) because for any numeral $k$, PA can't prove that $BB(n) < k$.

So, what is $T_2$?