Date: Nov 18, 2012 3:46 AM
Author: Graham Cooper
Subject: Re: A HARD FLAW in Godel's Proof
On Nov 18, 4:14 pm, George Greene <gree...@email.unc.edu> wrote:

> On Nov 17, 10:10 pm, "INFINITY POWER" <infin...@limited.com> wrote:

>

> > STEP 1: DEFINE a 2 parameter predicate DERIVE(THEOREM, DERIVATION)

>

> > DERIVE(T,D) is TRUE IFF

> > D contains a sequence of inference rules and substitutions

> > and the final formula T in D is logically implied from the Axioms.

>

> This is NOT even what you MEANT to say.

> The WHOLE QUESTION is <<not>> whether T is or isn't logically implied by the

> axioms.

> That is HARD. What is a SMALLER question and therefore

> EASY enough to make this doable

George I like your thinking here!

> is whether

> "the final formula T in D" is or isn't logically implied *BY*D*, by

> *THIS* derivation,

> by THIS sequence of inferences D. Even IF THIS chain of reasoning D

> is WRONG, it could STILL be the case

> that T followed frOM THE AXIOMS, by A DIFFERENT sequence of inferences

> (different from D).

> Checking whether the final formula in the sequence is correctly

> derived BY THAT SEQUENCE

> is easy. Checking whether there does or doesn't exist ANY old

> sequence-of-derived-inferences

> starting at some axioms and finishing with T is HARD, partly because

> the shortest such sequence might be

> MUCH MUCH longer than T.

>

OK so the T/F PREDICATE

DERIVES(T,<t1, t2, t3, t4,,,,T>)

is easy to program!

...As long as D is a given argument, for now.

STEP 2!

- - - - - - - - - - - - - -

STEP 2: DEFINE a Godel Statement.

i.e. Godel Statement named G =

ALL(M) ~DERIVE(G,M)

- - - - - - - - - - - - - -