```Date: Oct 12, 2012 8:37 PM
Author: camgirls@hush.com
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?

On Oct 13, 9:39 am, George Greene <gree...@email.unc.edu> wrote:> On Oct 12, 5:49 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:>> > deductive system is a list of formulas,> > each of which is a logical axiom>> NO, a deductive system IS NOT a list of formulas.>> JEEzus.That's a quote from WIKI>> > there is no decision procedure> > that determines whether arbitrary formulas are logically valid>> THERE IS, however, an algorithm that CONFIRMS that a formula is> logically valid WHEN IT IS.so why can't you do brute force lexicographically on ALL formulas andoutputVALIDNOT VALID> The consequence relation for standard classical first-order logic IS> SEMI-decidable.> The reason it is not a decision procedure is that there is no> algorithm that can confirm> (in the general case) that a first-order wff is NOT valid when it's> NOT (although that is also> confirmable SOMEtimes -- every confirmation that a wff IS valid is> also a confirmation&proof> that its denial is not).>> > So much for your ALGORITHMIC proof that>> > ~E(r) xer <-> ~xex>> > is a part of ZFC AUTOMATICALLY.>> NO, DUMBASS -- THERE IS a proof -- so, therefore, there is, also, by> definition, AN ALGORITHM that CONFIRMS> the existence of a proof -- that> ~Er[ xer <--> ~xex ] is valid.> If you had any sense you would just PRESENT THIS PROOF YOURSELF.I don't present proofs.I enter them into proof software and claim the theorem is true as faras the axioms and consistency of the proof software is concerned.>> BECAUSE this proof depends ON NO axioms -- LOGICAL OR OTHERWISE --> this sentence is necessarily valid> and necessarily a theorem OF ALL first-order formal theories in which> IT CAN BE STATED AT ALL, i.e., in which> a binary predicate e is in THE FIRST-ORDER LANGUAGE in which the> theory is being phrased.> All those theories "have" or "contain" (a theory is a set of sentences> that is closed under logical consequence)> all the first-order validities PLUS their axioms PLUS the theorems> THAT FOLLOW FROM their axioms...because you say so.Where on EARTH have you guys been HIDING this*******************************************************PLATONIC WORLD OF ABSOLUTE TRUTHS*******************************************************FOR THE LAST 10 YEARS YOU'VE BEEN DENYING1 SINGLE FORMULA IS BONA FIDE TRUE#.As far as MATHS AND LOGIC is CONCERNED#TRUE = W.R.T. STATED AXIOMSI have not SEEN a FORMAL PROOF BY RESOLUTION ONCE on SCI.LOGIC.I wan't born withT |- formula & ~formula->! (T |- formula )&T |- ~EXIST(formula)embedded into my AXIOMLESS AUTOMATIC Thought Processes!!Last chance George, put up THEOREM 1 of your AXIOMLESS LOGIC THEORY orSHUT UP!Herc
```