
Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
Posted:
Oct 14, 2012 9:05 PM


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.
MP
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.
I use
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?!?
Herc

