First-order Logic with Being a Thesis Modal Operator

TL;DR

The paper develops a first-order modal logic with a thesis operator $\Box$ inspired by Carnap, embedding modality into a variable-domain, possible-worlds framework. A universal-class semantics and a canonical model yield a completeness result, showing that satisfiability of $\Box A$ corresponds to $A$ being a thesis, thereby enabling a syntactic notion of entailment and consistency beyond standard Kripke semantics. The system $\mathsf{FOL\Box}$ includes normality, BOX-specific axioms (e.g., $\Box A\rightarrow A$, $\Box A\rightarrow\forall x A$), nonstandard substitution rules, and Barcan-type principles for $\Box$-free formulas, extending $\mathsf{S5}$ in meaningful ways. The contributions provide Carnap-inspired formalization of being a thesis with a rigorous semantic and proof-theoretic foundation, offering a principled basis for reasoning about logical theses and their entailments in first-order settings.

Abstract

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 Γ, Δ\rangle : \forall A (\BOX A \in Γ\Longrightarrow A \in Δ)\}$, 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.

Theorems & Definitions (16)

• Theorem 1
• proof
• Lemma 1
• Lemma 2
• Lemma 3
• proof
• Lemma 4
• Lemma 5
• proof
• Theorem 2