Summary: we haven’t actually got to the meat of Löb’s theorem yet.
We went over:
first-order logic
enough model theory to observe that “truth” is a property of a sentence applied to a model, whereas “provability” is a property of a sentence applied to a theory
mentioned Gödel’s completeness theorem (that “provable” = “true in all models”)
mentioned the Löwenheim-Skolem theorems which guarantee that there are nonstandard models of Peano arithmetic (in fact, nonstandard models of arbitrarily large cardinality), and handwaved what the smallest [countable] nonstandard model looks like (but my memory is very poor on this, and I might have got that model wrong)
observed that Gödel’s [first] incompleteness theorem can be sloppily stated as “there is a sentence S which is true but not provable” (or more precisely, there are models of Peano arithmetic in which S evaluates to false, but in the standard model \mathbb{N} S evaluates to true)
observed the diagonal lemma, and disagreed on whether it’s obvious; I believe it’s extremely nonobvious and indeed mind-bending and it took me several hours to reliably be able to write a quine, but perhaps I simply haven’t read Gödel, Escher, Bach recently enough.
Assuming the existence of an “is-provable” operation which can be coded up with primitive-recursive functions on the naturals and which satisfies three particular axiom [schema]s (the Hilbert-Bernays provability conditions, though I didn’t give them that name), we observed that the proof Yudkowsky gives in the Cartoon Guide is in fact correct, but we haven’t yet talked about what it means. (I noted that I dislike the cartoon guide, because it’s so… big.)
I also did a bit of fanboying about the Curry-Howard correspondence.
Interesting tidbits:
I claimed that “there’s only one axiom [schema] of first-order logic which makes the False symbol special, and that’s the Law of Excluded Middle”. Without LEM, no axiom schema mentions the symbol False, so the principle of explosion (“False implies everything”) follows a rather curious path: induction on proofs. If you’ve got a proof whose final line is False, then you could perform exactly the same proof but instead replace all instances of False with some fixed but arbitrary A, and then at the end rather than proving False you’ve produced a proof of A. Once we add LEM, this reasoning no longer works, because it’s no longer valid to substitute the occurrences of the symbol False within usages of LEM; so we need some other reason for explosion to be true. It follows from LEM thus: from False, deduce (A → False) → False, by “true things are implied by everything” (strictly, this is from the P → (Q → P) axiom schema). Then by LEM and modus ponens, conclude A.
Homework: Yudkowsky explicitly stated the Löb sentence, a specific sentence L such that PA proves “L iff (Provable(L) implies P)”. This sentence is what you get when you run the usual proof of a much more general theorem, the Diagonal Lemma, on the syntactic manipulation “turn L into the statement ‘Provable(L) implies P’”. Exercise: perform the diagonal lemma (“quining”) construction on the syntactic manipulation “turn L into the statement ‘len(L) ⇐ 1000’”. Note that the number 1000 is very long—more than 1000 characters long, it’s SSSSS…SSS0 - so we expect this construction to result in a false L (by contrast with the use in Löb’s theorem, where it results in an L that is true under the Löb hypothesis). I haven’t yet done this, and it might be rather hard, I don’t know!
Notes from first meeting
Summary: we haven’t actually got to the meat of Löb’s theorem yet.
We went over:
first-order logic
enough model theory to observe that “truth” is a property of a sentence applied to a model, whereas “provability” is a property of a sentence applied to a theory
mentioned Gödel’s completeness theorem (that “provable” = “true in all models”)
mentioned the Löwenheim-Skolem theorems which guarantee that there are nonstandard models of Peano arithmetic (in fact, nonstandard models of arbitrarily large cardinality), and handwaved what the smallest [countable] nonstandard model looks like (but my memory is very poor on this, and I might have got that model wrong)
observed that Gödel’s [first] incompleteness theorem can be sloppily stated as “there is a sentence S which is true but not provable” (or more precisely, there are models of Peano arithmetic in which S evaluates to false, but in the standard model \mathbb{N} S evaluates to true)
observed the diagonal lemma, and disagreed on whether it’s obvious; I believe it’s extremely nonobvious and indeed mind-bending and it took me several hours to reliably be able to write a quine, but perhaps I simply haven’t read Gödel, Escher, Bach recently enough.
Assuming the existence of an “is-provable” operation which can be coded up with primitive-recursive functions on the naturals and which satisfies three particular axiom [schema]s (the Hilbert-Bernays provability conditions, though I didn’t give them that name), we observed that the proof Yudkowsky gives in the Cartoon Guide is in fact correct, but we haven’t yet talked about what it means. (I noted that I dislike the cartoon guide, because it’s so… big.)
I also did a bit of fanboying about the Curry-Howard correspondence.
Interesting tidbits:
I claimed that “there’s only one axiom [schema] of first-order logic which makes the False symbol special, and that’s the Law of Excluded Middle”. Without LEM, no axiom schema mentions the symbol False, so the principle of explosion (“False implies everything”) follows a rather curious path: induction on proofs. If you’ve got a proof whose final line is False, then you could perform exactly the same proof but instead replace all instances of False with some fixed but arbitrary A, and then at the end rather than proving False you’ve produced a proof of A. Once we add LEM, this reasoning no longer works, because it’s no longer valid to substitute the occurrences of the symbol False within usages of LEM; so we need some other reason for explosion to be true. It follows from LEM thus: from False, deduce (A → False) → False, by “true things are implied by everything” (strictly, this is from the P → (Q → P) axiom schema). Then by LEM and modus ponens, conclude A.
Homework: Yudkowsky explicitly stated the Löb sentence, a specific sentence L such that PA proves “L iff (Provable(L) implies P)”. This sentence is what you get when you run the usual proof of a much more general theorem, the Diagonal Lemma, on the syntactic manipulation “turn L into the statement ‘Provable(L) implies P’”. Exercise: perform the diagonal lemma (“quining”) construction on the syntactic manipulation “turn L into the statement ‘len(L) ⇐ 1000’”. Note that the number 1000 is very long—more than 1000 characters long, it’s SSSSS…SSS0 - so we expect this construction to result in a false L (by contrast with the use in Löb’s theorem, where it results in an L that is true under the Löb hypothesis). I haven’t yet done this, and it might be rather hard, I don’t know!