I’m coming to this quite late, and these are the notes I wrote as I read the paper, before reading the comments, followed by my notes in the comments.
Has any of the (roughest) analysis been done to bound proving time for PrudentBot? It should be fairly trivial to get very bad bounds and if those are not so bad that seems like a worthwhile thing to know (although what does “not so bad” really mean I guess is a problem.)
Is there a good (easy) reference for the statement about quining in PA (on page 6 below CliqueBot)?
Under modal agents Kleene’s recursion algorithm is mentioned; should probably be mentioned at first use rather than second?
The proof of theorem 5.1 is losing me where other proofs didn’t; I don’t understand how minimality of modal rank gives other results.
Reading the comments to answer some of my own questions: 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?
Vaniver’s comment seems like a promising way of thinking about how to identify TrollBots. Or at least, the most promising thing about it I’ve seen; has this been pursued any further?
Perhaps as a possibly-answerable question: call a bot a troll if it can’t survive in a population with only itself or only itself and CB and DB (since these are the simplest bots to describe).
I’ll also note that PseudoTitForTatBot seems like an interesting basic candidate to play against; or say “TimeLimitTitForTatBot” which plays tit for tat until the time limit is near, so no single N can always fool it. Is there a way to (modally; if that is the right word for not-by-quoting-source-code) defeat TLTFTB?
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. Was this written by a different person/at a different time from the rest of the paper? The second sentence is less bad than the first but still worse than the entire rest of the paper.
Let me rephrase my question, then, because the diagonal lemma seems clear enough to me. What is a good definition of quining? The term isn’t used at all either in the article you linked or it the page on self-reference, which surprised me.
a computer program which takes no input and produces a copy of its own source code as its only output.
If you understand how to write a quine and you understand how the diagonal lemma works, you will find that the two concepts are basically the same thing. “Quine” is more of a computer science term than a mathematical logic term, so not all expositions of Gödel’s incompleteness theorem will mention “quining”.
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.
I’m coming to this quite late, and these are the notes I wrote as I read the paper, before reading the comments, followed by my notes in the comments.
Has any of the (roughest) analysis been done to bound proving time for PrudentBot? It should be fairly trivial to get very bad bounds and if those are not so bad that seems like a worthwhile thing to know (although what does “not so bad” really mean I guess is a problem.)
Is there a good (easy) reference for the statement about quining in PA (on page 6 below CliqueBot)? Under modal agents Kleene’s recursion algorithm is mentioned; should probably be mentioned at first use rather than second?
The proof of theorem 5.1 is losing me where other proofs didn’t; I don’t understand how minimality of modal rank gives other results.
Reading the comments to answer some of my own questions: 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?
Vaniver’s comment seems like a promising way of thinking about how to identify TrollBots. Or at least, the most promising thing about it I’ve seen; has this been pursued any further? Perhaps as a possibly-answerable question: call a bot a troll if it can’t survive in a population with only itself or only itself and CB and DB (since these are the simplest bots to describe). I’ll also note that PseudoTitForTatBot seems like an interesting basic candidate to play against; or say “TimeLimitTitForTatBot” which plays tit for tat until the time limit is near, so no single N can always fool it. Is there a way to (modally; if that is the right word for not-by-quoting-source-code) defeat TLTFTB?
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. Was this written by a different person/at a different time from the rest of the paper? The second sentence is less bad than the first but still worse than the entire rest of the paper.
Haskell code to run PrudentBot (quickly) and the other bots (also quickly) can be found on github here:
https://github.com/klao/provability/blob/master/modal.hs
On quining in arithmetic, see any exposition on Gödel’s First Incompleteness Theorem and the Wikipedia article on the diagonal lemma.
I am unsure which of my questions this is supposed to answer, although perhaps that will become clear on reading the wikipedia article.
That was a response to
Let me rephrase my question, then, because the diagonal lemma seems clear enough to me. What is a good definition of quining? The term isn’t used at all either in the article you linked or it the page on self-reference, which surprised me.
Oh! Ok, a quine is
If you understand how to write a quine and you understand how the diagonal lemma works, you will find that the two concepts are basically the same thing. “Quine” is more of a computer science term than a mathematical logic term, so not all expositions of Gödel’s incompleteness theorem will mention “quining”.
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.