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 NON-logical 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 first-order logic, any > investigation TO WHICH you might > be APPLYING first-order 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 pure-logical 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 FIRST-order system. P V ~P > *is*ZEROth*-order, to start with. > First-order 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