Post by Charlie-BooPost by Graham Cooper"Understanding Godel isn't about following his formal proof.
That would make a mockery of everything Godel was up to."
Since I'm obsessed with following in full detail a rigorous account of Godel's theorems (I've yet to find one online which has the detail I want and where I don't get stuck on one of the steps), then obviously I must be doing completely the wrong thing, ullrichistically speaking.
If following his formal proof is the wrong way to understand Godel, then what is a better way to understand Godel?
Thank You,
Paul Epstein
Beware the difference between GODELS PROOF
and MATHEMATICS ABOUT GODELS PROOF.
The latter is a lot more convoluted and not necessary to 1st follow
the proof itself.
“It is an error to believe that rigour is the enemy of simplicity. On
the contrary we find it confirmed by numerous examples that the
rigorous method is at the same time the simpler and the more easily
comprehended. The very effort for rigor forces us to find out simpler
methods of proof.” - David Hilbert, 'Mathematical Problems', Bulletin
of the American Mathematical Society (Jul 1902), 8, 441
“18 Word Proof of the Godel, Rosser and Smullyan Incompleteness
Theorems” http://www.cs.nyu.edu/pipermail/fom/2010-July/014890.html
Post by Graham CooperT1|-!(PRV(GS-GN)) & T2|-PRV[ T1|-!(PRV(GS-GN)) ]
!PRV(GS-GN) is true in THEORY 1
and
that fact is proven in THEORY 2.
GS = !PRV(GS-GN) *a Godel Statement
What are T1, PRV, GS-GN, T2, THEORY 1, THEORY 2 and GS? What is the
purpose of displaying these expressions?
EXACTLY MY POINT!
Beware the difference between GODELS PROOF
and MATHEMATICS ABOUT GODELS PROOF.
Post by Charlie-BooPost by Graham CooperAlso beware the phrase
"IN ANY THEORY WITH SUFFICIENT EXPRESSIVENESS..
..WE CAN CONSTRUCT THIS SENTENCE ..."
Ironically, they say that exactly because they have not formalized
it. They don’t know what the actual premise is, and so they use a
meaningless phrase “sufficiently expressive”.
Post by Graham CooperThat only holds for ZERO-AXIOM or INCONSISTENT systems where ALL (true
and false) theorems follow.
It holds for any system in which we can express “x is the number of a
provable sentence”, and the premise (soundness or w-consistency) is
true, depending on the version being cited from his 1931 paper. Both
hold for ordinary Peano Arithmetic.
NO!
TARSKI makes the EXACT SAME ERROR as GODEL
[DARYL]
Fix a coding for arithmetic, that is, a way to associate a unique
natural number with each statement of arithmetic. In terms of this
coding, a truth predicate Tr(x) is a formula with the following
property: For any statement S in the language of arithmetic,
Tr(#S) <-> S
holds (where #S means the natural number coding the sentence S).
If Tr(x) is a formula of arithmetic, then using techniques
developed by Godel, we can construct a sentence L such that
L <-> ~Tr(#L)
But by the definition of a truth predicate, we also have
L <-> Tr(#L)
NOTICE THE "we can construct a sentence L"
*a* sentence means *any* sentence here.
START WITH AN INCONSISTENT THEORY
then using techniques developed
by Godel, we can construct *ANY* sentence L
T |- W
T |- L
T |- L<->~G2T(L) *IN T |- W ANY FORMULA IS TRUE
T |- L<->G2T(L)
T |- L , T |- ~L *contradiction
T |- W *now any formula is true
Yeh so?
*************************
For any Theory T and it's Theorems t1, t2,t3,...
T |- t1 ^ t2 ^ t3 ^ t4 ^ ....
t3 <-> ~true(#t3)
t3 <-> not(t3)
IS CONSTRUCTABLE
ergo:
T |- t1 ^ t2 ^ t3 ^ (t3<->not(t3)) ^ t4 ^ ...
T |- t1 ^ t2 ^ t3 ^ not(t3) ^ t4 ^ ...
T |- contradiction
T |- any formula
ex contradictione sequitur quodlibet
from a contradiction, anything follows
{t3, !t3} |- W
So by allowing *any formula* you can possibly construct to be a
theorem of the Theory, Tarski proved that ANY_FORMULA can be a theorem
of the Theory.
Herc
KINGS Beach
QUEENSland
--
http://tinyURL.com/DEFINITION-MATHEMATICS
http://tinyURL.com/BLUEPRINTS-HYPERREALS
http://tinyURL.com/BLUEPRINTS-HALT-PROOF
http://tinyURL.com/BLUEPRINTS-QUESTIONS
http://tinyURL.com/BLUEPRINTS-POWERSET
http://tinyURL.com/BLUEPRINTS-THEOREM
http://tinyURL.com/BLUEPRINTS-TARSKI
http://tinyURL.com/BLUEPRINTS-FORALL
http://tinyURL.com/BLUEPRINTS-TURING
http://tinyURL.com/BLUEPRINTS-GODEL
http://tinyURL.com/BLUEPRINTS-PROOF
http://tinyURL.com/BLUEPRINTS-LOGIC
http://tinyURL.com/BLUEPRINTS-BRAIN
http://tinyURL.com/BLUEPRINTS-SETS
http://tinyURL.com/BLUEPRINTS-PERM
http://tinyURL.com/BLUEPRINTS-P-NP
http://tinyURL.com/BLUEPRINTS-LIAR
http://tinyURL.com/BLUEPRINTS-GUT
http://tinyURL.com/BLUEPRINTS-BB
http://tinyURL.com/BLUEPRINTS-AI