# Stronger notion of ultrafinite incompleteness

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}\}$$.