Re: A question on GIT.

andrevh_at_sci.kun.nl
Date: 09/07/04 

Date: Tue, 7 Sep 2004 18:53:07 +0000 (UTC)

>
> Re: A question on GIT.
>
> From: "Tim Peters" <tim.one@comcast.net>
> Reply to: [1]"Tim Peters"
> Date: Mon, 6 Sep 2004 18:15:44 -0400
> Newsgroups:
> [2]sci.logic
> Followup to: [3]newsgroup
> References:
> [4]<Ff3%c.330129$gE.89429@pd7tw3no>
>[namducnguyen]
>> In a meta level, a formula F is undecidable iff:
>>
>> (1) F is true in one model => F is false in another model
>>
>> Now, typically when one tries to prove F is an undecidable, one would try
>> to show:
>>
>> (2a) there is a *found* model in which F is true,
>> (2b) there is another found model in which F is false.
>>
>> With respect to G(PA), and given (1), (2a), (2b), a couple question
>> arise:
>>
>> Did Godel *hypothetically assume* G(PA) is true in one model, say the
>> standard model, and proceed to show that based on this assumption, G
>> could be shown to be false in a different model? [This kind of proof
>> reflects the _hypothetical_ spirit of (1): no actual model is required]
>>
>> Or did Godel in fact show beyond doubt that G(PA) is true in the standard
>> model, and false in a non-standard model? [This proof is based on the
>> spirit of (2)'s: models must be found.]
>>
>> The motivation for my asking these 2 question is I don't know how Godel
>> came about to know that G(PA) is true in the standard model. I mean in
>> either method, (1) or (2a-b), the conclusion of GIT is the same. But it
>> seems to make a difference, in some sense, whether Godel did know G(PA)
>> is true in the standard model, or didn't know and couldn't know- and
>> only hypothetically assumed so, in order to proceed in the manner of (1).
>>
>> Thanks for any hint/comment on this.
>
>I'd say "none of the above". GIT wasn't really a model-theoretic proof.
>The sentence G is, informally,
>
> For all integer N, N does not encode a proof of sentence G.
>
>Assume the system is consistent and sound.
>
>Assume G is provable. Then (soundness) it's also true: no N encodes G's
>proof. But if no N encodes G's proof, then G is not provable in the system.
>That's a contradiction, so the assumption that G is provable must be wrong.
>But "G isn't provable" is what G "says" (at the meta level), so G is in fact
>true. That's how Godel knew G was true, but the truth of G plays no role in
>the proof.
>

There is something I don't understand here. According to me, the following
statement (G) is FALSE:

   G: G is undecidable

G is not undecidable, G is decidable: G is false. So "I know G is false".
Where am I going wrong?

Relevant Pages

  • Re: A question on GIT.
    ... > The motivation for my asking these 2 question is I don't know how Godel ... > came about to know that Gis true in the standard model. ... But "G isn't provable" is what G "says" (at the meta level), ... omega consistency if you add -G, and, IIRC, omega consistency was introduced ...
    (sci.logic)
  • A question on GIT.
    ... a formula F is undecidable iff: ... reflects the _hypothetical_ spirit of: ... Or did Godel in fact show beyond doubt that Gis true in the standard ... came about to know that Gis true in the standard model. ...
    (sci.logic)