Binding modalities (Q2804339)

The paper studies a modal logic \(\mathsf{FOS4}^*\) with binding modalities. If \(X\) denotes a finite set of individual variables and \(y\) is an individual variable, then \(Xy\) stands for \(X \cup \{y\}\) and it is assumed that \(y \notin X\). The logic \(\mathsf{FOS4}^*\) is axiomatized by the following schemas, where \(A\) and \(B\) are formulas, \(X\) is a set of individual variables, and \(y\) is an individual variable: NEWLINE\begin{itemize}NEWLINE\item[(A0)] classical axiom schemas of first-order logic NEWLINE\item[(A1)] \(\square_{Xy} A \to \square_XA\), \(y \notin\mathrm{FVar}(A)\) \item[(A2)] \(\square_X A \to \square_{Xy} A\) \item[(A3)] \(\square_X A \to\square_X \forall{x}A\), \(x \notin X\) NEWLINE\item[(B1)] \(\square_X (A \to B) \to (\square_X A \to \square_X B)\) NEWLINE\item[(B2)] \(\square_X A \to A\). NEWLINE\end{itemize}NEWLINEInference rules: NEWLINE\begin{itemize}NEWLINE\item[(R1)] \(A,A\to B \Rightarrow \;\vdash \;B\quad \text{modus ponens}\) NEWLINE\item[(R2)] \(A \Rightarrow \;\vdash \forall{x}A\quad \text{generalization}\) NEWLINE\item[(R3)] \(A \Rightarrow \;\vdash \square_\emptyset A\quad \text{necessitation}\).NEWLINE\end{itemize} NEWLINEA sequent calculus for \(\mathsf{FOS4}^*\) is constructed in Section 3, and the cut-elimination theorem is proven. The connections between \(\mathsf{FOS4}^*\) and \(\mathsf{FOS4}\) -- first order \(\mathsf{S4}\) -- are studied in Section 4. In particular, if \(A^*\) is a formula obtained from a given \(\mathsf{FOS4}\)-formula \(A\) by replacing all occurrences of subformulas of \(A\) of the form \(\square B\) by \(\square_X B\), where \(X = \mathrm{FVar}(B)\), we have NEWLINE\[NEWLINE\mathsf{FOS4} \vdash A \text{ if and only if } \mathsf{FOS4}^* \vdash A^*.NEWLINE\]NEWLINE A complete Kripke semantic for \(\mathsf{FOS4}^*\) is described in Section 5. And Section 6 is dedicated to proof that every formula \(A\) derived in \(\mathsf{FOS4}^*\) has a normal realization \(A^r\) and \(\mathsf{FOLP} \vdash A^r\), where \(\mathsf{FOLP}\) is the first order logic of proofs.