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:
- Am I correct that $\mathsf{PA \vdash Con^\star}$?
- 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?
Best Answer
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.