Jonathan’s joke raises the interesting question of whether there are any everyday interpretations of the box (written here as L) such that L(Lp -> p) -> Lp holds, apart of course for the interpretations to do with provability in extensions of Peano arithmetic. Any suggestions?