A theorem on generalizations of proofs (Q2640597)

A motivation for generalizing proofs is, as the author quotes, to obtain ``similar proofs'' with ``similar conclusions'' from the given one. A typical example is a Kreisel conjecture that relates a proof of \(A(0^{(n)})\) to that of \(\forall x(x\equiv n(mod N)\supset A(x))\) in PA, including their lengths. In this vein, the author proves the following theorem. Assume that the given PA formula A(a), m,n\(\in \omega\), and a proof \({\mathfrak P}\) of \(A(0^{(n)})\) satisfy the conditions: \({\mathcal G}(m)<n\), the number of consecutive occurrences of ' in A(a) and the cardinality of the set \({\mathcal B}({\mathfrak P})\) are both less than m. Then there are p,q\(\neq 0\), and a \(PA^*\) proof \({\mathfrak Q}\) of \(A(0^{(p)}+qa)\) such that \({\mathfrak P}\simeq {\mathfrak Q}\), \(p\equiv n(mod q)\), \(p\leq {\mathcal G}(m)+({\mathcal F}(m))^ 3\), and \(q\leq {\mathcal F}(m)\). Here, \({\mathcal F}(m)\) and \({\mathcal G}(m)\) are functions of order 2 to the 2 to fifth degree polynomials of m, the set \({\mathcal B}({\mathfrak P})\) gives a measure of the complexity of \({\mathfrak P}\), \(PA^*\) allows, as beginning sequents, not only \(A\to A\) but also \(A\to B\) when A and B differ only by (formal) terms with the same meaning, and \({\mathfrak P}\simeq {\mathfrak Q}\) indicates that they have the same structure as proof trees. Due to the nature of the subject, ``knitty-gritty'' analysis of formal proofs and complicated definitions are unavoidable. The author also compares similar results of his and in the literature.