Is $\mathrm{PA^{top}}$ finitely axiomatizable? If not, does it have a finitely axiomatizable extension (allowing new predicates but not new variable types) that has arbitrarily large finite models?
$\mathrm{PA^{top}}$ is Peano Arithmetic with the unboundedness of natural numbers replaced by existence of the largest natural number. It consists of basic arithmetical axioms (with addition and multiplication treated as predicates), existence of the largest number, and full induction. It can be shown that a structure with the largest number satisfies $\mathrm{PA^{top}}$ iff it has an end extension into a model of $\mathrm{IΔ}_0$ ($\mathrm{PA}$ with induction restricted to bounded quantifier formulas). (Proof outline: $\mathrm{IΔ}_0$ has just enough induction for $\mathrm{PA^{top}}$; conversely, the set of finite tuples of elements of a model of $\mathrm{PA^{top}}$ can be 'composed' into a model of $\mathrm{IΔ}_0$.) Theorems in arithmetic can typically (or at least often) be rephrased to hold in $\mathrm{PA^{top}}$ by adding additional conditions to ensure that we do not go out of range.
In $\mathrm{PA^{top}}$, let $N$ be the largest number. A single axiom has $O(1)$ variables, and is thus essentially limited to numbers below $N^k$ (and $Σ_k$ quantification) for a constant $k$ depending on the axiom. By contrast, $\mathrm{PA^{top}}$ implies a basic $Σ_k$ theory of numbers below $N^k$ for every (metatheoretically finite) $k$, so we do not expect it to be finitely axiomatizable. However, I do not know how to modify Gödel's incompleteness theorem and related theorems to work in this context. Also, the above intuitive argument for $\mathrm{PA^{top}}$ does not apply to $\mathrm{IΔ}_0$ because $\mathrm{IΔ}_0$ has pairing (so $∃x_1∃x_2...∃x_k$ can be coded by a single quantifier); non-existence of finite axiomatizations for $\mathrm{IΔ}_0$ is an open problem related to whether the polynomial hierarchy (actually, for $\mathrm{IΔ}_0$, linear hierarchy) is infinite.
The second question above was inspired by Does “every” first-order theory have a finitely axiomatizable conservative extension?. To summarize what we know, let $T$ be a c.e. theory of finite relational type. If we allow new variable types (for example $\mathrm{ACA}_0$ adds subsets of $ℕ$ to $\mathrm{PA}$) or if we do not have identity, then $T$ has a finitely axiomatizable conservative extension. In logic with identity, $T$ has a finitely axiomatizable conservative extension that does not add new variable types iff $T$ is $Σ^1_1$ in second order logic. The set of infinite models of $T$ is always $Σ^1_1$. For finite structures, being a model of $T$ is $Σ^1_1$ iff it is NP.
Now, for finite structures, being a model $\mathrm{PA^{top}}$ is axiomatizable by a first order formula (and hence is in P and thus in NP). However, unlike infinity, finiteness is not $Σ^1_1$; and the ordinary $Σ^1_1$ description for infinite models of $\mathrm{PA^{top}}$ uses pairing, which does not work for finite models (but could be modified to work if we permitted new variable types); while the ordinary $Σ^1_1$ description for finite models misses induction. It might seem that we just need a trick to combine the two, but I suspect that the incompleteness that likely prevents $\mathrm{PA^{top}}$ from being finitely axiomatizable can somehow be extended to show impossibility here as well. However, it might be much easier to rely on computational complexity conjectures or consider extensions without new predicates.
