Models of PRA/EFA with induction on $X$ but not $\omega^X$

Question

As I currently understand it, induction on formulas containing $N+1$ first-order quantifiers is required to prove the well-ordering of the ordinal $(\omega \uparrow\uparrow N) < \epsilon_0$, that is, $\omega^{\omega^\cdots}$ for $N$ layers of $\omega$. See e.g. the second answer to Why do stacked quantifiers in PA correspond to ordinals up to $\epsilon_0$?.

If this is so then by Godel's Completeness Theorem there must be models of (if I have this right) $PRA+I(\Pi^0_{N+1})$ within which $\omega \uparrow\uparrow N$ is well-ordered, but $\omega \uparrow\uparrow (N+1)$ is not well-ordered.

What would these nonstandard models look like? Is there any intuitive way to describe them via ultrapowers or something similar? Or can we say something about their structure, the way that $\mathbb{N} + \mathbb{Z}\cdot\mathbb{Q}$ is the structure for countable nonstandard models of full first-order arithmetic?

For concreteness: Is there any more specific way to describe a nonstandard model of PRA in which the Ackermann function is not complete, beyond "The Ackermann function is not complete"? Hopefully via some construction which will extend to "Kirby-Paris hydras of height $N+2$(?) always terminate, but some of height $N+3$(?) don't"? Obviously every primitive recursive function $f_n$ with $n \in \mathbb{N}$ is complete for every standard and nonstandard input, while the Ackermann function is incomplete for some input $\varpi$ which is a nonstandard number ($\varpi > 0, \varpi > 1, \dots$), likewise with non-terminating hydras where at least one branch has nonstandard width, but beyond this I cannot visualize anything about what the nonstandard model looks like.

(Understanding this would provide a direct, non-Godelian argument for why induction on $N+1$ quantifiers is necessary as well as sufficient to prove well-ordering of $\omega \uparrow\uparrow N$. It would also show in a direct, non-Godelian way that $PA$ cannot prove the well-ordering of $\epsilon_0$, since this would require induction on infinite quantifiers.)

Answer 1

I suspect the paper you want is Avigad and Sommer, A Model-Theoretic Approach to Ordinal Analysis. As the name suggests, they give an ordinal analysis rooted in the structure of models of arithmetic.

The main idea is that if $\alpha$ is an ordinal, we define a decreasing sequence of ordinals $\alpha[A]$ whenever $A$ is an increasing sequence of numbers (in a nonstandard model). A sequence $A$ is $\alpha$-large if $\alpha[A]=0$. They use the combinatorial properties of $\alpha$-large sequences to show that if $A$ is $(\omega\uparrow\uparrow N+1)$-large then there is a "cut"---an initial segment of the numbers (again, in a nonstandard model)---which is a model of $I\Sigma_N$. (Forgive my indexing if I'm off.)

The point is that one has to find an increasing sequence $a_0,a_1,\ldots,a_c$ of nonstandard length, inside $A$, so that if an existential statement is witnessed below $a_c$, the statement is actually witnessed below $a_i$ for some (standardly) finite $i$. In particular, there's a Ramsey-theoretic argument which explains why more exponents correspond to finding witnesses for more complicated statements.

More generally, there is a substantial literature on models of arithmetic which satisfy fragments of arithmetic like $I\Sigma_n+\neg I\Sigma_{n+1}$. The paper which starts the area, and contains the basic construction of the models you want, is Paris and Kirby, "$\Sigma_n$-collection schemes in arithmetic". (Seemingly only available in book form, unfortunately.)

The most common method for constructing such models is to use a modified ultraproduct construction, usually called something like a "definable ultraproduct". Typically one starts with a nonstandard model of PA and considers the $\Sigma_n$ definable functions after a quotient by the $\Sigma_m$ definable sets. (There are many variants of this construction, of course.) The result is countable if the original model was (because there are only countably many definable functions) and generally only preserves truth for $\Sigma_i$ formulas up to some $i$.

Answer 2

The easiest way to construct a model $M$ of PRA where the Ackermann function is not total is to take a nonstandard model $M_0$ of PRA, fix a nonstandard element $a\in M_0$, and let $M$ be the cut in $M_0$ defined as $$\{x\in M_0:\exists f\text{ primitive recursive s.t. }M_0\models x\le f(a)\}.$$

In this specific case, one can even take just the closure of $a$ under all primitive recursive functions, without closing it downwards, but constructions using cuts tend to work for more theories of interest.

The indicator theory, of which the above mentioned Avigad–Sommer paper is an offshoot, is essentially a generalization of the same idea to theories higher in the hierarchy whose existential quantifiers are not so easy to witness directly.