References discussing the technical differences of $\neg\mathrm{Con}(\mathrm{PA})$ and "to exhibit an actual contradiction in PA"?

Question

Question.

What references do you recommend that dryly/precisely discuss differences between

(0) Trying to prove $\neg\mathrm{Con}(\mathrm{PA})$.

(1) Trying to exhibit an actual contradiction in $\mathrm{PA}$.

Remarks.

(0) While this is rather irrelevant for the question, I mention that I am currently neither trying to do (0), nor (1), rather would like to check a few things around this, to learn something that would take long to spell out here.

(1) Hoping for some brief relevant pointers, by people working in mathematical logic, to relevant literature, I keep this short and do not try to make precise what $\neg\mathrm{Con}(\mathrm{PA})$ and "to exhibit an actual contradiction" in (0) and (1) mean. This is an important and well-known distinction, occurring in relevant discussions of this topic.

Answer 1

The phrases you've quoted are informal, and as such can be interpreted in different ways. I think the most natural interpretations, however, are:

• To "exhibit an actual contradiction in PA" means to find a formal proof - e.g. in the sense of sequent calculus - of "$0=1$" from the axioms of PA. Note that a formal proof is computer-verifiable, so this really is a totally airtight notion: if you claim to have an actual contradiction from PA, that's an objective statement and can be objectively verified.

• To "prove that PA is inconsistent" means to prove the statement "PA is inconsistent" (appropriately coded) in some theory, possibly other than PA, which we are confident is $\Sigma^0_1$-correct. This is a somewhat informal notion, on two counts: "appropriately coded" and "we are confident" are each informal properties, and each is reasonably subtle. That said, once we fix a representation $\varphi$ of "PA is inconsistent" in some fixed language (e.g. the language of arithmetic, or the language of set theory) and some theory $T$ in the appropriate language, this can become totally objective if we interpret "prove" as "produce a formal proof from the axioms of $T$).

These are obviously in principle different tasks; however, most logicians agree that in practice they amount to the same thing. Namely, if some theory $T$ which is stronger than PA proves that PA is inconsistent, I think this would cause most logicians to doubt the $\Sigma^0_1$-correctness of $T$, rather than the consistency of PA; and most logicians are confident in the appropriateness of the representation of "PA is inconsistent" in the language of PA (although this has been studied) - so the non-objective parts of the second task are removed (work in PA itself, and use the usual coding). Meanwhile, if PA proved "PA is inconsistent," it is likely that this proof would easily yield an actual contradiction, even though a priori PA could be consistent even if it proved its own inconsistency.

---

I don't know a specific source which discusses this, but when in doubt: define your terms and phrases precisely, and then you don't need another source to clarify what you mean. And that said, I believe the above captures accurately how these phrases are used in logic the vast majority of the time.

Answer 2

If you already know the precise versions of what your (0) and (1) are usually taken to mean, then the answer should have been clear. $ \def\pa{\text{PA}} \def\con{\text{Con}} $

As usual assume PA is consistent. Consider $T = \pa + \neg \con(\pa)$. Then $T \nvdash \bot$ but $T \vdash \neg \con(T)$. So clearly an explicit proof of contradiction over PA may not exist even if PA proves $\neg \con(\pa)$. Of course, in the latter case we clearly should start doubting the meaningfulness of PA, since it would be $Σ_1$-unsound, which is really really bad.