For years in my logic classes I’ve been giving a rough but fairly accessible sketch of the fact that there are unprovable arithmetical truths (a special case of Tarski’s indefinability of truth), using an explicit Goedel sentence using concatenation of strings of symbols rather than Goedel encoding and the diagonal lemma.
I’ve finally revised the sketch to give the full First Incompleteness theorem, using Rosser’s trick. Here is a draft.
3 comments:
Fact 2’s proof is intuitive (comparing proof lengths to derive a contradiction), but Fact 3 is waved off as “fiddling with strings.” I get that it’s a sketch, but this is the heart of self-reference, do you plan on outlining the fiddling? (e.g., “( r ) quotes itself and negates its own Rosser-provability.”)
Like in Fact 1, you prove that r is the only sentence that satisfies the antecedent of the big conditional in r, except you now make sure you do the proof in T. This seems to me pretty intuitive. In the Fact 1 setting, any string x that satisfies the big conditional has to look like Almost except that it has a quote instead of the asterisk, because it has to satisfy FQAsterisked(x,"Almost"). And the quote has to be a quote of Almost. The only string satisfying these two constraints is g.
Post a Comment