6
$\begingroup$

Let $\phi$ be a "reasonable" formula in the language of first-order arithmetic expressing some amount of transfinite induction along a given (index for a) computable linear order; my default choice here is $\Sigma_1$-transfinite recursion, but I'm happy to tweak it if a different definition would result in an easier question.

Let $\mathsf{PA}$ be the usual first-order Peano arithmetic, and let $\mathsf{PA}_\omega$ be its cut-free infinitary analogue.

EDIT: As Anupam Das points out below, the full $\omega$-rule is far too strong for this question to be interesting. There are many weakenings of the $\omega$-rule studied in the literature, and I'm not sure which is appropriate. Here's one which I think de-trivializes the question, although I could be wrong and I'm separately happy for it to be replaced by a different weakening: we restrict attention to deductions which are computable as well-founded labelled trees and have some computable code which $\mathsf{PA}$ proves defines an appropriate tree.

Given an ordinal $\alpha$, let $P(\alpha)$ be the smallest rank of any $\mathsf{PA}_\omega$-deduction of $\varphi(e)$ for any index $e$ for a computable copy of $\alpha$.

My main question is:

What is $P$, explicitly?

However, a related question is whether we can compute $P$, or at least bound $P$ nontrivially, in a direct way:

Can we give an upper bound for $P(\alpha)$ in terms of $\alpha$ (and strictly below $\omega_1^\text{CK}$) without appealing to the second incompleteness theorem?

The motivation for this latter question is the broader question of whether Gentzen's theorem — that every $\mathsf{PA}$-proof corresponds to a $\mathsf{PA}_\omega$-proof with rank $<\epsilon_0$ — can yield Godel's first incompleteness theorem (for $\mathsf{PA}$ specifically) as a corollary in a non-circular way. The usual proof of this is via the second incompleteness theorem, but a positive answer to my second question would yield a specific $e$ such that $\mathsf{PA}\nvdash\varphi(e)$ without appealing to Godel along the way. (Put another way, I'm asking whether an old answer to another question of mine can be patched.)

Improve this question
$\endgroup$
11
  • 2
    $\begingroup$ If you have no further requirements on $P$ then why is it not just bounded above by $\omega$? Any true FO sentence $A$ should have a cut-free $\mathsf{PA}_\omega$-proof of height bounded above by the logical complexity of $A$ (assuming axioms for all true closed atomic formulas) by mimicking the inductive definition of satisfaction in $\mathbb N$. Of course this argument is using an oracle for the standard model $\mathbb N$, which perhaps you want to avoid? (I am assuming here that, by $\mathsf{PA}_\omega$ you mean $\mathsf{PA}$ but with the $\omega$-rule instead of induction axioms.) $\endgroup$
    – Anupam Das
    Commented Jul 1 at 15:32
  • $\begingroup$ Despite as Anupam pointed out the particular way you want to obtain examples of pressumably first-order independent sentences shouldn't work, the original Gentzen technique that actually was done via partial cut-elimination for finite proof-figures for $\mathsf{PA}$ actually gives such examples of independent sentences obtained without use of diagonalization. Namely $\Pi^0_2$-ordinal analysis of $\mathsf{PA}$ gives us the totality of $\mathsf{F}_{\varepsilon_0}$ as a $\mathsf{PA}$-unprovable $\Pi^0_2$ sentence. $\endgroup$
    – Fedor Pakhomov
    Commented Jul 3 at 13:22
  • $\begingroup$ @FedorPakhomov True, but doesn't that still invoke the second incompleteness theorem along the way (via if $\mathsf{PA}\vdash Tot(\mathsf{F}_{\epsilon_0}$ then $\mathsf{PA}\vdash Con(\mathsf{PA}$)? Or am I misremebering? $\endgroup$
    – Noah Schweber
    Commented Jul 4 at 20:17
  • 2
    $\begingroup$ If PA is complete then this weakened version is still bounded by $\omega$ (because first-order truth in $\mathbb{N}$ is decidable by searching for proofs in PA). Obviously it isn't (so in reality $P$ is (probably) nontrivial), but this seems like a problem if you want to derive the incompleteness of PA as a corollary. $\endgroup$
    – paste bee
    Commented Jul 5 at 7:29
  • 1
    $\begingroup$ I don't see why you would need to "unfold" proofs? I'm just pointing out that Anupam Das's construction becomes computable if PA is complete; the PA proofs are only used to decide the truth of arithmetic statements (to check if $\varphi$ is true, see which of $\varphi$ and $\neg\varphi$ is provable). The underlying issue is that I can't see any way to get a useful bound on what's computable that doesn't immediately imply PA is incomplete. $\endgroup$
    – paste bee
    Commented Jul 6 at 3:07

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .