
Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?
Posted:
Oct 7, 2012 5:48 PM


On Oct 8, 6:38 am, George Greene <gree...@email.unc.edu> wrote: > > Another point that makes enumeration irrelevant is that all the new > theorems > that you get from the axioms were in fact already present from the > UNDERLYING VALIDITIES that were provable FROM NO axioms, > because every proved theorem only USES a FINITE number of the axioms. > Thus, if the theorem was "h" and the axioms (or instances of axioms) > used > to prove it were a,b,c,d,f, and g, then > a^b^c^d^f^f>h > WAS ALREADY A THEOREM of *pure* predicate calculus, was ALREADY > a firstorder validity. So there really is a sense in which the > axioms merely > highlight a subset of the validities, as opposed to adding new stuff. > The order in which this highlighting occurs IS NOT important. > I'm SORRY FOR YOU, HERC, that the only treatment YOU have seen > HAPPENS to STRESS the "enumeration". You're a victim of a lame > education. > Which would be easily cured if you only had sense enough to read > ANOTHER book.
You can stick to "ENUMERABLE" if you are too clueless to WORK_OUT the ENUMERATION.
ATLEAST THAT'S SOMETHING TANGIBLE!
BUT YOU ARE CONTRADICTING YOURSELF ALL OVER THE PLACE.
YOU SAID THE SET OF TRUTHS ARE 'AUTOMATIC' AND NOT POSSIBLE TO DERIVE FROM AN ALGORITHM.
Herc 
GEORGE'S SET THEORY! *****************************
GEORGE'S RELATION ALGEBRA! aRb
GEORGE'S INFERENCE RULES! P > P ~(X > ~X) a^b^c^d^f^g>h
GEORGE'S SET AXIOMS! 1. Extensionality: AxAy [Az (zex <> zey) > x=y] 2. Regularity: Ax [Ea (aex) <> Ey (yex & ~Ez (zey & zex))] 3. Specification Schema: AzAw_1...w_nEyAx [xey <> (xez & phi)] 4. Pairing: AxAyEz (xez & yez) 5. Union: AfEaAyAx [(xey & yef) > xea] 6. Replacement Schema: AaAw_1...w_n [Ax (xea > E!y phi) > EbAx (xea > Ey (yeb & phi)] 7. Infinity: Ex [0ex & Ay (yex > S(y)ex)] 8. Powerset: AxEyAz [z subset x > zey] 9. Wellordering: AxEr (r wellorders x)
GEORGE'S VALIDATED SENTENCES! THEOREM 1 = .. THEOREM 2 = .. THEOREM 3 = !E(R) XeR <> !(XeX) *TADAAAA*

