3
$\begingroup$

Harvey Friedman has a statement (in MathOverflow question #442871) that is described as an "ultra finite incompleteness". The statement is

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.

According to the MO question, Friedman's rationale for calling this statement ultrafinitistically incomplete is that an ultrafinitist would not accept a proof of such massive length as valid. However, as its witnesses are massive, this statement is false in some "model of ultrafinitism" (e.g. $\{0,1,\ldots,2^{1000}\}$), so I think that an ultrafinitist may see this statement as outright false.

In order for the formula itself to be ultrafinitistically valid, any ultrafinitistically incomplete statement $\phi$ would have to have a feasible number of symbols. In that case, is there any short statement $\phi$ which does not assert a large number exists, yet requires a long proof? Specifically, is there a $\phi$ with at most $2^{1000}$ symbols which is true in $\{0,1,\ldots,2^{1000}\}$, but any proof of $\phi$ in EFA has length $>2^{2^{1000}}$?


If one approach is to rule out some forms of $\phi$, it may be relevant that $\Pi^0_2$ formulae states that some recursive function is total, and that there is a known bound on the EFA-provably total recursive functions (in Math SE answer #2411797). However statements that only assert "$f$ is total" for some computable $f$ may not be an example of ultrafinite incompleteness, as even for some slow $f$ (e.g. the successor function) this statement fails in $\{0,1,\ldots,2^{1000}\}$.

$\endgroup$

0

You must log in to answer this question.

Browse other questions tagged .