Re: A HARD FLAW in Godel's Proof

[Graham Cooper]

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

[Graham Cooper]

On Nov 19, 1:14 am, forbisga...@gmail.com wrote:

> On Sunday, November 18, 2012 12:46:17 AM UTC-8, Graham Cooper 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

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

> And always,
>


D is a finite length string, all the terms in D are from a fixed
alphabet or atleast countable.

The HYPOTHESIS which goes against "G=!proof(G)" being significant

is that:

for some suitably rich set of Axioms,
for every well formed formula F
exist <t1,t2,t3,,,,F>
or exist <t1 t2 t3,,,~F>

which would imply the existence of a halting thoerem decider.

Though it's complexity might be exponential anyway.

Herc

[Graham Cooper]

On Nov 18, 6:46 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> 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)
> - - - - - - - - - - - - - -
>

Thanks for bumping this thread, this ties together some high level
consistency theory with my current forward chaining Modus Ponens
Provers!

The PROOF is just an extra argument of MODUS PONENS listing the
inferences used so far!

how would you decide if the FORMULA
was a THEOREM of those AXIOMS?

AXIOM --> THM ---> THM ---> THM ---> FORMULA?


***************************************

A SIMPLY WAY TO [LIST] A THEORY!

***************************************

t(NEW,l(L)) :- trif(AXIOM,NEW,L), t(AXIOM,1).

TRANSITIVE IF
trif( OLD , NEW , l(L) ) :- if( OLD , NEW ).
trif( OLD , NEW , l(L) ) :- if( OLD , MID ) , trif( MID, NEW , L ).

NOW we can ask PROLOG what are all the THEOREMS?

..............................

?- t( THM , LVL ). <<<<<<< LIST THEORY!

THM= 1
LVL= 1

THM= 2
LVL= 1
* 1 and 2 are THEOREMS *

THM= if(1,3)
LVL=1

THM= if(3,4)
LVL=1

THM= if( and(2,4), 5)
LVL = 1

THM = if(5,6)
LVL = 1

THM= if(4,7)
LVL = 1

THM= if( and(6,7), 8)
LVL = 1

THM= if(8,9)
LVL = 1

THM= 3
LVL = l(l(_))
* 3 is a LEVEL 2 THEOREM *

THM= 4
LVL = l(l(l(_)))

THM=7
LVL = l(l(l(l(_))))




Herc