The elimination of \textit{de re} formulas (Q1368754)

A \textit{de re} formula in modal logic is one which contains free variables within the scope of a modal operator (others are \textit{de dicto}). \textit{De re} modalities cause some people metaphysical anxiety. The axiom scheme \(\square\exists x\phi\supset \exists x\square\phi\) has seemed crucial for the elimination of \textit{de re} modalities, but the exact conditions under which its addition was required were unclear. Kaminsky defines (Df 5, p. 418) a modal logic S as closed under non-modal parametric substitutions just in case for each formula \(\phi\), each atomic formula \(P(x_1,\dots, x_n)\), and each formula \(\psi\) not containing modal operators, where \(\phi(P/\psi)\) is the result of substituting \(\psi\) for every occurrence of \(P\) in \(\phi\), then \(\text{S}\lvdash\phi(P/\psi)\). (Note that it is not required that \(x_1,\dots, x_n\) are the only free variables of \(\psi\).) Kaminsky then proves that for a modal logic S containing S5 closed under non-modal parametric substitutions in which \textit{de re} formulas are eliminable, \(\text{S}\lvdash \square\exists x\phi\supset \exists x\square \phi\). Skolemization, which allows explicit description of objects, over a modal logic results in a theory which is not a conservative extension of the original. It is shown that Skolemization over the modal logic T (or higher) is equivalent to adding the axiom scheme \(\square\exists x\phi\supset \exists x\square\phi\); for modal logics weaker than T, such as K, a modified result holds.