# Confusion about $\mathsf{PA}$'s self-provable consistency sentences

Edit: This long question was basically answered by a quick comment! I'll accept an answer if someone posts one, but it's basically answered already.

Background:

In Peter Smith's Introduction to Gödel's Theorems §36.1, he introduces the sentence

$$\mathsf{Prf^\circ(x,y)} =_\text{def} \mathsf{Prf(x, y) \wedge \forall v \leq x \neg Prf(v, \ulcorner \bot \urcorner)}.$$

He then defines

\begin{align} \mathsf{Prov^\circ(y)} &:= \mathsf{\exists v Prf^\circ (v, y)} \\\\ \mathsf{Con^\circ} &:= \mathsf{\neg Prov^\circ(\ulcorner \bot \urcorner)} \end{align}

and proceeds to show that $$\mathsf{PA} \vdash \mathsf{Con^\circ}$$.

Smith's discussion is as follows: If (and only if!) $$\mathsf{PA}$$ is consistent, then $$\mathsf{Prf^\circ(x,y)}$$ expresses proofhood, and hence $$\mathsf{Con^\circ}$$ expresses consistency. However, if $$\mathsf{PA}$$ is inconsistent, then $$\mathsf{Prf^\circ}$$ does not express proofhood (this can be seen on a straightforward interpretation of the formula defining $$\mathsf{Prf^\circ}$$), hence $$\mathsf{Con^\circ}$$ does not express consistency.

Question Setup:

I'm not sure if this is a typo, but it seems to me that $$\leq$$ should be $$<$$ in the definition of $$\mathsf{Prf^\circ}$$, since the way it is written, $$\mathsf{Con^\circ}$$ is trivially provable. In particular

$$\tag{1} \label{con} \mathsf{Con^\circ} = \neg \exists x [ \mathsf{Prf(x, \ulcorner \bot \urcorner) \wedge \forall v \leq x \neg Prf(v, \ulcorner \bot \urcorner)} ]$$

is provable because the part inside the brackets is logically false, which can be seen by taking $$\mathsf{v = x}$$. Moreover, inspecting $$(\ref{con})$$ directly, it isn't clear at all whether $$\mathsf{Con^\circ}$$ actually expresses consistency, even assuming $$\mathsf{PA}$$ is consistent (contrary to the argument given above)—how could a basic logical truth express anything interesting?

So let me define

$$\mathsf{Prf^\star(x, y)} =_\text{def} \mathsf{Prf(x, y) \wedge \forall v < x \neg Prf(v, \ulcorner \bot \urcorner)},$$

with $$\mathsf{Prov^\star}$$ and $$\mathsf{Con^\star}$$ defined in the obvious way. It seems to me that $$\mathsf{Prf^\star}$$ is similar to $$\mathsf{Prf^\circ}$$ in that it clearly expresses provability if $$\mathsf{PA}$$ is consistent; but at the same time, it seems better than $$\mathsf{Prf^\circ}$$ because the resulting $$\mathsf{Con^\star}$$ is more than just vacuously true and provable. It seems to express $$\mathsf{PA}$$'s consistency even without already assuming $$\mathsf{PA}$$ is consistent: $$\mathsf{Con^\star}$$ says, after all, that there is no "smallest" proof of $$\bot$$, which is equivalent to saying there is no proof of $$\bot$$.

Question:

1. Am I correct that $$\mathsf{PA \vdash Con^\star}$$?
2. Am I correct that $$\mathsf{Con^\star}$$ expresses the consistency of $$\mathsf{PA}$$, without assuming $$\mathsf{PA}$$'s consistency?

I think the answer to (1) is "yes" because the same argument used by Smith for $$\mathsf{Con^\circ}$$ goes through for $$\mathsf{Con^\star}$$. The answer to (2) seems to be "yes" based on the rough argument I gave above. But together, this would imply the unlikely conclusion that $$\mathsf{PA}$$ simply proves its own consistency, without much room for quibbling about whether the purported consistency statement "counts." What am I missing?

• Why does the same argument that $PA\vdash \sf Con^\circ$go though for $\sf Con^*$? The argument he gives in the version I'm looking at (Thm 36.1) at is the same argument you give that $\sf Con^\circ$ is a trivial logical truth. Commented Feb 16 at 1:36
• @spaceisdarkgreen Ah, you're right. At first I misunderstood his proof as doing something else. So then, the answer to (1) is "no", presumably? Commented Feb 16 at 1:43
• Correct. As you remark, $\sf Con^*$ says there is no least proof of inconsistency, which is equivalent to there being no proof of inconsistency... and $\sf PA$ proves this equivalence because it can prove the least number principle. So it's equivalent to $\sf Con$ under $\sf PA$ so can't be proven in $\sf PA$ (unless $\sf PA$ is inconsisent). Commented Feb 16 at 1:45
• WillG if @spaceisdarkgreen does not wish to post the comment as an answer (which I totally understand, the lack of ability to manage what appears on one's userpage frequently stops me from posting answers), keep in mind that the rules do allow you to self-answer your question. It's better than leaving it in the unanswered queue. Commented Feb 16 at 7:45

To reiterate the comments, 2 is correct, but 1 is not. The author's argument that $$\sf PA\vdash Con^{\circ}$$ is essentially the same as your argument that $$\sf Con^{\circ}$$ is a trivial logical truth and doesn't transfer to $$\sf Con^\star.$$ And as you say, $$\sf Con^\star$$ expresses that there is no least proof of inconsistency, so this is provably equivalent to $$\sf Con$$ in $$\sf PA$$ as an instance of the least number principle.
So actually, the $$\le$$ (as opposed to $$<$$) is crucial. But for that matter, I'm not sure why the author doesn't just use the simpler definition $$\sf Prf^\circ(x,y) := Prf(x,y)\land \lnot Prf(x, \ulcorner \bot \urcorner).$$ Unless I'm missing something, one can show $$\emptyset \vdash \sf Con^\circ$$, and that $$\sf Prf^\circ$$ captures and expresses $$Prf$$ iff PA is consistent, etc. under this simpler definition by similar arguments.
• I think you mean $\emptyset \vdash \textsf{Con}^\circ$, toward the end? Commented Feb 17 at 5:47