```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 doableGeorge 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 PREDICATEDERIVES(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)- - - - - - - - - - - - - -
```