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?

  • $\begingroup$ What is a "nonstandard proof"? Is it a proof with a nonstandard number of steps? $\endgroup$ – Steven Landsburg May 5 '17 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 May 5 '17 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 May 5 '17 at 2:11

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.

| cite | improve this answer | |
  • 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 May 5 '17 at 3:28
  • 4
    $\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 May 5 '17 at 7:48
  • $\begingroup$ @EmilJeřábek Great remark! The example you gave perfectly addresses my concern. $\endgroup$ – Ruizhi Yang May 6 '17 at 0:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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