Re: Simple yet Profound Metatheorem

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'."

Obviously false, since if P equals 'Q has a proof'
then P does not equal Q. So that must not be what you mean.

>(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.

>C-B
>
>Hint: Consider the equivalent ( P = |-Q ) => ( P = |- P )


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

David C. Ullrich
.