Skip to main content
added 1632 characters in body
Source Link
Noah Schweber
  • 21.1k
  • 10
  • 110
  • 331

Your question seems to boil down to (after fixing an error) the following:

Any model $\mathfrak{M}$ of ACA$_0$ has a first-order part $Num(\mathfrak{M})$, which satisfies PA; why doesn't this mean that ACA$_0$ proves "PA has a model" (and(indeed, the a priori stronger "PA is sound") and hence its own consistency)?

Here ACA$_0$ is a conservative extension of the type Jech mentions (what he calls "$\Gamma$"): it can talk about models and prove basic model-theoretic results (e.g. the soundness and completeness theorems), and is PA-provably a conservative extension of PA.

The issue is the following. Fix a model $\mathfrak{M}$ of ACA$_0$. We can indeed talk about $Num(\mathfrak{M})$ as a structure in $\mathfrak{M}$, and have the following:

$(*)\quad$ Any set of sentences true in $Num(\mathfrak{M})$ is consistent.

However, we are not guaranteed that our model $\mathfrak{M}$ thinks that its first-order part actually satisfies PA. That is, the "obvious truth" of the PA axioms is not actually that obvious. From the existence of such models we conclude

PA $\not\vdash Sound($PA),

and so in particular the obvious argument for PA$\vdash$ "PA has a model" breaks down.

This is an example of a failure of the $\omega$-rule: while for each axiom $\varphi$ of PA we do in fact have that "$Num(\mathfrak{M})\models \varphi$" (appropriately formalized) is true in $\mathfrak{M}$, we do not get from this that "$Num(\mathfrak{M})\models$ each PA axiom" is true in $\mathfrak{M}$. And thisThat is:

ACA$_0$ doesn't prove that PA is sound; indeed, no conservative extension of PA can (since then it would prove that PA is consistent, which is in the language of PA and not PA-provable).

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 surprising.


Re: your edits, the point is that knowing that ACA$_0$ doesn't prove the soundness of PA indicates that we can be "smart enough" to know each specific axiom of PA, yet still not know that PA as a whole is true. So when Gentzen says that that PA is "obviously correct," that's a slightly weaker level of obviousness than any of the individual PA axioms.

This saves us from the circle Gentzen is gesturing at. While focusing on PA, Gentzen is more generally describing a hypothetical situation where - in a sufficiently rich language (e.g. that of second-order arithmetic) - we have some notion of "obviousness" with the following properties:

  • The set of obvious sentences is consistent,

  • Every axiom of PA is obvious,

  • The set of obvious sentences is c.e., and

  • It's obvious that every obvious arithmetic sentence is true.

Godel's theorem implies that no such property exists; the fact that ACA$_0\not\vdash Sound($PA) is a particular example of this phenomenon, showing that PA doesn't correspond to the first-order part of such a notion of obviousness and hopefully making it more intuitively clear why the above situation can't happen despite its face-value-plausibility.

Your question seems to boil down to (after fixing an error) the following:

Any model $\mathfrak{M}$ of ACA$_0$ has a first-order part $Num(\mathfrak{M})$, which satisfies PA; why doesn't this mean that ACA$_0$ proves "PA has a model" (and hence its own consistency)?

Here ACA$_0$ is a conservative extension of the type Jech mentions (what he calls "$\Gamma$"): it can talk about models and prove basic model-theoretic results (e.g. the soundness and completeness theorems), and is PA-provably a conservative extension of PA.

The issue is the following. Fix a model $\mathfrak{M}$ of ACA$_0$. We can indeed talk about $Num(\mathfrak{M})$ as a structure in $\mathfrak{M}$, and have the following:

$(*)\quad$ Any set of sentences true in $Num(\mathfrak{M})$ is consistent.

However, we are not guaranteed that our model $\mathfrak{M}$ thinks that its first-order part actually satisfies PA. That is, the "obvious truth" of the PA axioms is not actually that obvious.

This is an example of a failure of the $\omega$-rule: while for each axiom $\varphi$ of PA we do in fact have that "$Num(\mathfrak{M})\models \varphi$" (appropriately formalized) is true in $\mathfrak{M}$, we do not get from this that "$Num(\mathfrak{M})\models$ 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 surprising.

