
Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
Posted:
Oct 13, 2012 8:20 PM


On Oct 14, 10:06 am, George Greene <gree...@email.unc.edu> wrote: > On Oct 13, 4:30 pm, Graham Cooper <grahamcoop...@gmail.com> wrote: > > > These are just INFERENCES mind you. > > > You still owe me some BASE THEOREMS, otherwise all your "proofs" are > > Oracular. > > NO, I DON'T. > > In the NONlogical context, in the SET THEORY or NUMBER THEORY (Peano > Arithmetic) > or group theory OR ANY OTHER AXIOMATIC THEORY context, in the context > of anything > for which you might actually be USING firstorder logic, any > investigation TO WHICH you might > be APPLYING firstorder logic, what YOU are calling a "base theorem" > is called AN AXIOM. > That's what axioms ARE FOR. They are true DESPITE not having any > proofs (other than "it's an axiom".) > > In the purelogical context, there is no difference between a logical > axiom and the conclusion of an inference > rule that infers/derives that conclusion FROM AN EMPTY set of > premises. > I'm NOT being ORACULAR when I insist that P V ~ P > is true, withOUT any proof in a FIRSTorder system. P V ~P > *is*ZEROth*order, to start with. > Firstorder PRESUMES all that IN ONE handwave!
George, I don't care!
*I* use MODUS PONENS for inference and ANY OLE AXIOM and ANY THEOREM SO FAR.
a & (a>b) > b
*I* use double arrow > for NEW THEOREM
If you want to use a list of inferences distinct from axioms, may I suggest
(P ^ Q) > Q
so we know it's not a THEOREM/AXIOM
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.
*************
In MY TERMINOLOGY, since you use "model" to mean "deduction sequence" is meaningless.
A MODEL is CREATED in the theory like so:
a & (a >[p>q]) > [p>q]
NOW you have a 2ND LEVEL OF INFERENCE RULES [p>q]
You could JUST USE MODUS PONENS TO DO THIS and a set of tautology formula
but you like to have a list
1 P > P 2 !P > !P ...
which forces the prover into a single model.
Herc

