Simple yet Profound Metatheorem

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

C-B

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

.