Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?
From: Charlie-Boo on 14 Dec 2005 21:10
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 )

From: William Elliot on 14 Dec 2005 22:36
On Wed, 14 Dec 2005, Charlie-Boo wrote:

> Prove ( P = |- Q ) => |- ( P = Q )
>
As you are mixing the object language with the meta language
your statement as presented is non-sense gibberish.

> (P and Q have the same sets of free variables.)
>
> Hint: Consider the equivalent ( P = |-Q ) => ( P = |- P )
>
All gibberish is equivalent to all other gibberish except some
gibberish is more equivalently certified and guaranteed non-sense.
From: Charlie-Boo on 15 Dec 2005 03:45

William Elliot wrote:
> On Wed, 14 Dec 2005, Charlie-Boo wrote:
>
> > Prove ( P = |- Q ) => |- ( P = Q )
> >
> As you are mixing the object language with the meta language
> your statement as presented is non-sense gibberish.

Don't you think that provability is expressible within the Logic?

C-B

> > (P and Q have the same sets of free variables.)
> >
> > Hint: Consider the equivalent ( P = |-Q ) => ( P = |- P )
> >
> All gibberish is equivalent to all other gibberish except some
> gibberish is more equivalently certified and guaranteed non-sense.

From: William Elliot on 15 Dec 2005 03:55
On Thu, 15 Dec 2005, Charlie-Boo wrote:
> William Elliot wrote:
> > On Wed, 14 Dec 2005, Charlie-Boo wrote:
> >
> > > Prove ( P = |- Q ) => |- ( P = Q )
> > >
> > As you are mixing the object language with the meta language
> > your statement as presented is non-sense gibberish.
>
> Don't you think that provability is expressible within the Logic?
>
Do it. But before you do it, explain what your object language is.
From: Charlie-Boo on 15 Dec 2005 05:07
William Elliot wrote:
> On Thu, 15 Dec 2005, Charlie-Boo wrote:
> > William Elliot wrote:
> > > On Wed, 14 Dec 2005, Charlie-Boo wrote:
> > >
> > > > Prove ( P = |- Q ) => |- ( P = Q )
> > > >
> > > As you are mixing the object language with the meta language
> > > your statement as presented is non-sense gibberish.
> >
> > Don't you think that provability is expressible within the Logic?
> >
> Do it. But before you do it, explain what your object language is.

Something as fundamental as the above theorem is certainly valid in
more than one Logic. Like any good metamathematical theorem, we give
the least limiting requirements for our conclusions to hold (cf the
Godel/Rosser competition.) We instead allow whatever Logics through
which our argument can be carried. (I'm not saying that the proof
has to be formal or representable in the Logic, although of course
that's always nice. The formality begins after the above is proven.
The theorems of informal proofs are the axioms of formal proofs.
Uninspired axioms are NOT inevitable.)

C-B

"I had all of the problems of science analyzed and solved - until I
awoken only to discover it was but the ranting of a madman."
12-22-05

 |  Next  |  Last
Pages: 1 2 3 4 5 6 7 8 9 10 11
Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?