4
$\begingroup$

Wikipedia and other sources claim that

$PA +\neg G_{PA}$

can be consistent, where $\neg G_{PA}$ is the Gödel statement for PA.

So what is the error in my reasoning?

$G_{PA}$ = "$G_{PA}$ is unprovable in PA"

$\neg G_{PA} $

$\implies$ $\neg$ "$G_{PA}$ is unprovable in PA"

$\implies$ "$G_{PA}$ is provable in PA"

$\implies$ $G_{PA}$

I would also appreciate it if someone could provide a somewhat intuitive explanation.

Sources:

  1. Non-standard model of arithmetic on Wikipedia
  2. Rosser's trick on Wikipedia
  3. Understanding Gödel's Incompleteness Theorem
  4. Is the negation of the Gödel sentence always unprovable too?
$\endgroup$

3 Answers 3

Reset to default
5
$\begingroup$

The point is that $G_{PA}$ is neither provable nor refutable in $\sf PA$. But it is a concrete sentence, and in a given model of $\sf PA$ it has a concrete truth value.

But if in all models $\sf PA$ it would have the same truth value, then the completeness theorem tells us that it is provable from $\sf PA$. Therefore there has to be some models where $G_{PA}$ is true and others where it is false; in particular both options are consistent with $\sf PA$.

In your suggested reasoning you forget that, for example, $\sf PA+\lnot\operatorname{Con}(PA)$ is also consistent. There are models of $\sf PA$ that "think" that $\sf PA$ is not consistent, therefore can prove anything.

Those models are non-standard models, and the non-standard numbers introduce new lengths of formulas and proofs, new rules of inference, and new axioms to $\sf PA$. Because internally, $\sf PA$ (and rules of logic, etc.) are all just recursive predicates to be interpreted in some way.

The point here is that all the things we do with Godel numbering (represent logic and theories using integers) are just "definable predicates", and the sentence $G_{PA}$ is really just saying the following thing:

Using the way described in $\varphi_1$ to understand numbers as formulas, and with the inference rules described by the formula $\varphi_2$ and the formula $\varphi_3$ describing the theory $\sf PA$, then if this theory as understood with all these rules is consistent, then there is no proof of this very sentence.

But in non-standard models all these formulas will necessarily define sets which include non-standard integers (if only because they define unbounded sets in the standard model). So a non-standard model can have more inference rules, more proofs, more cowbell, and definitely more axioms to $\sf PA$. And there lies the contradiction from which we can show that every statement has a "code for a proof" (which may be of non-standard length, and it might be using non-standard formulas, and non-standard inference rules).

$\endgroup$
3
  • $\begingroup$ Thanks for your answer, but what is the error in my reasoning? I would like to know so I can develop correct mathematical reasoning skills. $\endgroup$
    – ignoramus
    Commented Mar 14, 2015 at 8:32
  • $\begingroup$ I've tried to add a bit on that. Is this more helpful? $\endgroup$
    – Asaf Karagila ♦
    Commented Mar 14, 2015 at 8:35
  • $\begingroup$ After reading over it a few times, I still can't understand your answer. I guess there isn't a simple explanation for why my reasoning doesn't work. $\endgroup$
    – ignoramus
    Commented Mar 14, 2015 at 9:11
5
$\begingroup$

The last step is the problematic one: You are given a formula $\varphi$ and try to prove, in the (finitistic!) metatheory, that $\textsf{PA}\vdash "\textsf{PA}\vdash\varphi"$ implies $\textsf{PA}\vdash\varphi$. While the implication "$\Leftarrow$" is fine (a proof of $\varphi$ from $\textsf{PA}$ could be explicitly coded, giving a proof of $"\textsf{PA}\vdash\varphi"$ in $\textsf{PA}$, too) the implication "$\Rightarrow$" needs the $\omega$-consistency of $\textsf{PA}$: It might happen that, even though we have $\textsf{PA}$ proving $\exists n: "n\text{ codes a proof of }\varphi"$, for every 'actual' natural number $\textbf{n}$ we have $\textsf{PA}\vdash "\textbf{n}\text{ does not code a proof of }\varphi$". This is what Asaf alluded to model theoretically.

