Re: Simple yet Profound Metatheorem

On 16 Dec 2005 11:07:53 -0800, "Charlie-Boo" <chvol@xxxxxxx> wrote:

>David C. Ullrich wrote:
>
>> 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.
>
>Show me how to underline = in a post and I'll be glad to (seriously.)

All you have to do is explain what your notation means.

Also probably when I have a conjecture about what you
mean by the notation and it's _not_ what you actually
meant saying yes it is is probably not a good idea.

But never mind that - your "=" meant logical equivalence,
fine (if you insist).

>But isn't true=true and false=false and ~(true=false)?

I have no idea, because the fact that you insist on
using "=" to denote something other than equality
means that I have no idea what you're asking.

>> Or, in extremely bad notation: |- (|-Q == Q)
>>
>> (bad notation because the first |- means |-, while
>> the second |- refers to some encoding of provability...)
>
>And [] ( []Q == Q ) ?

What about it? (Is it extemely bad notation? No.
Does it mean the same thing as |-(|- Q == Q)? No.
Is it a theorem of any system of modal logic
known to man? No. If your question is not answered
above, what _did_ you mean to ask?)

>> >> >(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?
>
>Too hard of a question?

Right. The question is equivalent to "Would it be awesome if
2 + 2 = 5?" That is indeed a very difficult question.

>What I really need is the "hint" ( P = |- Q) => ( P = |-P ) to
>effect the translation from Theory of Computation theorems to
>Incompleteness in Logic theorems. (And since I axiomatize Theory of
>Computation theorems in http://arxiv.org/html/cs.LO/0003071 , that
>paper plus this theorem provides an axiomatization of Incompleteness in
>Logic results, including the theorems of Godel, Rosser, Smullyan and
>others.)
>
>Since P = |- Q then (P = |- P) means (|- P) = (|- Q). I thought that
>maybe (|- P) = (|- Q) is equivalent to |- (P=Q) and added it to spice
>up the theorem as ( P = |-Q ) => |- (P=Q), but Barbara Knox (and you)
>posted a very nice proof to the contrary!*

Poor Charlie. You announce that you've _proved_ a "simple yet
profound" metatheorem. Turns out that part of the "proof" was
just something you "thought" was so. And you wonder why nobody
takes you seriously.

>I still have faith in the
>original theorem (above.)

What is the "original theorem"? There are many things "above".

>( P = |- Q) => ( P = |-P) because P must be r.e.

Uh, this is gibberish. A set of natural numbers is or is not
r.e. What the hell does it mean to say that a wff is r.e.?

>I just spent a few
>minutes thinking about it in terms of pure Logic (Modal Logic,
>actually), and came up with:
>
> Thm. ( P = |- Q) => ( P = |-P)
>1. P = |-Q Premise
>2. |-P = |-|-Q ( w = v ) => ( (|-w) = (|-v) ) , 1
>3. |-P = |-Q ( |-w ) = ( |- |- w) , 2
>4. P = |-P Substitution 1,3
> qed
>
>Now do you agree? (Just cut out the red herrings about syntax. Or
>admit "I don't know anything about Logic but I know what the symbols
>are.")

"red herrings about syntax". Right.

First, that doesn't have anything to do with modal
logic that I can see. Second, I can't parse most
of it, because of your idiosyncratic notation
(I can't tell which |-'s are actually assertions
and which are abbreviations for an encoding of
provability.)

>C-B
>
>(I'll be glad to provide further details if anyone is interested.)
>
>* However, what is wrong with:
>
> Thm. ( |- (P=Q) ) =>((|- P) = (|- Q))

If my guess regarding what you mean is correct then
this is a true fact, not that the "derivation"
below makes much sense.

>1. |- (P=Q) Premise
>2. |- (P => Q) Definition 1
>3. |- (Q => P) Commutativity and Definition 1
>4. (|-P) => (|-Q) Deduction Theorem 2
>5. (|-Q) => (|-P) Deduction Theorem 3
>6. (|-P) = (|-Q) Definition 4,5
> qed
>
> Thm. ((|- P) = (|- Q)) => |- (P=Q)

This on the other hand is obviously false.
It's 75 percent true: If P is provable and
Q is provable (so that ((|- P) == (|- Q)) is
true) then P==Q is certainly provable.
And if P is provable and Q is not provable
(so that ((|- P) = (|- Q)) is false) then
P == Q is certainly not provable; similarly
if Q is provable and P is not.

But if neither P nor Q is provable (so that
((|- P) = (|- Q)) is true) it certainly
does not follow that P==Q _is_ provable.

(For example, suppose P and Q are both atomic
formulas in the predicate calculus: P = p
and Q = q, where _those_ equal signs denote
_equality_. Then P is not provable, Q is not
provable, and neither is P == Q.)

>1. ((|- P) = (|- Q)) Premise
>2. (|- P) => (|-Q) Definition 1
>3. (|-Q) => (|-P) Commutativity and Definition 1
>4. |- (P=>Q) Deduction Theorem 2
>5. |- (Q=>P) Deduction Theorem 3
>6. |- (P=Q) Definition 4,5
> qed
>
>Thus ( |- (P=Q) ) <=> ( (|- P) = (|- Q) ), no?
>
>> David C. Ullrich


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

David C. Ullrich
.