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