First-order Logic with Being a Thesis Modal Operator

We introduce syntactic modal operator $\BOX$ for \textit{being a thesis} into first-order logic. This logic is a modern realization of R. Carnap's old ideas on modality, as logical necessity (J. Symb. Logic, 1946) \cite{Ca46}. We place it within the modern framework of quantified modal logic with a variant of possible world semantics with variable domains. We prove completeness using a kind of normal form and show that in the canonical frame, the relation on all maximal consistent sets, $R = \{\langle \Gamma, \Delta \rangle : \forall A (\BOX A \in \Gamma \Longrightarrow A \in \Delta)\}$, is a universal relation. The strength of the $\BOX$ operator is a proper extension of modal logic $\mathsf{S5}$. Using completeness, we prove that satisfiability in a model of $\BOX A$ under arbitrary valuation implies that $A$ is a thesis of formulated logic. So we can syntactically define logical entailment and consistency. Our semantics differ from S. Kripke's standard one \cite{Kr63} in syntax, semantics, and interpretation of the necessity operator. We also have free variables, contrary to Kripke's and Carnap's approaches, but our notion of substitution is non-standard (variables inside modalities are not free). All $\BOX$-free first-order theses are provable, as well as the Barcan formula and its converse. Our specific theses are \linebreak[4] $\BOX A \to \forall x A$, $\neg \BOX (x = y)$, $\neg \BOX \neg (x = y)$, $\neg \BOX P(x)$, $\neg \BOX \neg P(x)$. We also have $\POS \exists x A(x) \to \POS A(^{y}/_{x})$, and $\forall x \BOX A(x) \to \BOX A(^{y}/_{x})$, if $A$ is a $\BOX$-free formula.