Re: Simple yet Profound Metatheorem

On 15 Dec 2005 12:16:35 -0800, "Charlie-Boo" <chvol@xxxxxxx> wrote:

>David C. Ullrich wrote:
>> On 14 Dec 2005 18:10:58 -0800, "Charlie-Boo" <chvol@xxxxxxx> wrote:
>
>> >Prove ( P = |- Q ) => |- ( P = Q )
>>
>> Various people have asked what the heck this means.
>> You should _say_ what it means, instead of replying
>> with questions.
>
>[...]
>
>> Hint: My best attempt at deciphering it leads to
>> something obviously false:
>>
>> "If P equals 'Q has a proof' then there is a
>> proof of 'P equals Q'."
>
>That's it. What was so hard about that?

Very curious - a minute ago I saw you say that it
meant something else.

>> Obviously false, since if P equals 'Q has a proof'
>> then P does not equal Q.
>
>Why is that false? (Once again, what you are so adamantly convinced of
>is just not so.)

If this is not clearly false you must be assuming that I'm
being as sloppy with the language as you are. I'm not -
when I say "equals" I mean "equals", not "is logically
equivalent to". For example, P is not equal to P&P,
although they're certainly equivalent.

Evidently from what you say elsewhere in the thread
what you really mean, and what you thought I meant,
is this:

"If P is equivalent to 'Q has a proof' then there is a
proof of 'P is equivalent to Q'."

This is also false, as has been pointed out, although
it's not quite so _obviously_ false as my first interpretation,
where I was assuming that "=" referred to equality.

Why is it false? Consider the special case where P literally
equals "Q is provable". Then your theorem implies this,
for any Q:

(*) "It is provable that 'Q is provable' is equivalent to Q."

Or, in extremely bad notation:

(*) |- (|-Q == Q)

(bad notation because the first |- means |-, while
the second |- refers to some encoding of provability...)

This is false. It contradicts the incompleteness theorem,
for example, which says that in any system satisfying this
and that there exists Q which is true but not provable.

>> So that must not be what you mean.
>
>Thanks for the vote of confidence.
>
>> >(P and Q have the same sets of free variables.) This simple theorem (I
>> >created 12/1/05) provides the link between Theory of Computation and
>> >Proof Theory (Incompleteness in Logic) that theoreticians such as
>> >myself have been looking for since the 1930's. (Each Theory of
>> >Computation theorem becomes an Incompleteness theorem in Logic,
>> >providing almost trivial formal derivation of the exact results of
>> >Godel, Rosser and Smullyan.)
>>
>> Awesome.
>
>Would it be awesome (interesting, new, useful) if it were true?
>
>C-B
>
>> >Hint: Consider the equivalent ( P = |-Q ) => ( P = |- P )
>>
>>
>> ************************
>>
>> David C. Ullrich


************************

David C. Ullrich
.

Relevant Pages

  • Re: why does dz = dx + dyi in complex analysis
    ... int f dz = int f dx + i int f dy ... equals a small change in x + i * a small change in y. ... David C. Ullrich ...
    (sci.math)
  • Re: Peanos space-filling curve
    ... I've replied to four posts in one to save space and time. ... David C. Ullrich wrote in message ... I have difficulty with 'separate' applied to ordered reals. ...
    (sci.fractals)
  • Re: Peanos space-filling curve
    ... I've replied to four posts in one to save space and time. ... David C. Ullrich wrote in message ... I have difficulty with 'separate' applied to ordered reals. ...
    (sci.math)
  • Re: Some Simple Questions
    ... stupid as the original version. ... >providing evidence that it is not true. ... >> David C. Ullrich ...
    (sci.math)
  • Re: Some Simple Questions
    ... That's an utterly stupid question. ... >that the system can in fact produce X, they are suggesting that the ... >> David C. Ullrich ...
    (sci.logic)