For those interested, Hoffstadter's Godel Escher Bach gives a great introduction into formal systems and Godels incompleteness theorem. Highly recommended.
(GEB has other philosophical discourses that are interesting, if only as an example of how people can very reasonably mispredict the future. In Hofstader’s case, he posited that chess would only be played at a human level by an AGI.)
I read Godel's Proof after though, and I agree that it is a far clearer introduction to Godel's theorems.
Also, the book is about 98% Gödel and 2% Escher and Bach. Any time it steps outside its wheelhouse of math and into the realm of philosophy or art, you get the distinct sense that it has no idea what it's talking about.
Do yourself a favor and just take discrete math 1 and read a few Wikipedia articles instead.
+100, exactly. I have some familiarity with mathematical logic, and with Bach (though admittedly I'm less familiar with Escher) and I found GEB to be unintuitive at best, and misleading at worst.
To be honest, there may not be anything really magic about Goedel's incompleteness theorem once you grasp the core concept, which is: If you encode all proofs into a formal language, you can make a statement that is true but unprovable. (Which is, effectively: "This statement has no proof"). Most of Goedel's work on the incompleteness theorem was on the systematization of proofs, which can be tedious to work through.
I found at the time Godel's completeness theorem to be more interesting. Though I never got into model theory or more advanced mathematical logic so, grain of salt.
Godel's proof of inferential undecidability [incompleteness] was too superficial. It didn't get at the real heart of what was going on. It was more tantalizing than anything else. It was not a good reason for something so devastating and fundamental. It was too clever by half. It was too superficial. [It was based on the clever construction] I'm unprovable. So what? This doesn't give any insight how serious the problem is.
And GEB's explanation of it is more complete/exact than the one in the article.
It is also amazingly mind-twisting. Not the explanation per se, but the theorem.
And I think its consequences are under appreciated: no (sufficiently complex) logical system is free from self-contradictions.
Incompleteness: there exist true statements that lack proofs
Unsoundness: there exist false statements with proofs
If I understand all this correctly, what Goedel demonstrated was that a sufficiently complex logical system could self-reference, and from self-reference unprovable (not contradictory) true statements fall out.
By reductio ad absurdum any self-contradictory logical system is useless as a logic because everything is provable in it, so one wonders if such systems should even be considered "logical systems".
You don't RAA it because you can't prove the system is consistent (because you can't prove the counterexample)
I believe your position is that "sufficiently complex" == "able to formulate and prove its own consistency"; my position is that such a system would be worthless as a logic, because in such a system you can prove anything.
Your second paragraph is inscrutable to me. Are you trying to claim that you can't prove everything with a known inconsistent logic? Are you referring to paraconsistent logics?
[1] http://mathworld.wolfram.com/GoedelsSecondIncompletenessTheo...
Meaning, not "trivially simple". The description in your link is good enough, the description in the Wikipedia is more detailed
> any formal system that is interesting enough to formulate its own consistency can prove its own consistency iff it is inconsistent.
That's what "sufficiently complex" means and why you can't Reduction Ad Absurdum it.
That doesn't seem right? Any logical system that has a self-contradiction (which I take to mean can prove a statement and its inverse) will be able to prove everything, which is obviously a pretty big flaw.
What Godel's 2nd incompleteness theorem says is that if a system can prove its own consistency, then it follows that it is unsound.
In this theory, proof checking is computationally decidable even though the theorems are not computationally enumerable by a total procedure.
No it doesn't - that would contradict Goedel's well-established theorem. The formal consistency of Peano arithmetic has been proven, but not by Peano arithmetic:
> Gentzen's theory obtained by adding quantifier-free transfinite induction to primitive recursive arithmetic proves the consistency of first-order Peano arithmetic (PA) but does not contain PA [...] Gentzen's theory is not contained in PA, either, however, since it can prove a number-theoretical fact—the consistency of PA—that PA cannot. [1]
[1] https://en.wikipedia.org/wiki/Gentzen%27s_consistency_proof#...
Also, Godel's proposition "I'mUnprovable" does not exist in the higher order theory because it doesn't type check.
I also don't understand how proof checking can be decidable if the axioms are not recursively enumerable. If proof checking is decidable, there must be a way of determining if a use of an axiom refers to a valid axiom. But if you can do that, as long as you can put the syntactic formulas of the system in bijection with the natural numbers (which I presume is the case if this is aimed at computing, and would hope in general that you can write them on paper using a finite string of symbols) you can produce an enumerating program by just running the decision procedure on every syntactic formula and only emitting ones that pass. More succinctly, all recursive sets are recursively enumerable.
But proof checking is still computationally decidable by a provably total higher order procedure. See the following: https://hal.archives-ouvertes.fr/hal-01566393
See the following: https://cacm.acm.org/blogs/blog-cacm/231495-what-turing-and-...