2024/06/23 by Marcin Łyczak, Łyczak, Marcin
Computer Science · #Advanced Algebra and Logic #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge
paper · pdf · doi:10.48550/arxiv.2406.16133
openalex publication_date 2024/06/23 · openalex created_date 2024/06/27 · openalex updated_date 2026/07/28
We introduce syntactic modal operator \BOX for 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) \citeCa46. 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 = \⟨ Γ, Δ⟩ : ∀ A (\BOX A ∈ Γ\Longrightarrow A ∈ Δ)\, is a universal relation. The strength of the \BOX operator is a proper extension of modal logic 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 \citeKr63 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 → ∀ x A, ¬ \BOX (x = y), ¬ \BOX ¬ (x = y), ¬ \BOX P(x), ¬ \BOX ¬ P(x). We also have \POS ∃ x A(x) → \POS A(y/x), and ∀ x \BOX A(x) → \BOX A(y/x), if A is a \BOX-free formula.