3
$\begingroup$

On page 7 of his paper “Adventures in Incompleteness”, Harvey Friedman states the following:

IN ANY LONG ENOUGH SEQUENCE $x_1,...,x_n$ FROM $\{1,2,3\}$, SOME $(x_i,...,x_{2i})$ IS A SUBSEQUENCE OF SOME LONGER $(x_j,...,x_{2j})$. ...

  • Size for [this] is > 7198th Ackermann function at 158,386 = $A_{7198}(158,386)$.
  • Any proof of [this] in EFA = exp function arithmetic, needs $> A_{7198}(158,385)$ symbols, a bit much. Same for SEFA.
  • This is an ULTRA FINITE INCOMPLETENESS.

He calls it ultrafinite incompleteness because an ultrafinitist would presumably not accept a statement requiring such a long proof. In any case, what is the definition of nth Ackerman function Friedman is relying on? And what is the proof that this statement is true, and moreover that this statement is provable in $EFA$ but only with such an absurdly long proof?

I assume there’s a much shorter proof in some stronger system, as presumably Friedman did not write down a proof with $> A_{7198}(158,385)$ symbols!

Improve this question
$\endgroup$
5
  • 7
    $\begingroup$ Harvey Friedman, Long finite sequences, J. Combin. Theory Ser. A, 95 (1) (2001), 102–144. sciencedirect.com/science/article/pii/S0097316500931546 $\endgroup$
    – Andrés E. Caicedo
    Commented Mar 16, 2023 at 18:10
  • 2
    $\begingroup$ Re: provability of provability in EFA without actually proving in $\mathsf{EFA}$, note that $\mathsf{WKL_0}$ proves that the statement in question is equivalent to the finiteness of a particular "nicely definable" (e.g. $\Delta_1$) subtree of $3^{<\omega}$; the right-to-left direction of this equivalence is outright $\mathsf{EFA}$-provable. By $\Sigma_1$-completeness of $\mathsf{EFA}$, provable in $\mathsf{WKL_0}$, we get a $\mathsf{WKL_0}$-proof that if Friedman's sentence is true then it is provable in $\mathsf{EFA}$. $\endgroup$
    – Noah Schweber
    Commented Mar 16, 2023 at 18:26
  • $\begingroup$ In particular, letting [F] be the sentence in question, it is not claimed that $\mathsf{EFA}$ itself can prove "$\mathsf{EFA}$ proves [F]" in any reasonable amount of symbols. $\endgroup$
    – Noah Schweber
    Commented Mar 16, 2023 at 18:32
  • $\begingroup$ @NoahSchweber Can WKL_0 prove (in a small number of lines) that [F] is true though? If not, how strong a system do you need to prove [F]? $\endgroup$
    – Keshav Srinivasan
    Commented Mar 17, 2023 at 1:23
  • $\begingroup$ @KeshavSrinivasan No idea. I suspect not. My point was just that there's a general technique to these "some-long-proof" ideas. $\endgroup$
    – Noah Schweber
    Commented Mar 17, 2023 at 1:24

0

Reset to default

You must log in to answer this question.