On Oct 15, 1:01 am, George Greene <gree...@email.unc.edu> wrote: > > a & (a->b) --> b > > > *I* use double arrow --> for NEW THEOREM > > > > The only lesson here is that there is SOME / ONE rule that operates ON > > the theory by creating --> new formula which is distinct from the > > theorems. > > You prove a theorem by inferring/deriving it FROM THE AXIOMS, USING > the inference rules! > But the axioms ARE NOT *logical* axioms! > Anything YOU might want TO CALL a "logical axiom" would BE BETTER > thought of as an inference rule! > And there is NO reason for you to limit yourself to ONE of them! > You CAN do that, but it requires EFFORT AND TRANSLATION, which is not > normally going to be considered natural! > Natural treatments do NOT normally confine themselves to --> (MP) or V > (resolution) as their only connective!
No it's really quite simple and 20 years ago was the defacto standard in theorem provers.
LHS & (LHS->RHS) --> RHS
where --> *ADDS* A NEW THEOREM
where LHS->RHS is any THEOREM with an outermost implication.
IF you make a OBJECT LANGUAGE with a big list of
LHS --> RHS LHS --> RHS ..
that's really neat but it's going to miss any derived inference rules.
LHS & (LHS -> (a&b->c)) -> a&b->c
to derive models of backward chainable embedded theories that are recursively provable back to the axioms!
but you are stuck on
ALL(x) x is a set with FOL language in WFF this and object that so where does !E(x) go?!?