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