|
|
Re: A HARD FLAW in Godel's Proof
Posted:
Nov 18, 2012 3:46 AM
|
|
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)
- - - - - - - - - - - - - -
|
|
