Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
Towards formalising 'essentially the same proof', in proof theory it is common to identify proofs denoting the same program (up to conversion), under the Curry-Howard correspondence. This is robust for intuitionistic proofs, but for classical ones one must precompose with a chosen double negation translation for constructivity, and so in this sense a (classical) mathematical proof of FTA (or anything else) denotes a set of programs. Comparing proofs in this way might also accommodate a form of closeness too, e.g. when two sets have large intersections.
I think a standard answer to this is Elementary Recursive Arithmetic, i.e. the fragment of PRA restricted to the elementary functions (this can be defined in a few ways, but it suffices to restrict primitive recursion to only bounded recursion, a la Cobham). Note that, for such weak fragments one does not usually employ equational systems in all finite types, with more direct witnessing arguments available direct from the classical theory. Many such interpretations are found in bounded arithmetic, e.g. the interpretation of Buss' $S^1_2$ in Cook's PV.
If you have no further requirements on $P$ then why is it not just bounded above by $\omega$? Any true FO sentence $A$ should have a cut-free $\mathsf{PA}_\omega$-proof of height bounded above by the logical complexity of $A$ (assuming axioms for all true closed atomic formulas) by mimicking the inductive definition of satisfaction in $\mathbb N$. Of course this argument is using an oracle for the standard model $\mathbb N$, which perhaps you want to avoid? (I am assuming here that, by $\mathsf{PA}_\omega$ you mean $\mathsf{PA}$ but with the $\omega$-rule instead of induction axioms.)
[Assuming you mean composition rather than application] I don't think the $V_i$'s I gave, in general, coincide with any $V_n' := V\circ U \circ \cdots n \cdots \circ V$. For this it is not hard to see that each $V_n' \langle g,\Psi\rangle h$ is always in the range of $g\circ \Psi$ (provable, e.g., by induction on $n$, assuming extensionality), whereas each $V_n \langle g,\Psi\rangle h$ is always in the range of $g\circ h$, by inspection of the definition. Of course those ranges could just be disjoint in some models.
I think saying "the Curry-Howard correspondence realizes this as a pair of operators..." is misleading, as $V$ is not the only inhabitant of that type. Indeed, there are infinitely many inhabitants: set $V_0:= V$ and then $V_{i+1} \langle g,\Psi\rangle h := g (h (V_i \langle g,\Psi\rangle h ))$. Now each $V_i$ has the same type as $V$.
