Why is $I\Sigma_2$ (arithmetic with $\Sigma_2$ induction) finitely axiomatizable? According to this comment on this answer to this question I asked an hour ago, there exist universal $\Sigma_2$ sentences.
$\Sigma_2$ sentences are part of the arithmetical hierarchy. They allow bound or unbound quantifiers, one quantifier alternation, and with $\exists$ as the outermost quantifier. In addition, well-formed formulas in $\Sigma_2$ are allowed to contain parameters.
It seems really surprising to me that universal $\Sigma_2$ formulas exist. I'm not completely sure what a universal formula means; and the definition of universal formula seems to differ from the definition presented here.
At the moment I'm thinking about a universal formula in the context of $I\Sigma_2$ as simply being a formula $\varphi$ such that "$I\varphi$", where the induction non-schema trivially ranges over $\varphi$ alone, proves the same theorems as $I\Sigma_2$. I'm curious what the actual definition is though since this definition is really weird and bakes in the language of arithmetic $\{0, 1, +, *\}$ and other stuff about arithmetic that feels really incidental.
So, my question is threefold:

*

*Why do universal $\Sigma_2$ sentences exist?

*Is the proof of their existence constructive or nonconstructive?

*What is the real definition of a universal $\Sigma_2$ sentence?

 A: There is no connection with the notion of a universal theory. Roughly, a ($2$-variable) universal $\Gamma$-formula for some syntactic class $\Gamma$ is a $2$-variable formula $\varphi(x,y)$ such that:

*

*$\varphi\in \Gamma$, and


*for each $1$-variable formula $\psi(x)\in\Gamma$ there is some $c$ such that $\psi(x)\equiv \varphi(x,c)$.
Think by analogy of a universal Turing machine, or - if you're familiar with descriptive set theory - of the notion of a universal set for a pointclass. The existence of a universal $\Sigma_n$ formula, for each $n$, is totally constructive and explicit. For example:

*

*"The $x$th Turing machine halts on input $y$" is universal $\Sigma_1$, and is basically a rephrasing of the halting problem..


*"For every $z$ the $x$th Turing machine halts on input $\langle y,z\rangle$" (with $\langle \cdot,\cdot\rangle$ being an appropriate pairing function) is universal $\Sigma_2$, and is basically a rephrasing of the totality problem (which Turing machines halt on all inputs?) which has Turing degree ${\bf 0''}$ - "the halting problem's halting problem."
And so on. (As usual we express statements about Turing machines and halting in the language of arithmetic via Kleene's $T$ predicate.)

The point is that we can use universal formulas to collapse schemes. For example, let $\eta(x,y)$ be universal $\Sigma_2$. Then the single sentence $$\forall y[\eta(0,y)\wedge\forall x(\eta(x,y)\rightarrow\eta(x+1,y))\rightarrow\forall x(\eta(x,y))]$$ expresses induction for all $1$-variable $\Sigma_2$ formulas.
Note that while I've focused on the language of first-order arithmetic above, we can also talk about universal $\Gamma$-formulas in other contexts. For example, in the language of second-order arithmetic (which despite the name is the setting of many interesting first-order theories) the existence of universal $\Pi^1_n$ formulas for each $n$ gives the finite axiomatizability of each of the theories $\Pi^1_n$-$\mathsf{CA_0}$ which appear in reverse math. And on the set-theoretic side we get, thinking in terms of the Levy hierarchy, that (a version of) $\mathsf{KP}$ is finitely axiomatizable.
