Аннотация:
We prove that the $\mathsf{PA}$-consistency property is provably in $\mathsf{PA}$ equivalent to the scheme $\mathsf{Con}^S_{\mathsf{PA}}$: for $n=0,1,2,\dots$, “$n$ is not a code of a proof of $(0=1)$.” Since the consistency formula $\mathsf{Con}_{\mathsf{PA}}$ is strictly stronger than $\mathsf{Con}^S_{\mathsf{PA}}$ in $\mathsf{PA}$, the unprovability of $\mathsf{Con}_{\mathsf{PA}}$ in $\mathsf{PA}$ does not settle the question of provability of the consistency, which remained in limbo and has been reduced to finding a finite proof in $\mathsf{PA}$ of $\mathsf{Con}^S_{\mathsf{PA}}$. Following Hlbert's approach to proving consistency, we offer the general notion of a proof of a sequence of $\mathsf{PA}$-formulas $F_1, F_2,..., F_n,\dots$ as a pair of a primitive recursive function (selector) $s$ and a proof of “for each $n$, $s(n)$ is a $\mathsf{PA}$-proof of $F_n$.” We demonstrate that “$\mathsf{PA}$ is consistent” is provable in $\mathsf{PA}$. These findings apply to a broad class of formal theories, including $\mathsf{ZF}$.
