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.

翻译：我们在经典一阶逻辑中引入了一个表示“作为论题”的句法模态算子 $\BOX$。该逻辑是R. Carnap关于模态性（即逻辑必然性）早期思想（J. Symb. Logic, 1946）\cite{Ca46}的一种现代实现。我们将其置于具有变域可能世界语义变体的现代量化模态逻辑框架内。我们使用一种正规形式证明了完备性，并证明了在典范框架中，所有极大一致集上的关系 $R = \{\langle \Gamma, \Delta \rangle : \forall A (\BOX A \in \Gamma \Longrightarrow A \in \Delta)\}$ 是一个全关系。$\BOX$ 算子的强度是模态逻辑 $\mathsf{S5}$ 的真扩张。利用完备性，我们证明了在任意赋值下 $\BOX A$ 在模型中的可满足性意味着 $A$ 是所构建逻辑的一个论题。因此，我们可以在句法上定义逻辑蕴涵和一致性。我们的语义在句法、语义及必然算子的解释方面均不同于S. Kripke的标准语义 \cite{Kr63}。与Kripke和Carnap的方法不同，我们允许自由变元，但我们的代入概念是非标准的（模态词内的变元不是自由的）。所有不含 $\BOX$ 的一阶逻辑论题都是可证的，Barcan公式及其逆公式亦然。我们特有的论题包括 \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)$。此外，若 $A$ 是不含 $\BOX$ 的公式，则有 $\POS \exists x A(x) \to \POS A(^{y}/_{x})$，以及 $\forall x \BOX A(x) \to \BOX A(^{y}/_{x})$。