<freddywilli...@btinternet.com> wrote:
> Nam Nguyen wrote:
> > Fwiw, one of the mistakes I made is I threw away a copy of Kleene's book
> > I had held for years. [...]
> If you disposed of it in a respectful manner then it was no mistake,
> Kleene's book is difficult.
> G\"odel's paper was about P which can indeed express elementary
> arithmetic, and let's hope its theorems are indeed true. But G\"odel
> nowhere relies on them being true. Nor is a quote from Kleene (to which
> I have no objection) a quote from G\"odel's proof of G\"odel theorem.
> Having proved, for some sentence phi in the language of P, that
> neither P |- phi nor P |- ~phi
> one can go on and claim
> one of phi and ~phi is true because phi is a sentence
Ahh! Fred has finally reached [ERROR 1]
At this rate, Aatu will be figuring out how to construct a_ny sentence
F&~F |- g, g<->~prv(g)
by next Easter!
------------------------------------
[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"
PA |- P
This is using an axiom-less or inconsistent theory
CONTRADICTION |- ANY FORMULA
--------------------------------------
[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 (but not formula with quantifiers)
You conclude adding AXIOMS to PA could never filter out the Godel
Statement and call it
MONOTONIC LOGIC!
-------------------------------
On Oct 28, 2:36 am, Nam Nguyen <namducngu...@shaw.ca> wrote:
> >> - Therefore a theory that can carry out basic arithmetic operations
> >> is a consistent theory.
> > G del never says any such thing.
> Not literally word for word of course. No more than he said
> that his informal proof can be "formalized" by PRA 80 years
> later, word for word.
SCI.MATH and SCI.LOGIC seem to think FORMAL means it's got A, E, ~,
( ) in it!
Common mistake by beginners to assume their language is formal because
it looks rigorous but it's actually a lot of work to construct an
actual formal system.
On Oct 27, 11:28 am, George Greene <gree...@email.unc.edu> wrote:
> EVERYthing is formal and algorithmic. In particular, first-order
> INFERENCE AND PROOF are formal and algorithmic.
This is just LINE BY LINE level of automation, not a formal system.
Same MEGA-MISTAKE by Godel and Tarski.
The FORMAL SYSTEM enumerates the sentences, you don't CONSTRUCT
anything!
"We can CONSTRUCT *A* sentence" L<->~Tr(#L)
/\
||
\/
"We can CONSTRUCT *ANY* sentence" L<->~Tr(#L)
/\
||
\/
F&~F |- W
From a Contradiction Anything Follows!
You cannot prove anything about Axiomatic Systems this way!
QED
> On Oct 30, 2:24 am, Graham Cooper <grahamcoop...@gmail.com> wrote:
> > On Oct 30, 11:14 am, MoeBlee <modem...@gmail.com> wrote:
> > > On Oct 29, 8:10 pm, Graham Cooper <grahamcoop...@gmail.com> wrote:
> > > > MoeBlee wrote:
> > > > > It's a simple exercise to derive the more ordinary
> > > > > axioms.
> > > > You don't derive axioms.
> > > We may derive axioms of one system from axioms of another system.
> > > > So your SUICIDE THEOREMS that destroy the consistency of any Theory
> > > > are not only Self-Defeating, but it's a Time Bomb ticking away...
> > > > Because when a rudimentray Logic Theory comes along in .EXE form it's
> > > > not going to be bothered by your posts here and in every Uni Library
> > > > that it can't calculate this and it can't calculate that...
> > > > ___________________
> > > > In fact, I write this melancholy foresight for a reason. I figured
> > > > out how to get PROLOG UNIFY(f1, f2) solving predicates.
> > > > Its really quite simple!
> > > You are quite simply off the deep end.
> > > MoeBlee
> > Unlike the shallow theories you regurgitate ad infinitum that cannot
> > even solve this!
> > ?- and( or(1,0) , or(0,X) )
> > X=1
> What's the meaning of the symbol "?-"
Backward Chain the Answer. UNIFY( query, <database> )
