Search All of the Math Forum:

Views expressed in these public forums are not endorsed by NCTM or The Math Forum.

Notice: We are no longer accepting new posts, but the forums will continue to be readable.

Topic: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
Replies: 39   Last Post: Oct 14, 2012 11:56 PM

 Messages: [ Previous | Next ]
 Graham Cooper Posts: 4,495 Registered: 5/20/10
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

Date Subject Author
10/5/12 Graham Cooper
10/5/12 Frederick Williams
10/7/12 Charlie-Boo
10/5/12 Graham Cooper
10/5/12 Frederick Williams
10/5/12 Graham Cooper
10/7/12 Graham Cooper
10/8/12 Graham Cooper
10/9/12 Graham Cooper
10/11/12 Graham Cooper
10/12/12 Graham Cooper
10/12/12 Graham Cooper
10/12/12 camgirls@hush.com
10/12/12 Richard Tobin
10/12/12 camgirls@hush.com
10/13/12 george
10/13/12 Graham Cooper
10/14/12 george
10/13/12 Graham Cooper
10/13/12 george
10/13/12 george
10/13/12 Graham Cooper
10/14/12 Graham Cooper
10/14/12 Graham Cooper
10/14/12 Graham Cooper
10/5/12 Scott Berg
10/5/12 Curt Welch
10/6/12 Mike Terry
10/6/12 Graham Cooper