Re: Godel's comments about the "true reason" for incompleteness

On Mar 30, 7:49 pm, "R. Srinivasan" <sradh...@xxxxxxxxxx> wrote:
On Mar 30, 4:11 pm, Aatu Koskensilta <aatu.koskensi...@xxxxxxxxx>
wrote:



On 2008-03-30, in sci.logic, R. Srinivasan wrote:

First of all let me clarify that the sentence I am considering is:

For each P (T0 |- Pv~P)            (4)

As per what AK has written, this sentence is legitimate in the
metatheory T of PA which formalizes the syntax of PA, and "for each
P.." in the above means "for each sentence P in the language of PA".
Further (4) can be translated into the language of PA and then proven
in PA. I am asserting that (4) is equivalent to the sentence

For each P (Pv~P)            (3)

And that if PA proves (4), then PA proves (3).

This is trivial since according to you (3) means exactly the same as
(4). On that understanding there's nothing problematic about PA
proving (3). It's another matter that (3) and (4) do not mean the same
thing, as we can see for example by noting that (3) is the sort of
stuff people went on about saying long before anyone knew anything
about formal derivations in first-order logic; and that (4) is a
mathematical result about first-order logic, a very trivial one but
one nevertheless, while (3) is a basic law of (classical) logic, of
which the justification is of quite different kind.

Of course PA *should* not prove (3), because that is the way we have
set up FOL and the metatheory T of PA in which we formulate (4) is
supposedly equivalent to PA.

It is obscure what you have in mind. Why shouldn't PA prove (3) if it
just means that "P or not-P" is logically provable for every P?

Because (3) would not be provable in PA without coding. Only each
instance of this sentence expressed as a schema is provable in PA. To
claim that the sentence itself is provable in PA only follows after
coding and amounts to adding to the strength of PA. Since the claim is
that the metatheory T (in which facts about syntax of PA are
expressed) is just as strong as PA, it should not allow the sentence
(3) to be encoded into the language of PA. So if we accept the
equivalence of truth and provability in the sense that I have in mind,
it appears to me that Godel's reasoning is not finitary.

The claim made by AK is that PA proves the encoded version of (4) (see
this post for the numbering). And that PA does not prove (3), which is
not even a legitimate sentence. Do you agree that (4) ought to be
equivalent to (3) if we grant that

For each P ((T0|-Pv~P) <-> Pv~P)  (5)

is unassailably true (via a proof in PA of each of its instances)?

No. After all, it's provable in PA that

 For each P( "P or not-P" is logically provable <--> 0 = 1)

I don't understand this. How is this sentence (in particular, the
forward implication) provable in PA, unless PA is inconsistent? Here I
am using the fact that the negation of

For each P (f(P) <-> Q)       (8)

is

For some P ( (f(P)&~Q) or (~f(P)&Q) )   (9)

where f(P) stands for  '"P or not-P" is logically provable' and Q
stands for '0=1'. Surely the first disjunct of (9) is provable in PA
and so (9), the negation of your original sentence (8),  is provable
in PA?



so it's difficult to see why the provability of (5) should tell us
anything about equivalence of (3) and (4). It is also somewhat
misleading to include "P or not-P" within (5) under the scope of the
quantifier "For each P". A more transparent formulation of (5) would
be (6):

 For every x(if x is the code of a sentence P in the language of PA,
 then the code of "P or not-P" is logically provable) <--> Q \/ not-Q

where Q is a sentence in the language of PA. On this formulation it is
perhaps more clear why it is a baffling suggestion we derive anything
from (5) about equivalence of (3) and (4).

If your (5) is not supposed to be equivalent to (6), and the
quantifier "For each P" is supposed to bind also the P in the latter
occurrence of "Pv~P" in (5) then (5) is not expressible in PA at
all.

It is possible you had in mind the schema (7)

 "P or not-P" is logically provable <--> P or not-P

the instances of which are all provable in PA, again for trivial
reasons. There's nothing in the provability of the instances of (7)
that would tell us anything about equivalence of (3) and (4) either.

This schema (7) is what I had in mind. The question is whether if PA
proves each instance of the schema (7) and if PA proves (4), does PA
prove (3)? This seems so to me, given the fact that we do not concede
the existence of non-standard models of PA in which (some instance of)
(7) can fail.

What I am trying to express here is that with no coding, the only
reason why PA doesn't prove (3) is that (3) is not a sentence in the
language of PA. And the reason (3) is not a sentence in the language
of PA is that PA cannot recognize something that is quantified over
sentences. In other words, PA cannot recognize that some sentence
expressed in terms of sentential variables (ranging over all
sentences) is provable. But the moment we admit (4) as a sentence that
is provable in PA (via coding), all that changes. Now the stated
reason for not admitting (3) as a legitimate sentence no longer holds
water. Because we have already seen via (4) that PA does prove
something expressed in terms of the variable P, which ranges over all
sentences. And the moment (3) is admitted as a legitimate sentence, it
must be provable (from (4) and (7)) unless we admit non-standard
models of PA in which some instance of the schema Pv~P fails (and is
therefore not provable in PA).

Regards, RS
.

Relevant Pages

  • Re: Question regarding incompleteness in formal systems without sufficient power for arithmetic.
    ... contingent or a self-contradiction iff the sentence is not provable. ... pure predicate calculus alone. ... Consider a particular first order language. ... No, 'contingent' does not refer to status per provability from axioms, ...
    (sci.logic)
  • Re: Godels comments about the "true reason" for incompleteness
    ... Further can be translated into the language of PA and then proven ... anything about equivalence of and. ... There's nothing in the provability of the instances of ... And the reason is not a sentence in the language ...
    (sci.logic)
  • Re: Godels comments about the "true reason" for incompleteness
    ... What language or theory is THAT sentence in? ... truth is model theoretic truth, you should have no difficulty in going ... set up FOL and the metatheory T of PA in which we formulate is ... equivalent to formal provability. ...
    (sci.logic)
  • Re: Godels comments about the "true reason" for incompleteness
    ... Further can be translated into the language of PA and then proven ... Because would not be provable in PA without coding. ... instance of this sentence expressed as a schema is provable in PA. ... equivalence of truth and provability in the sense that I have in mind, ...
    (sci.logic)
  • Re: Goedel - interesting problem?
    ... If its provably false then assume the antithesis that it is true ... membership in the deductive closure of T, i.e. provability from T. ... Pi_1 statements, we would have T |/- G, which contradicts the assumption ... formulas in the language of T are provable in T simply contradicts the ...
    (sci.logic)