[FOM] S4 + ZFC

[Michael Carroll]

The modal system S4 has been used meta-theoretically in the study of set 
theory and the independence proofs (Smullyan & Fitting, "Set Theory and the 
Continuum Hypothesis", for example). From a formal standpoint, it would then 
seem natural to ask: what happens if we add modal operators to the object 
language of ZFC (or NBG), and adjoin the S4 axioms as logical axioms? Do the 
incompleteness proofs remain unaffected by this change?

But I haven't been able to find any research along these lines. I wonder 
whether it has been pursued and found fruitless, or hasn't been pursued for 
sound mathematical reasons, or merely hasn't been pursued due to 
philosophical preconceptions ("All truths of set theory are necessary 
truths, so modal operators have no place", etc.). This question must have 
occurred before to brighter minds than mine. Perhaps I haven't looked in the 
right place for an answer?

Mike Carroll