Notes/blog posts on two recent MIRI papers
I've been learning math lately; specifically I've been reading MIRI's recent research preprints and the prerequisite material. In order to actually learn math, I typically have to write it down again, usually with more details and context. I started a blog to make my notes on these papers public, and I think they're of high enough quality that I ought to share them here. Note: my use of the pronoun "we" is instilled habit; I am not claiming to have helped develop the core ideas herein. * Löb's Theorem and the Prisoner's Dilemma is an account of the LaVictoire et al paper Robust Cooperation in the Prisoner's Dilemma. * Details in Provability Logic is a technical followup to the above, which goes into the details of modal logic needed for the LaVictoire et al paper; namely the normal form theorem, the fixed point theorem, and the decidability of GL via Kripke semantics. * Definability of Truth in Probabilistic Logic goes through the Christiano et al paper of the same name. It's a little rougher around the edges on account of being the first blog post I ever wrote (and being produced more hastily than the other two). I note that the construction doesn't truly require the Axiom of Choice.
Thanks for pointing that out. My feeling is still "well yes, that's technically true, but it still seems unnatural, and explosion is still the odd axiom out".
Coq, for example, allows empty case expressions (for empty types), and I expect that other languages which double as proof assistants would support them as well... for the very purpose of satisfying explosion. General purpose languages like Haskell (and I just checked OCaml too) can seemingly overlook explosion/empty cases with few if any practical problems.