Mike Carroll wrote: ... what happens if we add modal operators to the object language of ZFC (or NBG), and adjoin the S4 axioms as logical axioms? ... In fact, I have asked myself something quite similar, and am actively turning this into a fleshed-out research project. I have gotten so far as to determine that no one else has done this yet. Bob Lubarsky