8
$\begingroup$

Assuming $\text{PA}$ is consistent. Then $\text{PA} + \neg\text{Con}(\text{PA})$ is consistent and have a model, say $M$. We know $M$ must be nonstandard, in which case, there is a nonstandard proof of $0=1$ from ($M$'s version of) $\text{PA}$ in $M$. The fact that $M$'s version of $\text{PA}$ is different from the "real" $\text{PA}$ make the assertion $$ M\vDash\text{PA} + \neg\text{Con}(\text{PA}) $$ kind of less stunning than we might expect it to be.

My question is if we can compose some other expressions of $\text{PA}$ so that if $M\vDash\neg\text{Con}(\text{PA})$ then there is a (nonstandard) proof of absurdity making use of only the standard part of $\text{PA}$ and logic axioms. If it is impossible, how to prove it?

Improve this question
$\endgroup$
6
  • $\begingroup$ What is a "nonstandard proof"? Is it a proof with a nonstandard number of steps? $\endgroup$
    – Steven Landsburg
    Commented May 5, 2017 at 2:03
  • $\begingroup$ By "nonstandard proof", I mean a proof whose code is a nonstandard number. It is probably a proof with a nonstandard number of steps. $\endgroup$
    – Ruizhi Yang
    Commented May 5, 2017 at 2:08
  • 5
    $\begingroup$ There are also nonstandard proofs with only one step, since they assert an nonstandard axiom. This can occur even for assertions with low-level complexity, simply because they have a term of nonstandard length, such as $1+1+1+\cdots+1$, with a nonstandard number of $1$s. $\endgroup$
    – Joel David Hamkins
    Commented May 5, 2017 at 2:11
  • $\begingroup$ @JoelDavidHamkins, at MSE there are separate tags for nonstandard analysis and nonstandard models. At MO there is only a tag for nonstandard analysis. It seems that there are many questions here that would fit well under a tag "nonstandard models" (including this question). Should such a tag be created? $\endgroup$
    – Mikhail Katz
    Commented Dec 19, 2023 at 17:30
  • $\begingroup$ For this question and others like it, I conceive of the top as "models of PA" or "models of arithmetic" rather than "nonstandard models", even though most of the are nonstandard, because the standard model is also often part of the investigation. I think you are free to go ahead and create any tag you want. $\endgroup$
    – Joel David Hamkins
    Commented Dec 19, 2023 at 19:01

1 Answer 1

Reset to default
11
$\begingroup$

It seems that the Feferman-style description of PA will exhibit your requirements.

Specifically, consider the theory $P$ defined as follows. Begin to enumerate the usual PA axioms, but include the next axiom in $P$ only if doing so keeps $P$ consistent. Never add an axiom to $P$ that would make it inconsistent.

Since PA proves of every finite subset of PA that it is consistent, it follows that PA proves of any particular axiom of PA, that it is in $P$. In this sense, this theory $P$ is the same as PA, just described in a different way.

But because of how it is described, it follows that PA proves $\text{Con}(P)$. We never include an axiom in $P$ that would enable it to prove a contradiction.

Therefore, there is no model $M\models PA+\neg\text{Con}(P)$, and so the theory vacuously has your desired property.

Of course, notice that all instances of your requested property must be vacuous like this, because if the proof of a contradiction inside $M$ were somehow forced to be standard, then it would be actual proof of a contradiction, and so $M$ couldn't exist in the first place, if it is a model of this theory. So it seems to me that the only way to get your situation is in the vacuous way that the Feferman theory achieves it.

Improve this answer
$\endgroup$
3
  • 2
    $\begingroup$ Thank you for pointing out that the Feferman-style of PA works! I am not sure if I fully understand your find remark. Is it possible to have a proof using only standard axioms but with nonstandard number of steps, and cannot be shrunk back to a standard proof of the same sentence? Am I right that such a proof can only make use of finitely many standard axioms, since it cannot use exactly $\omega$ many standard axioms, and if it uses nonstandard number of axioms, there must be some nonstandard one? Is that why such a proof does not exist? $\endgroup$
    – Ruizhi Yang
    Commented May 5, 2017 at 3:28
  • 7
    $\begingroup$ @ganganray PA proves the consistency of each its (standard) finite part. So, a proof of contradiction in PA in a model of PA must necessarily use nonstandard axioms of PA. But in general, it is perfectly possible to have nonstandard proofs using only standard axioms. For example, consider a model of $I\Sigma_1+\neg \mathrm{Con}(I\Sigma_1)$ (using its finite axiomatization). Since the theory is finitely axiomatized, all axioms in the proof of contradiction are standard, but the proof must be nonstandard. $\endgroup$
    – Emil Jeřábek
    Commented May 5, 2017 at 7:48
  • $\begingroup$ @EmilJeřábek Great remark! The example you gave perfectly addresses my concern. $\endgroup$
    – Ruizhi Yang
    Commented May 6, 2017 at 0:36

Not the answer you're looking for? Browse other questions tagged or ask your own question.