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.