Overall I still have no understanding of theorem 5.1 though. I’m not terribly familiar with the field in general but the other proofs were still fairly straightforward, whereas this proof loses me in the first sentence, without referencing a result I can look up either inside or outside of the paper.
Were you OK with the proof of Theorem 4.1? To me, that and the proof of Theorem 5.1 are of equal difficulty. (Some of the other authors had more experience with Kripke semantics than I did, so they did most of the editing of those proofs. They work better with diagrams.)
orthonormal seems to believe that PrudentBot couldn’t be implemented for the LessWrong PD competition, although he did say with algorithmic proof search, would he change his opinion using Kripke semantics?
Yes; a PD tournament among modal sentences using the code Eliezer linked would be feasible and quite interesting!
I would say that “I am surprised that the bots have not been submitted to a PD tournament” but then I saw the paper was published in May and that’s less than 6 months ago so instead I’ll make the (silly, easy-to-self-fulfill) prediction that many or all of those bots will show up in the next PD tourney.
To the first point: I guess I’m not really comfortable with the proof of Theorem 4.1, per se, however the result seems incredibly intuitive to me. The choice of symbol/possible LaTeX error where one of the symbols is a square is confusing, and looking at it again three weeks later (I have not been on LW recently) I’ve forgotten too much of the notation to review it in depth in two to five minutes.
But I see Theorem 4.1 as the statement that “you can’t stop someone from punishing you for something unless you think at a higher level than they do” and I assume that there exists a proof of that statement, and that the proof provided is such a proof.
I see Theorem 5.1 as saying that some set is compact for some reason and that implies existence of something for some reason, but I don’t know why the thing is compact or why the desired object is the limit of the the things we constructed in the right way.
Although again it’s been a while so I could be misremembering here.
Were you OK with the proof of Theorem 4.1? To me, that and the proof of Theorem 5.1 are of equal difficulty. (Some of the other authors had more experience with Kripke semantics than I did, so they did most of the editing of those proofs. They work better with diagrams.)
Yes; a PD tournament among modal sentences using the code Eliezer linked would be feasible and quite interesting!
I would say that “I am surprised that the bots have not been submitted to a PD tournament” but then I saw the paper was published in May and that’s less than 6 months ago so instead I’ll make the (silly, easy-to-self-fulfill) prediction that many or all of those bots will show up in the next PD tourney.
To the first point: I guess I’m not really comfortable with the proof of Theorem 4.1, per se, however the result seems incredibly intuitive to me. The choice of symbol/possible LaTeX error where one of the symbols is a square is confusing, and looking at it again three weeks later (I have not been on LW recently) I’ve forgotten too much of the notation to review it in depth in two to five minutes.
But I see Theorem 4.1 as the statement that “you can’t stop someone from punishing you for something unless you think at a higher level than they do” and I assume that there exists a proof of that statement, and that the proof provided is such a proof.
I see Theorem 5.1 as saying that some set is compact for some reason and that implies existence of something for some reason, but I don’t know why the thing is compact or why the desired object is the limit of the the things we constructed in the right way.
Although again it’s been a while so I could be misremembering here.
The square is a symbol in Gödel-Löb provability logic.