```Date: Oct 14, 2012 9:21 PM
Author: Graham Cooper
Subject: Re: If ZFC is a FORMAL THEORY ... then what is THEOREM 1 ?

> LHS & (LHS -> (a&b->c)) -> a&b->c>> to derive models of backward chainable embedded theories that are> recursively provable back to the axioms!>BINARY MODUS PONENSa & b & (a&b)->c  --> cThis not only WORKS!  It derives all proofs!PROOF = backward chainable binary directed acylic graphYou're still stuck on the 'CLASSIC THEOREM'!******** 10 YEARS DEBUGGING TO FIX THIS **********>   NOT(PA |- P) & NOT(PA |- ~P).> That is the classical theorem.  Duh.> [...]> >> I don't see your point.  The theorem says that PA can not decide a> >> particular formula.> > no, a particular wff (conditions apply)> When I say "formula", I mean "WFF".  I have no reason to talk about> non-well-formed formulas.That's why your proof is wrong.-------------------------------------[ERROR 1]By WFF you mean it has a single reduction tree in predicate calculusfrom sub predicates and atomic formula, giving it a uniqueinterpretation. So you have limited the scope of your proof to booleanformula (true or false).-------------------------------[ERROR 2]THEN:  YOU START ADDING FORMULA AT WILL."WE CAN CONSTRUCT ANY FORMULA AND TRY TO ADD IT TO THE THEORY"ERROR!PA |- PThis is using an axiom-less or inconsistent theoryCONTRADICTION |- ANYTHING--------------------------------------[VALID STEP]Because P is "true" by some rudimentary reductions (P can't be false)NOT( PA |- P )NOT( PA |- ~P )-------------------------------------[ERROR 3]P <-> NOT( PA |- P )so P is TRUE  (in PA)-------------------------------------[ERROR 4]P is a WFF in PA    ANDP is TRUE in PA--->  P is a missing theorem of PAYou EQUATEWFF + TRUE -->  THEOREM-------------------------------------[ERROR 5]Because:(P -> Q)  ->   (P ^ AXIOM) -> Qis true for 0 order terms (not formula with quantifiers)You conclude adding AXIOMS to PA could never filter out the GodelStatement and call itMONOTONIC LOGIC!--------------------------------Herc
```