Return to Question

$<$ $\mathfrak N$, $+$, $\times$, = $>$

where $\mathfrak N$ = { |, ||, |||,...}, '$+$' as meaning concatenation, '$\times$' as meaning the Hilbert-Bernays definition of multiplication (e.g., || $\times$ ||| means replacing each | in || by |||, i.e., ||||||), and '=' as simply meaning equality as defined by the axioms of equality, i.e. for the axiom of equality 'a=a' one has, for the elements of $\mathfrak N$, the following equalities:

$$\langle \mathfrak N, +, \times, = \rangle$$

where $\mathfrak N = \{ |, ||, |||,\ldots\},$ '$+$' as meaning concatenation, '$\times$' as meaning the Hilbert-Bernays definition of multiplication (e.g., || $\times$ ||| means replacing each | in || by |||, i.e., ||||||), and '=' as simply meaning equality as defined by the axioms of equality, i.e. for the axiom of equality 'a=a' one has, for the elements of $\mathfrak N$, the following equalities:

This is an example of a failure on an $\omega$-rule: while for each axiom $\varphi$ of $PA$ we do in fact have "$Num$($\mathfrak M$) $\vDash$ $\varphi$ (appropriately phrased) is true in $\mathfrak M$, we do not get from this that "$Num$($\mathfrak M$) $\vDash$ each $PA$ axiom " is true in $\mathfrak M$. And this is just like how being able to check each individual derivation in $PA$ doesn't give us a way to check all derivations at once, so it really shouldn't be suprising.

This is an example of a failure on an $\omega$-rule: while for each axiom $\varphi$ of $PA$ we do in fact have "$Num$($\mathfrak M$) $\vDash$ $\varphi$" (appropriately phrased) is true in $\mathfrak M$, we do not get from this that "$Num$($\mathfrak M$) $\vDash$ each $PA$ axiom" is true in $\mathfrak M$. And this is just like how being able to check each individual derivation in $PA$ doesn't give us a way to check all derivations at once, so it really shouldn't be suprising.

Assume that $PA$ is consistent and that "$PA$ is consistent" is provable in $PA$. There is a conservative extension $\Gamma$ [let it be $ACA_0$ as in Noah Schweber's answer--my comment] of $PA$ in which the Completeness Theorem is provable [Theorem 5.5, p. 443, of Takeuti's Proof Theory, 2nd ed.--my expansion of his comment by his reference--not correct by Noah's most recent comment--stick with $ACA_0$], and moreover, $PA$ $\vdash$ ($\Gamma$ is a conservative extension of $PA$). Therefore, $\Gamma$ $\vdash$ ($\Gamma$ is a conservative extension of a consistent theory) and thus proves its own consistency. Consequently, $\Gamma$ proves that $\Gamma$ has a model.

Assume that $PA$ is consistent and that "$PA$ is consistent" is provable in $PA$. There is a conservative extension $\Gamma$ [let it be $ACA_0$ as in Noah Schweber's answer--my comment] of $PA$ in which the Completeness Theorem is provable [Theorem 5.5, p. 443, of Takeuti's Proof Theory, 2nd ed.--my expansion of his comment by his reference], and moreover, $PA$ $\vdash$ ($\Gamma$ is a conservative extension of $PA$). Therefore, $\Gamma$ $\vdash$ ($\Gamma$ is a conservative extension of a consistent theory) and thus proves its own consistency. Consequently, $\Gamma$ proves that $\Gamma$ has a model.