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