Prev: Obections to Cantor's Theory (Wikipedia article)
Next: Why Has None of Computer Science been Formalized?
From: William Elliot on 15 Dec 2005 06:00
On Thu, 15 Dec 2005, Charlie-Boo wrote:

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

Indeed, they're called not well formed formulas.



From: Dan Christensen on 14 Dec 2005 22:32
"Charlie-Boo" <chvol(a)aol.com> wrote in message
news:1134612658.814742.58980(a)f14g2000cwb.googlegroups.com...
> Prove ( P = |- Q ) => |- ( P = Q )
>

What does this mean? I am not familiar with the notation.

Dan


> (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: David C. Ullrich on 15 Dec 2005 08:34
On 14 Dec 2005 18:10:58 -0800, "Charlie-Boo" <chvol(a)aol.com> 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
From: Charlie-Boo on 15 Dec 2005 14:14
William Elliot wrote:
> On Thu, 15 Dec 2005, Charlie-Boo wrote:
>
> > 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.
>
> Indeed, they're called not well formed formulas.

Not to be flippant, but which characters of the expression are not
well-formed? Is ( P = |-Q ) a wff? Is => an operator? etc.

C-B

From: Charlie-Boo on 15 Dec 2005 15:02
Dan Christensen wrote:
> "Charlie-Boo" <chvol(a)aol.com> wrote in message

> > Prove ( P = |- Q ) => |- ( P = Q )

> What does this mean? I am not familiar with the notation.
>
> Dan

P and Q are variables that range over wffs
|- means "It is provable that"
= is logical equivalence
=> is implication

Check out any text on Logic, especially Modal Logic e.g. The
Unprovability of Consistency, or The Logic of Provability by Boolos.

C-B

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

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