First-Order Fischer Servi Logic

TL;DR

This work establishes the completeness of a first-order intuitionistic analogue of Fischer Servi logic, $\mathsf{FOFS}$, with respect to its birelational semantics by introducing a trace model that mimics canonical-model arguments and proving a truth lemma. The trace model, together with saturation arguments and modal-chain extensions, yields strong completeness for $\mathsf{FOFS}$ and extends to five related first-order Fischer Servi logics, including $\mathsf{FOFS}$ variants corresponding to $\mathsf{FSS4}$. The authors also analyze extensions by modal axioms (D, T, 4, S4) and the necessity of identity and distinctness (NI, ND), providing soundness and completeness results under appropriate frame conditions. The paper highlights a robust, expanding-domain, birelational framework for first-order intuitionistic modal logics and outlines future work on applying trace-model techniques to more complex systems such as $\mathsf{MIPC}$. Overall, the trace-model approach offers a powerful method for proving completeness in rich first-order modal logics with explicit domain dynamics.

Abstract

We prove the completeness of a first-order analogue of the Fischer Servi logic $\mathsf{FS}$ with respect to its expected birelational semantics. To this end we introduce the notion of the $\textit{trace model}$ and, much like in a canonical model argument, prove a truth lemma. We conclude by examining a number of other first-order Fischer Servi logics, including the first-order analogue of $\mathsf{FSS4}$, whose completeness can be similarly proved.

Figures (8)

• Figure 1: $c,c_1,c_2\in \sigma^\nu$, $x\in V$, and $\varphi$ and $\psi$ are sentences unless otherwise noted
• Figure 2: The Fischer Servi frame conditions from \ref{['fsframe']} where blue arrows indicate the modal relation, black arrows the intuitionistic relation, and dotted arrows and hollow points existence claims
• Figure 3: A diagram of \ref{['fc2']}
• Figure 4: A schematic of the construction in the proof of \ref{['getdschain']}
• Figure 5: Examples of Ferrers sets where $(0,0)$ is the bottom left point, the first coordinate tracks horizontally, and the second vertically

Theorems & Definitions (78)

• Definition 2.1
• Definition 2.2
• Definition 2.3
• Lemma 2.4
• proof
• Lemma 2.5
• proof
• Lemma 2.6
• proof
• Proposition 2.7