In a very accessible form one could state the first incompleteness as follows:
Incompleteness Theorem I
Assume that $\textbf{PA}$ is consistent. Then there is a sentence $\phi$ such that
- $\textbf{PA}\nvdash \phi$ and
- if $\textbf{PA}\vdash\textsf{Pr}_{\textbf{PA}}(\overline{\phi}) \Rightarrow \textbf{PA}\vdash\phi$, then $\textbf{PA}\nvdash\neg\phi$,
where $\textsf{Pr}_{\textbf{PA}}(y)$ is the "is provable in $\textbf{PA}$" predicate, i.e. $\exists x . \textsf{Prov}_{\textbf{PA}}(x,y)$.
$\omega$-consistence
My question is about the relation between the assumption given in 2. and the $\omega$-consistence of $\mathbf{PA}$, since one can state Gödel I like above but with the $\omega$-consistence as assumption instead.
The definition I know is the following:
There is no formula $\phi(x)$ such that $\mathbf{PA}\vdash\exists x.\phi(x)$ and simultaneously that we have for every $n$: $\mathbf{PA}\vdash \neg\phi(\overline{n})$.
I've tried a few times, always running into the syntactic negation of the assumption. At least I would like to know if it is equivalent at all!?
Thanks!
The assumption in 2. indeed follows from $\omega$-consistency: Consider the formula $\textsf{Pr}_{\textbf{PA}}(x,\overline{\phi})$ in the free variable $x$ expressing that $x$ codes a proof of $\phi$. If $\textbf{PA}\vdash \textsf{Pr}_{\textbf{PA}}(\overline{\phi})$, then $\textbf{PA}\vdash \exists x. \textsf{Pr}_{\textbf{PA}}(x,\overline{\phi})$, so $\omega$-consistency implies the existence of some $n$ such that $\textbf{PA}\not\vdash\neg\textsf{Pr}_{\textbf{PA}}(n,\overline{\phi})$, so $\textbf{PA}\vdash\textsf{Pr}_{\textbf{PA}}(n,\overline{\phi})$ by the soundness of the coding $\textsf{Pr}_{\textbf{PA}}$. Now, in the meta theory you can decode this $n$ and check whether it is indeed a proof of $\phi$ in $\textbf{PA}$ - if it is, fine, and if it is not, the soundness of the coding would also give $\textbf{PA}\vdash \neg\textsf{Pr}_{\textbf{PA}}(n,\overline{\phi})$, hence an inconsistency.