Re: Simple yet Profound Metatheorem

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.)
But isn't true=true and false=false and ~(true=false)?

> 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 ) ?

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

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!* I still have faith in the
original theorem (above.)

( P = |- Q) => ( P = |-P) because P must be 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.")

C-B

(I'll be glad to provide further details if anyone is interested.)

* However, what is wrong with:

Thm. ( |- (P=Q) ) =>((|- 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

Thm. ((|- P) = (|- Q)) => |- (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

.