[HN Gopher] An Introduction to Godel's Theorems (Second Edition)...
___________________________________________________________________
An Introduction to Godel's Theorems (Second Edition) [pdf]
Author : furcyd
Score : 86 points
Date : 2020-08-07 13:59 UTC (9 hours ago)
(HTM) web link (www.logicmatters.net)
(TXT) w3m dump (www.logicmatters.net)
| hwc wrote:
| Why does the author use "sound" instead of "consistent"?
| Smaug123 wrote:
| I can recommend Peter Smith as an author; I was part of a small
| reading group with him while we were all getting to grips with
| Cambridge's Part III Introduction to Category Theory, and he's
| definitely good at identifying the difficult bits and breaking
| them down.
| bmitc wrote:
| I need to learn more about Godel and read the books about him.
| From the outside, he almost seems like an intellectual rebel,
| showing how systems are broken when people assume they aren't.
| With his completeness theorems and his Godel metric, he seemed to
| be excited by logical exotica. I find the Godel metric and its
| closed timelike curves to be an interesting case study of general
| relativity. This is just me spitballing here, as I have not yet
| dove into the many books I have on him.
| antman wrote:
| This is a book, if someone wants to introduce himself to the
| field and its actors I suggest Logicomix.
| braindongle wrote:
| If you're uninitiated and simply want to grok where true-but-
| unprovable comes from, I recommend:
| https://www.quantamagazine.org/how-godels-incompleteness-the...
|
| Wolchover is masterful here. The layers of abstraction keep
| piling up, and I had to read the last part more than a couple of
| times to really get it, but then you have it.
| dvt wrote:
| Just going to echo @dwohnitmok here in saying that this is a
| pretty 'meh' article. Understanding Godel's First
| Incompleteness Theorem is actually very accessible, I wrote
| about it a few years ago[1]. His second is _much_ more involved
| and laymen won 't have the required tools to grasp it. In my
| opinion, the easiest way to understand it is probably using
| Lob's Theorem, but that's neither here nor there. Either way,
| I'm of the opinion that arithmetic coding is very confusing and
| shouldn't be used to introduce people to Godel.
|
| [1] https://dvt.name/2018/03/12/godels-first-incompleteness-
| theo...
| krick wrote:
| I'm not sure this is equivalent to Godel's theorem. Actually,
| I'm not sure this is a correct proof of anything at all,
| merely a sort-of demonstration of Richard's paradox.
|
| First, for reference, let me quote First Incompleteness
| Theorem: "Any consistent formal system F within which a
| certain amount of elementary arithmetic can be carried out is
| incomplete; i.e., there are statements of the language of F
| which can neither be proved nor disproved in F." (from
| Wikipedia)
|
| Now back to your post.
|
| Obviously, f' is not in T and it is not computable. But
| neither is T. It is incomputable merely by being the list of
| computable functions, which we cannot construct because of
| halting problem and stuff like that.
|
| And your definition of f' relies on having T. So we don't in
| fact have seen "statement f'". So, the direct connection
| between Godel's theorem and your construct is not obvious to
| me, because first is about constructable, but unprovable
| statements, and second seems to be a faulty (i.e.
| mathematically uninterpretable) construct itself.
| dvt wrote:
| > I'm not sure this is equivalent to Godel's theorem.
|
| It is. In fact, I've seen it proven this way several times
| (mostly in CS-y papers), but it's definitely not common. My
| post is in fact based (almost beat-by-beat) on this UC
| Davis lecture: https://www.youtube.com/watch?v=9JeIG_CsgvI
| krick wrote:
| Your plain and confident statement "it is" doesn't really
| address any of my concerns, and I just explained why, as
| it seems, it actually isn't.
|
| P.S.
|
| I did some random googling, and while I'm not sure, all
| this story seems to be based off of Paul Finsler's work,
| which he himself thought to be the priority for an
| incompleteness theorem (Collected Works Vol. IV., p. 9),
| but didn't seem so to Godel (and, seemingly, the majority
| of those who had to say something about it).
|
| If this indeed is the same thing, it would explain to me
| why this "proof", which doesn't seem to me like a proof
| at all is so widespread. But, again, I'm not sure I'm
| reading into it correctly, and operating under assumption
| that if somebody could provide something more weighty
| than "it is" statement, I could be persuaded otherwise.
| irontinkerer wrote:
| Per the end of your article, have you started writing about
| the 2nd theorem yet?
| dvt wrote:
| I did (https://dvt.name/2018/04/11/godels-second-
| incompleteness-the...) -- but like I mentioned, it's not
| very accessible and I don't think it's a particularly good
| explanation, either (although I've yet to find one I really
| like, to be honest).
| dwohnitmok wrote:
| The article plays a little fast and loose with language
|
| > For example, Godel himself helped establish that the
| continuum hypothesis, which concerns the sizes of infinity, is
| undecidable, as is the halting problem
|
| The continuum hypothesis is definitely not "undecidable" in the
| same way that the halting problem is undecidable. Though there
| are deep connections behind the two, the two notions of
| "undecidability" (logical independence in the former and Turing
| machine computability in the latter) are very different.
|
| Also,
|
| > He also showed that no candidate set of axioms can ever prove
| its own consistency.
|
| This is powerful as a limiting result, but it has little direct
| impact for philosophy, because you wouldn't trust the
| consistency result of a system you suspect might be
| inconsistent to begin with because inconsistent systems can
| prove anything. So saying "my axioms prove themselves
| consistent" shouldn't have increased your trust in those axioms
| to begin with in the absence of the incompleteness theorems.
|
| I'm not really a fan of "true-but-unprovable" as short-hand the
| incompleteness theorems, because that hinges a lot on what kind
| of logic system you're in and how that logic system defines
| "truth" (taken at face value, how do we know that Godel's
| incompleteness theorem is "true?").
|
| I prefer rather to pose two questions to reflect on that I
| think illuminate Godel's incompleteness theorems some more.
| Most modern logical systems (e.g. first-order logic and its
| various extensions and variants) equate unproveability with
| logical independence. So with that in mind, here's two
| questions.
|
| First, Conway's Game of Life:
|
| Conway's Game of Life seem like they should be subject to
| Godel's incompleteness theorems. It is after all powerful
| enough to be Turing-complete.
|
| Yet its rules seem clearly complete (they unambiguously specify
| how to implement the Game of Life enough that different
| implementation of the Game of Life agree with each other).
|
| So what part of Game of Life is incomplete? What new rule (i.e.
| axiom) can you add to Conway's Game of Life that is independent
| of its current rules? Given that, what does it mean when I say
| that "its rules seem clearly complete?" Is there a way of
| capturing that notion? And if there isn't, why haven't
| different implementations of the game diverged? If you don't
| think that the Game of Life should be subject to Godel's
| Incompleteness Theorems why? Given that it's Turing complete it
| seems obviously as powerful as any other system.
|
| Second, again, in most logical systems, another way of stating
| that consistency is unproveable is that consistency of a system
| S is independent of the axioms of that system. However, that
| means that the addition of a new axiom asserting that S is
| either consistent or inconsistent are both consistent with S.
| In particular, the new system S' that consists of the axioms of
| S with the new axiom "S is inconsistent" is consistent if S is
| consistent.
|
| What gives? Do we have some weird "superposition" of
| consistency and inconsistency?
|
| Hints (don't read them until you've given these questions some
| thought!):
|
| 1. Consider questions of the form "eventually" or "never." Can
| those be turned into axioms? If you decide instead to tackle
| the question of applicability of the incompleteness theorems,
| what is the domain of discourse when I say "clearly complete?"
| What exactly is under consideration?
|
| 2. Consider carefully what Godel's arithmetization of proofs
| gives you. What does Godel's scheme actually give you when it
| says it's "found" a contradiction? Does this comport with what
| you would normally agree with? An equivalent way of phrasing
| this hint, is what is the actual statement in Godel's
| arithmetization scheme created when we informally say "S is
| inconsistent?"
|
| At the end of the day, the philosophical implications of
| Godel's incompleteness theorems hinge on whether you believe
| that it is possible to unambiguously specify what the entirety
| of the natural numbers are and whether they exist as a separate
| entity (i.e. does "infinity" exist in a real sense? Is there a
| truly absolute standard model of the natural numbers?).
| braindongle wrote:
| Who cares about the philosophical implications of the
| theorems? Philosophers! The linked article is about how the
| theorems destroyed Whitehead et al's aspirations to find One
| Algebra To Rule Them All.
|
| The literature on Godel and philosophy is gargantuan, for
| some reason. Wasn't it summed up well by Wittgenstein?
| Paraphrasing: "Who cares about your contradictions?" Well
| said. Also not the topic Wolchover's article.
|
| Math people can make the same move: "Who cares about your
| philosophizing?"
| dwohnitmok wrote:
| > The linked article is about how the theorems destroyed
| Whitehead et al's aspirations to find One Algebra To Rule
| Them All.
|
| Sort of. Whitehead's contributions to universal algebra are
| still relevant and universal algebra is still a thriving
| field of study for mathematical logic. Although perhaps you
| mean "algebra" in a more informal sense?
|
| Again, the conclusion of the article is a bit strong.
|
| > Godel's proof killed the search for a consistent,
| complete mathematical system.
|
| The consistency half doesn't make sense. (EDIT: I get it
| now, see the last sentence of this paragraph) There was
| never a search for a consistent mathematical system in the
| sense that Godel destroyed because again a system that can
| prove its own consistency has no positive value in
| evaluating the consistency of that system (Godel's big
| contribution here is contributing a strong negative result,
| if it could prove its own consistency you're pretty
| screwed). EDIT: On reflection I see that the sentence
| probably means to tie consistency to completeness rather
| than as a stand-alone quality. That makes more sense.
|
| As for mathematicians, their reactions to Godel's
| incompleteness theorems overall are probably similar to
| "Who cares about your incompleteness theorems?" (there's a
| reason Russell and Whitehead are known primarily for being
| philosophers first and mathematicians second and why often
| times there is distinction between logicians like Godel and
| other mathematicians). Most mathematicians don't think
| about the foundations of mathematics because it is (perhaps
| surprisingly) largely irrelevant to the day-to-day work of
| mathematicians. Indeed the vast majority of mathematics is
| very resilient to changes in its underlying foundations.
|
| To interpret Godel's incompleteness theorems requires a
| healthy dose of at least mathematical logic that can start
| veering quite close to mathematical philosophy.
|
| An example from the article:
|
| > However, although G is undecidable, it's clearly true. G
| says, "The formula with Godel number sub(n, n, 17) cannot
| be proved," and that's exactly what we've found to be the
| case!
|
| Well no, that's not true in certain senses. Indeed in a
| larger axiomatic system subsuming the current system that
| corresponds to G, it is completely consistent to state that
| G is provable and that its statement is provable (see my
| example of S'), i.e. there are Godel numbers that
| correspond to both a proof of G and to a proof of its
| content. To interpret that statement that way requires
| certain philosophical commitments to the correspondence
| between a Godel number and truth, which not everyone would
| accept (do you accept the truth of the new axiom introduced
| by S'? Why then do you accept the truth of the statement "S
| is consistent?" and vice versa).
|
| "In striving for a complete mathematical system, you can
| never catch your own tail." This on the other hand I think
| is a very good informal description of what's on with
| Godel's incompleteness theorems. Focus on the
| incompleteness not on truth.
|
| That's why I'm not a fan of using the word "truth" when
| talking about Godel's incompleteness theorems. I am in fact
| deeply sympathetic to your desire to separate philosophy
| from Godel's incompleteness theorems.
|
| I prefer to clearly delineate between its logical
| properties in mathematical logic and its philosophical
| implications and using the word "truth" by necessity
| muddles the two.
|
| FINAL EDIT: I am being perhaps a bit too harsh on the
| article. I think it does a fine job of describing the
| arithmetization of the incompleteness theorems. But if
| someone else reading this also decides to create an
| informal guide to Godel's incompleteness theorems, please
| please please don't use the word "truth" and "true" or at
| least separate it out into its own section on philosophy.
| pdonis wrote:
| _> that 's not true in certain senses_
|
| I think it's not true in a very clear sense: you can
| construct semantic models of the axioms of arithmetic in
| which it is false. In other words, you can construct
| semantic models of the axioms of arithmetic (more
| precisely, of the axioms of arithmetic using first-order
| logic, which is what the article is about) in which there
| _is_ a "number" that is the Godel number of a proof of
| the Godel sentence G! Godel's Theorem just ensures that
| in any such model, the "number" that is the Godel number
| of such a proof will _not_ be a "standard" natural
| number, i.e., one that you can obtain from zero via the
| application of the successor operation.
|
| So another way of viewing this whole issue of "truth" is
| that it is always relative to some semantic model. If
| your chosen semantic model of the axioms of arithmetic is
| the "standard" natural numbers, and _only_ those numbers,
| then the Godel sentence G for that system will be true--
| there will indeed be no number in your model that is the
| Godel number of a proof of G. But if you pick instead a
| non-standard model that includes "numbers" other than
| the standard natural numbers, but still satisfies the
| axioms, then the Godel sentence G can be false in that
| model, since there _can_ exist a "number" (just not a
| standard one) in that model that is the Godel number of a
| proof of G.
| unknown_apostle wrote:
| Very interesting remarks... never looked at it in this way.
| Thx!
|
| Care to write a short but more explicit wrap up of how you
| see your two questions yourself?
| jjcc wrote:
| May I suggest that "true" in "true-but-unprovable" means from
| God's eye or in a higher level system but not in current system
| because "unprovable"(in current system only) means it's not
| really true in current system? Correct me if I'm wrong in this
| context.
| hilbertseries wrote:
| You are wrong. Godel in fact showed precisely that there are
| unprovable statements in any consistent set of axioms. In
| fact it's equivalent. The only systems in which every
| statement is provable are inconsistent. Consistent here
| meaning that statements cannot be proven to be both true and
| false from axioms.
| dpierce9 wrote:
| This isn't quite right, though perhaps a nit, plenty of
| formal systems are provably sound (only true things are
| provable) and complete (all true things are provable). For
| example, the predicate calculus you learn in Logic 101.
| Formal systems become provably incomplete when they are
| able to express arithmetic (e.g., Peano axioms).
| dtornabene wrote:
| A Couple of comments here on "this isn't an introduction, its a
| book!!", for anyone who checked here first, that is the _title_
| of the book, and while I can 't speak to Smith's coverage, if
| you're going to "introduce" someone to the incompleteness
| theorems, a book is how you're going to do it. They're two of the
| most significant theorems in modern mathematics, maybe all of
| mathematics. Logicomix is fine, but I'm not pushing anyone to
| actually _learn_ these theorems through a graphic novel or a
| blogpost. As far as book alternatives, an interesting and useful
| way to get your head around what Godel was doing is to try to
| read Gottlob Frege, his notation isn 't that hard to parse, and
| it marks the origin point of modern mathematical logic and the
| attempt to do that which Godel proved impossible.
|
| Foundations of Arithmetic is easily readable with only a slight
| amount of contextualization for someone with a high school level
| mathematical education.
| ntabris wrote:
| For a shorter (but still fairly thorough) introduction by the
| same author, I recommend:
|
| https://www.logicmatters.net/igt/godel-without-tears/
|
| I found this super helpful when I was studying Godel's theorems
| in grad school. (Fwiw, the 3rd edition of Boolos & Jeffrey's
| _Computability and Logic_ is also great and takes a somewhat
| atypical approach to the proofs.)
| irontinkerer wrote:
| 402 pages is one incredible introduction!!
|
| Godel's theorems are fun to study though. What other theorems
| have equally blown your mind?
| throwgeorge wrote:
| coincidentally enough cantor's diagonalization was formative
| for me as a budding mathematician.
| boyobo wrote:
| Here is a nice, short proof, utilizing the conceptual framework
| of "Computation".
|
| https://www.scottaaronson.com/incompleteness.pdf
|
| See chapter 3.
| Kednicma wrote:
| It's a book! I was expecting a short paper along the lines of [0]
| or [1] but this is going to take a while to evaluate. Nonetheless
| I like the surface-level presentation and it seems like the
| author takes the time to carefully explain each concept in
| detail.
|
| [0] http://tac.mta.ca/tac/reprints/articles/15/tr15.pdf
|
| [1] http://r6.ca/Goedel/goedel1.html
___________________________________________________________________
(page generated 2020-08-07 23:01 UTC)