$\endgroup$
12
  • $\begingroup$ Are you referring to this implication ¬ "GPA is unprovable in PA" ⟹ "GPA is provable in PA" ? $\endgroup$
    – ignoramus
    Commented Mar 14, 2015 at 9:23
  • 1
    $\begingroup$ @ignoramus: No, I mean deducing the provability of $G_{\textsf{PA}}$ from the provability of $"G_{\textsf{PA}} \text{is provable}"$ - your last step. $\endgroup$
    – Hanno
    Commented Mar 14, 2015 at 9:25
  • 2
    $\begingroup$ Hanno, I think the OP was saying that if there is a model where $G_{PA}$ is false, then we can conclude such and such. The reason this is not a contradiction is because the statement is about internal provability, and internal consistency. These distinctions are tricky and they take some time getting used to. $\endgroup$
    – Asaf Karagila ♦
    Commented Mar 14, 2015 at 9:29
  • $\begingroup$ @Hanno Thanks, the idea that PA⊢"PA⊢φ" implies PA⊢φ is not necessarily true is very counter-intuitive to me. I'm still reading over your answer and trying to understand it. $\endgroup$
    – ignoramus
    Commented Mar 14, 2015 at 9:29
  • 1
    $\begingroup$ @Hanno: It's fine to think about formalization, but the first sentence is foremost about what "we" can deduce, and we can certainly deduce that if PA proves something then it is true. The intended meaning is not about a formal system, it's about what we can deduce as mathematicians. For a formalization, the only challenging thing is deciding how to formalize "true". E.g. if we let $T$ be ZFC and say that a sentence $\phi$ of PA is "true" if $\omega \vDash \phi$, then ZFC proves $\text{Pvbl}_{\text{PA}}(\phi) \to \omega \vDash \phi$ for $\phi \in L(\text{PA})$. So that is one formalization. $\endgroup$
    – Carl Mummert
    Commented Mar 16, 2015 at 11:50
4
$\begingroup$

Long comment, regarding the "deductive flaw" in your argument.

We have that Gödel's First Incompleteness Theorem needs the Gödel's sentence $G_{\mathsf {PA}}$ such that :

$\mathsf {PA} \vdash G_{\mathsf {PA}} ↔ ¬Prov_{\mathsf {PA}}(\ulcorner G_{\mathsf {PA}} \urcorner)$.

Now your proof is :

1) $\lnot G_{\mathsf {PA}}$ --- assumed,

which means, as you say : "not $G_{\mathsf {PA}}$ is unprovable in $\mathsf {PA}$"

2) $Prov_{\mathsf {PA}}(\ulcorner G_{\mathsf {PA}} \urcorner)$ --- by the above equivalence and double negation,

which means, as you say : "$G_{\mathsf {PA}}$ is provable in $\mathsf {PA}$".

But 2), as you can easily check, is not $G_{\mathsf {PA}}$, so you cannot conclude it only by the above equivalence.

As per Hanno's answer, the "move" from : $Prov_{\mathsf {PA}}(\ulcorner S \urcorner)$ to $S$ needs some "additional resource", like the so-called Reflection Principle :

(Ref) $ \ \ Prov_{\mathsf {PA}}(\ulcorner S \urcorner) → S$

which asserts a sort of soundeness of the system (a stronger property than consistency).

In a nutshell, we cannot simply "equate" the intuitive concepts of provable and true.

The gist of Gödel's (and Traski's) Theorems is that if we work with the "formal counterparts" of the two concepts (like provable in a (formal) theory $\mathsf T$) we have to ackowledge that the two are not equivalent.

$\endgroup$
2
  • 2
    $\begingroup$ It is worth pointing out that, by Löb's theorem, that the only time PA is able to show $\text{Pvbl}(S) \to S$ for a sentence $S$ is when $S$ is already probable in PA. So no nontrivial instance of reflection is provable in PA. en.wikipedia.org/wiki/L%C3%B6b%27s_theorem $\endgroup$
    – Carl Mummert
    Commented Mar 15, 2015 at 12:29
  • $\begingroup$ @Carl Mummert: Interesting, thanks! $\endgroup$
    – Hanno
    Commented Mar 16, 2015 at 9:54

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .