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 PONENS

a & b & (a&b)->c --> c

This not only WORKS! It derives all proofs!

PROOF = backward chainable binary directed acylic graph

You'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 calculus

from sub predicates and atomic formula, giving it a unique

interpretation. So you have limited the scope of your proof to boolean

formula (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 |- P

This is using an axiom-less or inconsistent theory

CONTRADICTION |- 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

AND

P is TRUE in PA

---> P is a missing theorem of PA

You EQUATE

WFF + TRUE --> THEOREM

-------------------------------------

[ERROR 5]

Because:

(P -> Q) -> (P ^ AXIOM) -> Q

is true for 0 order terms (not formula with quantifiers)

You conclude adding AXIOMS to PA could never filter out the Godel

Statement and call it

MONOTONIC LOGIC!

--------------------------------

Herc