First-order Logic with Being a Thesis Modal Operator

We introduce syntactic modal operator 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) {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 = \ Γ, Δ : ∀ A ( A ∈ Γ A ∈ Δ)\, is a universal relation. The strength of the operator is a proper extension of modal logic S5. Using completeness, we prove that satisfiability in a model of 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 {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 -free first-order theses are provable, as well as the Barcan formula and its converse. Our specific theses are [4] A → ∀ x A, (x = y), (x = y), P(x), P(x). We also have ∃ x A(x) → A(ʸ/ₓ), and ∀ x A(x) → A(ʸ/ₓ), if A is a -free formula.