Public
I'm at the Machine Intelligence Research Institute, in Berkeley, helping Eliezer Yudkowsky and other folks think about Löb's theorem and its implications for artificial intelligence.
Löb's theorem is one of the most amazing results in mathematical logic. Roughly: take some axioms for arithmetic, like Peano Arithmetic, also known as 'PA'. You can encode statements about arithmetic as numbers and you can make up a formula P(n) that means "Peano arithmetic can prove statement n".
Now suppose you can prove, using Peano arithmetic, that for some statement, if this statement is provable then it's true. Then you can actually prove this statement using Peano arithmetic!
If you haven't seen Löb's theorem already, you'll need to read what I just said 5 times before it sinks in. Don't feel bad.
The little picture below may help. The smiley face is Peano arithmetic. The little speech balloon means "Peano arithmetic proves....". The little lightning bolt is some statement in arithmetic.
For Eliezer Yudkowsky and Marcello Herreshoff's cartoon proof of Löb's theorem, go here:
http://www.scribd.com/doc/4844564/Cartoon-Guide-to-Lobs-Theorem
This is a cartoon version of the standard proof of Löb's theorem. I have always found this proof hard to remember. I just discovered, by reading George Boolos' The Logic of Provability, that Kripke found a proof of Löb's theorem based on Gödel's 2nd incompleteness theorem. This one seems easier to understand. Unfortunately it's too large to fit into the margins of this G+ post.
You can see a sketchy version of it in the talk page here:
https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem
Someone should clean it up and put it on the actual Wikipedia article!
#logic
Löb's theorem is one of the most amazing results in mathematical logic. Roughly: take some axioms for arithmetic, like Peano Arithmetic, also known as 'PA'. You can encode statements about arithmetic as numbers and you can make up a formula P(n) that means "Peano arithmetic can prove statement n".
Now suppose you can prove, using Peano arithmetic, that for some statement, if this statement is provable then it's true. Then you can actually prove this statement using Peano arithmetic!
If you haven't seen Löb's theorem already, you'll need to read what I just said 5 times before it sinks in. Don't feel bad.
The little picture below may help. The smiley face is Peano arithmetic. The little speech balloon means "Peano arithmetic proves....". The little lightning bolt is some statement in arithmetic.
For Eliezer Yudkowsky and Marcello Herreshoff's cartoon proof of Löb's theorem, go here:
http://www.scribd.com/doc/4844564/Cartoon-Guide-to-Lobs-Theorem
This is a cartoon version of the standard proof of Löb's theorem. I have always found this proof hard to remember. I just discovered, by reading George Boolos' The Logic of Provability, that Kripke found a proof of Löb's theorem based on Gödel's 2nd incompleteness theorem. This one seems easier to understand. Unfortunately it's too large to fit into the margins of this G+ post.
You can see a sketchy version of it in the talk page here:
https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem
Someone should clean it up and put it on the actual Wikipedia article!
#logic
View 108 previous comments
+Lucius Meredith wrote: "the axiom |- []( []A => A ) => []A"
You probably realize this, but in Peano arithmetic, treating []A as an abbreviation in the way I described, this is a theorem: an internalized version of Löb's theorem.Dec 25, 2013
Ok, i believe i have found an investigation relevant to this discussion. There's a 2010 paper (http://www.helsinki.fi/~negri/selected_pub/dedthm.pdf) discussing the apparent failure of the deduction theorem for modal logics. They provide a proof of the deduction theorem for K (theorem 2, pg 10). Since GL is an extension of K with the axiom
|- []( []A => A ) => []A
it should follow that their proof of the deduction theorem holds for GL, and thus for at least one flavor of provability logic. That means, in particular, that we can derive
|- A => []A
Thus, with the deduction theorem in hand rule 2 is superfluous.
As for the use of category theory, and in particular, (co)monads to model modalities, this is the standard treatment of the linear modalities. See http://www.cs.man.ac.uk/~schalk/notes/llmodel.pdf
This suggests that the provability modality might be faithfully interpreted as a monad with some odd flavor of tensorial strength.Dec 25, 2013- +Lucius Meredith wrote: "This suggests that the provability modality might be faithfully interpreted as a monad with some odd flavor of tensorial strength."
I think that's a great idea to explore. Presumably it won't seem "odd" when we really understand it.Dec 25, 2013 - Thanks for all the info and input! Regarding your comment
"You probably realize this, but in Peano arithmetic, treating []A as an abbreviation in the way I described, this is a theorem: an internalized version of Löb's theorem."
It's only just dawning on me that Löb worked in a model, PA + a particular notion of provability, first. The theorem holds in the model. But, the presentation of GL, namely
K + |- []( []A => A ) => []A
is the abstract presentation of which the PA situation is a model. Sorry, i'm particularly slow at this stuff.
Note, if []( - ) is modeled as a monad, then []A => A says there's a way to extract A's out of the monad. That's particularly interesting to me because in the computational setting monads can be classified into three basic categories:
1) what goes in never comes out
2) what goes in sometimes comes out (data structures like option, list, ... )
3) things that go in are perfectly matched by something coming out (these correspond to linear data structures)
The axiom for Gödel-Löb modal logic appears to be saying something about what happens when you can take stuff out of the monad.Dec 25, 2013 
+Lucius Meredith Oh, bloody awful. In the modal logic paper you mentioned they claim "Necessitation can be applied only to derivations without assumptions."
I get that somewhat but looks I was wrong on assuming [] to wrap propositional formulas only.Dec 25, 2013- On further reflection the GL axiom appears to say something very much related to what i call "intuitionistic" monads. Monads like Option or List have an interesting property. The producer of an inhabitant of List[A], l1 : List[A], knows, with certainty, whether there's an A to be gotten out of the inhabitant, l1. A consumer of l1 cannot know, without opening the inhabitant, whether an inhabitant of A can be gotten out of l1. In short, the producer of a list knows whether the list is empty or not. The consumer of the list can't know without inspecting the list.
The axiom GL says that if it's provable that an A can be produced from the container, then A was in the container. In other words, if i can reach into the provability jar and pull out a fortune cookie, the fortune of which says i can reach into the provability jar and pull out an A, then i can reach into the provability jar and pull out an A.
This is a very nearly perfect characterization of how i think about "intuitionistic" monads.Dec 26, 2013
