3
$\begingroup$

I'm trying to get a deeper understanding of Buss's version of Gödel's speedup proof. In short, if we assume that $Z_0$ is first-order arithmetic, $Z_1$ is second-order arithmetic, and so on, then for $i>0$, $Z_{i+1}$ exhibits speedup over $Z_i$. But on page 11, he says this without citing it:

Using a truth-definition for (i+1)-st order formulas, $Z_{i+1}$ can prove the consistency of $Z_i$, i.e., $Z_{i+1}$ can prove $(\forall_x)Con_{z_i}(x).$

Here, $Con_{z_i}(x)$ means: $Z_i$ is consistent up to all proofs in $Z_i$ which have symbol lengths $\leq x$ (using some fixed encoding of proof length). Clearly, this is decidable: just list all $Z_i$-proofs up to size $x$ and make sure they don't prove any inconsistencies.

But here's where I'm lost. From Gödel's second incompleteness theorem, second-order arithmetic cannot prove its own consistency:

$\neg (Z_1 \vdash (\forall_x)Con_{z_1}(x))$

But according to Buss's statement, third-order arithmetic can prove:

$Z_2 \vdash (\forall_x)Con_{z_1}(x)$

And since second-order logic can express anything that higher-order logics can, this means:

$Z_1 \vdash (\forall_x)Con_{z_1}(x)$

I'm sure that I'm missing some nuance here. So here are my questions:

  1. Is there a definitive citation for the claim that for all $i\geq 0$, $Z_{i+1} \vdash (\forall_x)Con_{z_i}(x)$? I know you can do this for $Z_0$ by expressing the Tarskian conditions for a truth predicate in $Z_1$, but it's not clear to me you can do that with higher-order logics as well.

  2. Is there a definitive citation for the claim that $Z_1$ can express anything that $Z_2$, $Z_3$, ... can?

  3. What am I missing in my apparent contradiction above?

EDIT: I'm now convinced that my understanding of the expressive power of second-order logic was indeed where the flaw was, as SOL can in fact express whatever third- and higher-order logics can (in the sense of mutual validity), but that SOL can not necessarily capture whatever third- and higher-order logics can. But part of my original question is still unanswered: does anyone have a citation or proof of Buss's claim I quoted above (that second-order arithmetic can prove the consistency of first-order arithmetic, third-order arithmetic can prove the consistency of second-order arithmetic, etc.)?

Improve this question
$\endgroup$
3
  • 8
    $\begingroup$ Your apparent contradiction arises from conflating the slogan "second-order logic can express anything that higher-order logics can" with The idea that $\text{Con}_{Z_1}$ is equivalent to $\text{Con}_{Z_2}$. Unfortunately, I don't have time right now to write more, but I think that, if you check the theorem underlying that slogan (in particular the relevant meaning of "express"), the difficulty may disappear. $\endgroup$
    – Andreas Blass
    Commented Aug 5, 2019 at 18:12
  • $\begingroup$ Sorry, but I'm confused by your comment---I didn't write $Con_{Z_2}$ anywhere, nor did I claim it was equivalent to $Con_{Z_1}$. $\endgroup$
    – John Licato
    Commented Aug 6, 2019 at 12:59
  • $\begingroup$ Sorry, I should have written "the idea that $Z_1\vdash$ is equivalent to$Z_2\vdash$. $\endgroup$
    – Andreas Blass
    Commented Aug 6, 2019 at 13:31

0

Reset to default

You must log in to answer this question.