4
$\begingroup$

$\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$?

Improve this question
$\endgroup$
5
  • $\begingroup$ @EmilJeřábek $\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$in that answer one of the steps was "Since $\exists x\,(x\kr\phi)$ is a sentence, this implies $\T{HA+MP+SLEM}\vdash\exists x\,(x\kr\phi).$". How does that work using excluded middle just for negated sentences? $\endgroup$
    – Christopher King
    Commented Jan 30 at 20:44
  • $\begingroup$ (fyi, the lower bound of 8000 was lowered by bachelor student Johannes Riebel to 745 (from an earlier bound of 748).) $\endgroup$
    – Ingo Blechschmidt
    Commented Jan 31 at 10:17
  • $\begingroup$ The 745 bound is for ZFC; it should be considerably less for PA. In particular, if you take the adjunctive set theory plus the induction schema as in mathoverflow.net/a/461632 (you don't need the empty set axiom if you formulate induction in the right way, and I think you can make do without extensionality while keeping the same consistency strength), the axioms should have a shorter description than ZF. $\endgroup$
    – Emil Jeřábek
    Commented Jan 31 at 11:17
  • $\begingroup$ There may also be ways of optimizing the proof system. I’m a bit puzzled by the unusual quantifier axioms, but the propositional part can be definitely shortened by using Meredith’s single axiom ((((p→q)→(¬r→¬s))→r)→t) → ((t→p)→(s→p)). Or, use $\bot$ as primitive instead of $\neg$, and take Łukasiewicz’s axiom $((p\to q)\to r)\to((r\to p)\to(s\to p))$ and $\bot\to p$. $\endgroup$
    – Emil Jeřábek
    Commented Jan 31 at 14:27
  • $\begingroup$ (I’m sorry for the off-topic comments. I swear I will stop.) Here’s a fun way of axiomatizing ZFfin (without regularity, but including extensionality), which should lead to a particularly short description: $\forall x,y\,\exists z\,\forall t\,(t\in z\leftrightarrow(t\in x\oplus t=y))$ + the schema $\forall x\,(\forall y\subsetneq x\,\phi(y)\to\phi(x))\to\phi(x)$. $\endgroup$
    – Emil Jeřábek
    Commented Jan 31 at 14:42

1 Answer 1

Reset to default
7
$\begingroup$

$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}\let\LOR\bigvee$The same argument as in my linked answer shows that $$T_2=\T{HA+ECT_0+MP+SWLEM},$$ where $$\T{SWLEM}=\{\neg\phi\lor\neg\neg\phi:\text{$\phi$ sentence}\}.$$ You already observed that $T_2$ includes $T_1+\T{SWLEM}$.

On the other hand, assume $\T{PA}\vdash\exists x\le\overline n\,x\kr\phi$, and let $\psi(x)$ be a negative formula equivalent to $x\kr\phi$ in $\T{HA+MP}$. Then $\T{PA}\vdash\LOR_{m\le n}\psi(\overline m)$, thus $\T{HA}$ proves its double negation translation, which is equivalent to $\neg\neg\LOR_{m\le n}\psi(\overline m)$ as $\psi$ is negative. Consequently, $\T{HA+SWLEM}\vdash\LOR_{m\le n}\neg\neg\psi(\overline m)$, i.e., $\LOR_{m\le n}\psi(\overline m)$, using negativity again, thus $\T{HA+SWLEM+MA}\vdash\LOR_{m\le n}\overline m\kr\phi$, and $\T{HA+SWLEM+MA+ECT_0}\vdash\phi$.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .