Answer to exercise “What’s the sentence you get from the diagonal lemma, L iff ‘L has length less-than-or-equal-to 1000’?”: len(“replace(’len(x) ⇐ 1000″, ‘x’ → “replace(‘len(x) ⇐ 1000’, ‘x’ → x)”)”) ⇐ 1000. I think.
We went through the Smullyan paper and got up to the moment before “The Stability Predicament”. The point of the paper turns out to be “if we interpret the box modality as ‘belief’, then a bunch of English sentences sound weird”. The real moral of the paper is that it’s awfully hard to be a knight or a knave on a knights-and-knaves island! (Making any statement about my beliefs involves extrapolating my entire future mind-state, for example, so only an extremely powerful knight or knave can make such a statement.) A bunch of the paper only requires that the reasoner believe the island to be a knight-knave island, but the reasoner is thereby making an extremely strong assumption.
Brief aside where I got confused about whether a symmetry argument meant we could never distinguish between knights and knaves: of course we can, because a knight can prove knighthood by saying “0 = 0”.
After some thought, we eventually decided that Smullyan’s “you will never believe I’m a knight” is equally well served by “you will eventually believe I’m a knave”, although this wasn’t obvious. The former is a statement about all of time; the latter is a statement only about an instant in time. The reasoner is assumed to never believe a false statement, though, so in fact once they believe something, it must be true.
General consensus that the notation of “type 1/2/3/4” is deeply annoying. I consistently refer to Type 1 as “deductively closed”, and then types 2/3/4 are precisely adding one each of the Hilbert-Bernays properties.
Question about what the semantics are, if “belief” (= proof) is the syntax. Answer which I was mostly satisfied with at the time: we’ve got a sequence of statements from numbered knight-or-knaves, and then we freeze the world and get to reason about which speaker has what property, eventually assigning them a boolean “is-knight” label.
Identification of typo in paper: p348 “if there is a proposition q such that he believes q~(Bq implies q), then he will believe p”; that should read “… q~(Bq implies p)…”.
Considerable confusion about why the self-fulfilling belief required the presence of a knight-or-knave at all, to say “If you ever believe I’m a knight, then the cure will work”. Why couldn’t the reasoner simply imagine this sentence to start off with? Answer: actually a later section makes explicit the condition under which the reasoner can imagine this sentence and hence perform all the reasoning of this sentence without a knight-or-knave: this is the “reflexive” property, that for every p there is q such that the reasoner believes q = (Bq implies p). This is of course true of PA, but that’s a heavy-duty fact that requires the diagonal lemma or an extremely inspired quine.
We stopped before section 5 due to lack of time, but I at least had a lot of fun, and our waiter said it sounded very interesting!
Homework:
We weren’t instantly convinced about the Remarks after “Reflexive Reasoners”. It was not at all obvious to me that statements 2, 3, or 4 in fact would have kicked off the Löb reasoning (that is, that they are suitable as Löb sentences). Prove that they do in fact work!
What is the status of all of this stuff if you reject excluded middle? A whole lot of stuff concludes “not A, or not-not-A”, and deduces “not A, or A”. Does Löb’s theorem even hold without LEM, for example? (Not at all obvious to me that it should! How could I magic up a member of A given only an interpretation function SyntaxTree(A) → A?)
Interesting tidbits:
PA (if consistent) can never prove any statement to be unprovable! Indeed, if PA proves “provable(A) → False”, then by explosion, PA proves “provable(A) → A”, and hence by Löb PA proves A. Hence by one of the Hilbert-Bernays rules, PA proves provable(A), and hence PA proves False by modus ponens. So, for example, PA can’t even prove “not(provable(0=1))”! Though it can prove “provable(not(0=1))”. Which is very weird, and I still feel like we must have made some mistake!
Notes from second meeting
Answer to exercise “What’s the sentence you get from the diagonal lemma, L iff ‘L has length less-than-or-equal-to 1000’?”: len(“replace(’len(x) ⇐ 1000″, ‘x’ → “replace(‘len(x) ⇐ 1000’, ‘x’ → x)”)”) ⇐ 1000. I think.
We went through the Smullyan paper and got up to the moment before “The Stability Predicament”. The point of the paper turns out to be “if we interpret the box modality as ‘belief’, then a bunch of English sentences sound weird”. The real moral of the paper is that it’s awfully hard to be a knight or a knave on a knights-and-knaves island! (Making any statement about my beliefs involves extrapolating my entire future mind-state, for example, so only an extremely powerful knight or knave can make such a statement.) A bunch of the paper only requires that the reasoner believe the island to be a knight-knave island, but the reasoner is thereby making an extremely strong assumption.
Brief aside where I got confused about whether a symmetry argument meant we could never distinguish between knights and knaves: of course we can, because a knight can prove knighthood by saying “0 = 0”.
After some thought, we eventually decided that Smullyan’s “you will never believe I’m a knight” is equally well served by “you will eventually believe I’m a knave”, although this wasn’t obvious. The former is a statement about all of time; the latter is a statement only about an instant in time. The reasoner is assumed to never believe a false statement, though, so in fact once they believe something, it must be true.
General consensus that the notation of “type 1/2/3/4” is deeply annoying. I consistently refer to Type 1 as “deductively closed”, and then types 2/3/4 are precisely adding one each of the Hilbert-Bernays properties.
Question about what the semantics are, if “belief” (= proof) is the syntax. Answer which I was mostly satisfied with at the time: we’ve got a sequence of statements from numbered knight-or-knaves, and then we freeze the world and get to reason about which speaker has what property, eventually assigning them a boolean “is-knight” label.
Identification of typo in paper: p348 “if there is a proposition q such that he believes q~(Bq implies q), then he will believe p”; that should read “… q~(Bq implies p)…”.
Considerable confusion about why the self-fulfilling belief required the presence of a knight-or-knave at all, to say “If you ever believe I’m a knight, then the cure will work”. Why couldn’t the reasoner simply imagine this sentence to start off with? Answer: actually a later section makes explicit the condition under which the reasoner can imagine this sentence and hence perform all the reasoning of this sentence without a knight-or-knave: this is the “reflexive” property, that for every p there is q such that the reasoner believes q = (Bq implies p). This is of course true of PA, but that’s a heavy-duty fact that requires the diagonal lemma or an extremely inspired quine.
We stopped before section 5 due to lack of time, but I at least had a lot of fun, and our waiter said it sounded very interesting!
Homework:
We weren’t instantly convinced about the Remarks after “Reflexive Reasoners”. It was not at all obvious to me that statements 2, 3, or 4 in fact would have kicked off the Löb reasoning (that is, that they are suitable as Löb sentences). Prove that they do in fact work!
What is the status of all of this stuff if you reject excluded middle? A whole lot of stuff concludes “not A, or not-not-A”, and deduces “not A, or A”. Does Löb’s theorem even hold without LEM, for example? (Not at all obvious to me that it should! How could I magic up a member of A given only an interpretation function SyntaxTree(A) → A?)
Interesting tidbits:
PA (if consistent) can never prove any statement to be unprovable! Indeed, if PA proves “provable(A) → False”, then by explosion, PA proves “provable(A) → A”, and hence by Löb PA proves A. Hence by one of the Hilbert-Bernays rules, PA proves provable(A), and hence PA proves False by modus ponens. So, for example, PA can’t even prove “not(provable(0=1))”! Though it can prove “provable(not(0=1))”. Which is very weird, and I still feel like we must have made some mistake!