Your question seems to boil down to (after fixing an error) the following:

Any model $\mathfrak{M}$ of ACA$_0$ has a first-order part $Num(\mathfrak{M})$, which satisfies PA; why doesn't this mean that ACA$_0$ proves "PA has a model" (indeed, the a priori stronger "PA is sound") and hence its own consistency?

Here ACA$_0$ is a conservative extension of the type Jech mentions (what he calls "$\Gamma$"): it can talk about models and prove basic model-theoretic results (e.g. the soundness and completeness theorems), and is PA-provably a conservative extension of PA.

The issue is the following. Fix a model $\mathfrak{M}$ of ACA$_0$. We can indeed talk about $Num(\mathfrak{M})$ as a structure in $\mathfrak{M}$, and have the following:

$(*)\quad$ Any set of sentences true in $Num(\mathfrak{M})$ is consistent.

However, we are not guaranteed that our model $\mathfrak{M}$ thinks that its first-order part actually satisfies PA. That is, the "obvious truth" of the PA axioms is not actually that obvious. From the existence of such models we conclude

PA $\not\vdash Sound($PA),

and so in particular the obvious argument for PA$\vdash$ "PA has a model" breaks down.

This is an example of a failure of the $\omega$-rule: while for each axiom $\varphi$ of PA we do in fact have that "$Num(\mathfrak{M})\models \varphi$" (appropriately formalized) is true in $\mathfrak{M}$, we do not get from this that "$Num(\mathfrak{M})\models$ each PA axiom" is true in $\mathfrak{M}$. That is:

ACA$_0$ doesn't prove that PA is sound; indeed, no conservative extension of PA can (since then it would prove that PA is consistent, which is in the language of PA and not PA-provable).

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 surprising.


Re: your edits, the point is that knowing that ACA$_0$ doesn't prove the soundness of PA indicates that we can be "smart enough" to know each specific axiom of PA, yet still not know that PA as a whole is true. So when Gentzen says that that PA is "obviously correct," that's a slightly weaker level of obviousness than any of the individual PA axioms.

This saves us from the circle Gentzen is gesturing at. While focusing on PA, Gentzen is more generally describing a hypothetical situation where - in a sufficiently rich language (e.g. that of second-order arithmetic) - we have some notion of "obviousness" with the following properties:

  • The set of obvious sentences is consistent,

  • Every axiom of PA is obvious,

  • The set of obvious sentences is c.e., and

  • It's obvious that every obvious arithmetic sentence is true.

Godel's theorem implies that no such property exists; the fact that ACA$_0\not\vdash Sound($PA) is a particular example of this phenomenon, showing that PA doesn't correspond to the first-order part of such a notion of obviousness and hopefully making it more intuitively clear why the above situation can't happen despite its face-value-plausibility.

Source Link
Noah Schweber
  • 21.1k
  • 10
  • 110
  • 331

Your question seems to boil down to (after fixing an error) the following:

Any model $\mathfrak{M}$ of ACA$_0$ has a first-order part $Num(\mathfrak{M})$, which satisfies PA; why doesn't this mean that ACA$_0$ proves "PA has a model" (and hence its own consistency)?

Here ACA$_0$ is a conservative extension of the type Jech mentions (what he calls "$\Gamma$"): it can talk about models and prove basic model-theoretic results (e.g. the soundness and completeness theorems), and is PA-provably a conservative extension of PA.

The issue is the following. Fix a model $\mathfrak{M}$ of ACA$_0$. We can indeed talk about $Num(\mathfrak{M})$ as a structure in $\mathfrak{M}$, and have the following:

$(*)\quad$ Any set of sentences true in $Num(\mathfrak{M})$ is consistent.

However, we are not guaranteed that our model $\mathfrak{M}$ thinks that its first-order part actually satisfies PA. That is, the "obvious truth" of the PA axioms is not actually that obvious.

This is an example of a failure of the $\omega$-rule: while for each axiom $\varphi$ of PA we do in fact have that "$Num(\mathfrak{M})\models \varphi$" (appropriately formalized) is true in $\mathfrak{M}$, we do not get from this that "$Num(\mathfrak{M})\models$ 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 surprising.