2 First-order relevant modal logics

Here, we present the first-order relevant modal logics which serve as a foundation for the remainder of the paper. The logics and semantics defined here are essentially those found in [Reference Ferenz5, Reference Ferenz6], which combines and furthers the Mares–Goldblatt interpretation of quantifiers (see, e.g., [Reference Goldblatt8, Reference Mares and Goldblatt12]) and Seki’s general frame semantics for regular relevant model logics (see, e.g., [Reference Seki20, Reference Seki21]).Footnote ¹

For now, we simplify the matter at hand by presenting a constant domain semantics—indeed, a single universal domain—with no existence predicates. Therefore the quantifiers are to be considered possibilist, although the actualist, variable domain semantics is obtainable, through the modifications detailed in [Reference Mares11]. An agent may claim to have beliefs about possible situations with a different set of objects composing it; that is, objects that either do not exist or have no counterparts in the agent’s world. Nonetheless, we will sideline these kinds of philosophical issues for the time being.

The language of the first-order substructural epistemic logic $\textbf {QBM.C}_{\Box \Box _{L}}$ , hereafter just $\textbf {QBM.C}$ , will be built up from a set of symbols that can be divided as follows:

1. 1. a denumerable set of variables $Var = \{x_0, x_1, \dots \}$ ;

2. 2. an at most denumerable signature $\mathbb {S}$ consisting of:

   1. (a) a set of constant symbols $Con^{\mathbb {S}} = \{c_0, c_1, \dots \}$ ;

   2. (b) a non-empty set of predicate symbols $Pred^{\mathbb {S}}$ ;

3. 3. constant symbol ${\mkern 1mu\boldsymbol t}$ ;

4. 4. binary operators $\land , \lor , \rightarrow , \circ , \leftarrow $ ;

5. 5. unary operators $\neg , \Box , \Box _{L}$ ;

6. 6. quantifier symbol $\forall $ , $\exists $ .

Each n-ary predicate symbol will be written as $P^n_k$ (with identifying subscript k often omitted), and the set of n-ary predicates shall be written as $Pred^n \subseteq Pred^{\mathbb {S}}$ .

For a signature ${\mathbb {S}}$ , the set of terms of $\textbf {QBM.C}$ is $Term^{\mathbb {S}}_{\textbf {QBM.C}} = Con^{\mathbb {S}} \cup Var$ , and $\tau $ (often with subscripts) will always denote a term. For the remainder of the paper, it is often the case that a signature will implicitly be taken for granted, or stated explicitly. Hereafter we will drop the “ $\mathbb {S}$ ” in notation.

Officially, we take the set of variables to be ordered, as in $x_1, \dots , x_n, \dots $ . Then, given a set of U of individuals, a variable assignment is a denumerable sequence of individuals, $f \in U^\omega $ , such that the nth element in the sequence (written as $fn$ ) is the individual assigned to the n-th variable $x_n$ . Given a variable assignment f, an x-variant of f differs from f in at most the assignment to the variable x. The set of all x-variants of f will be denoted $xf$ . We will write $f[j/n]$ (or $f[j/x_n]$ ), with $j \in U$ to denote the result of changing the n-th element of f with the individual j.

Definition 2.1 (Language $\mathfrak {L}_{QBM.C}$ ).

The basic first-order substructural language $\mathfrak {L}_{QBM.C}$ , or well-formed formulas (hereby wff) is defined in BNF as follows:

$$ \begin{align*} \phi ::= P^n (\tau_1, \dots, \tau_n) |{\mkern1mu\boldsymbol t}|\neg \phi|\Box \phi|\Box_{L} \phi|\phi \land \phi|\phi \lor \phi|\phi \rightarrow \phi | \phi \circ \phi | \phi \leftarrow \phi | \forall x \phi| \exists x \phi. \end{align*} $$

In terms of binding strength, for the purposes of omitting parentheses, we assume that unary connectives and quantifiers bind the strongest (and equally so). We assume the left and right arrow bind weaker than fusion, which itself binds weaker than the extensional conjunction and disjunction.

We shall write $\mathcal {A}[\tau /x]$ for the result of replacing every free occurrence of x in $\mathcal {A}$ with the term $\tau $ . Similarly, we will use $\mathcal {A}[\tau _0/v_0, \dots , \tau _n/v_n]$ for the result of simultaneously replacing $v_0$ through $v_n$ with $\tau _0$ through $\tau _n$ respectively. A variable is said to be bound in a formula $\mathcal {A}$ if it (i) is the instance x in a quantifier $\exists x$ or $\forall x$ , or (ii) is an instance of x that occurs within the scope of either $\exists x$ or $\forall x$ . Non-bound variables are said to be free. A term $\tau $ is free for (or freely substitutable for) a variable x in $\mathcal {A}$ if $\tau $ does not become bound in the resulting formula $\mathcal {A}[\tau /x]$ .

Note the inclusion of $\leftarrow $ and $\circ $ . This inclusion is not only formally interesting—e.g., see Section 4, where additional frame conditions for classical possible worlds must be satisfied—but also enables additional expressive power in terms of formulating the beliefs of an agent. With fusion, for example, we are able to represent the difference between an agent merely believing $(\mathcal {A} \rightarrow \mathcal {B})\wedge \mathcal {A} $ (which does not imply $\mathcal {B}$ in BM), and believing $(\mathcal {A} \rightarrow \mathcal {B})\circ \mathcal {A} $ (which does imply $\mathcal {B}$ in BM) The latter is a type of conjunction which “applies” modus ponens in this case. We can thus represent the nuanced difference between believing a set of sentences in a simple way and believing a set of sentences in way that implies belief of the relevant consequences of such a set. One may come to believe that $\mathcal {A} \wedge \mathcal {B}$ is true by believing each conjunct individually, but yet one need not have additionally entertained combining these beliefs to obtain their joint logical consequences. For left-implication, the case only arises when $\circ $ is not commutative (otherwise $\leftarrow $ is just $\rightarrow $ ). With distinct left-implication, we can represent (epistemic states regarding) implications corresponding to conjoining premises in different orders. I emphasize again that the project here is a general framework: for particular applications one needs to assume the right properties for both these connectives, implication, and the epistemic modality.

The frames and models are defined as in [Reference Ferenz6], following Mares and Goldblatt’s interpretation of quantifiers in the first-order extensions of the relevant logic R.

Definition 2.2 (Base First-Order Frames).

A Base First-Order Frame is a tuple

$$ \begin{align*} F &= \langle K, N, R, *, S_{\Box}, S_{\Box_{L}}, U, Prop, PropFun \rangle, \end{align*} $$

where $N \subseteq K \neq \emptyset $ ; $R \subseteq K^3$ ; $*: K \rightarrow K$ ; $S_{\Box } \subseteq K^2$ ; $S_{\Box _{L}} \subseteq K^2$ ; U is a non-empty set of individuals; and, defining the “upsets” as $\mathscr {P}(K)^{\uparrow } = \{X \in \mathscr {P}(K) : \forall a, b, \in K (a \in X \ \& \ a \leq b)\Rightarrow b \in X\}$ , with $a \leq b =_{df} \exists x \in N (Rxab)$ we have that $ Prop \subseteq \mathscr {P}(K)^{\uparrow }$ , $PropFun \subseteq \{\phi : U^\omega \longrightarrow Prop\}$ , and the following conditions hold:

1. (c1) $\leq $ is reflexive and transitive.

2. (c2) $N \in Prop$ .

3. (c3) $Rabc$ , $a' \leq a$ , $b' \leq b$ & $c \leq c'$ imply $Ra'b'c'$ .

4. (c4) $a \leq b$ implies $b^* \leq a^*$ .

5. (c5) $S_{\Box }bc$ and $a \leq b$ imply $S_{\Box }ac$ .

6. (c6) $S_{\Box _{L}}bc$ and $a \leq b$ imply $S_{\Box _{L}}ac$ .

7. (c7) $Prop$ is closed under $\cap , \cup , \neg , \Box , \Box _L, \rightarrow , \circ , \leftarrow $ where:

   1. (a) $\neg X=\{a\in K: \alpha ^*\not \in X\}$ .

   2. (b) $\Box X = \{a \in K : \forall b (S_\Box )ab \Rightarrow b \in X \}$ .

   3. (c) $\Box _{L} X = \{a \in K : \forall b (S_{\Box _{L}})ab \Rightarrow b \in X \}$ .

   4. (d) $X\rightarrow Y=\{a \in K : \forall b, c \in K (Rabc \ \& \ b \in X \Rightarrow c \in Y)\}$ .

   5. (e) $X\circ Y=\{a \in K : \exists b, c \in K (Rbca \ \& \ b \in X \ \& \ c \in Y )\}$ .

   6. (f) $X\leftarrow Y=\{a \in K : \forall b, c \in K (Rbac \ \& \ b \in X \Rightarrow c \in Y )\}$ .

8. (c8) $\phi _N \in Prop$ (where $\phi _N f = N$ , for every $f \in U^\omega $ ).

9. (c9) $PropFun$ is closed under $\cap , \cup , \neg , \Box , \Box _L,\rightarrow , \circ , \leftarrow $ where for all $f \in U^\omega $ , every $\phi , \psi \in PropFun$ :

   1. (a) $(\oplus \phi ) f = \oplus (\phi f)$ , for each $\oplus \in \{\neg , \Box , \Box _L\}$ .

   2. (b) $( \phi \otimes \psi ) f = \phi f \otimes \psi f$ , for each $\otimes \in \{\cap , \cup , \rightarrow , \circ , \leftarrow \}$ .

10. (c10) $PropFun$ is closed under $\forall _n$ and $\exists _n$ , for every $n \in \omega $ , where:

    1. (a) .

    2. (b) $(\exists _n\phi )f=\underset {g \in x_nf}{\bigsqcup }\phi g=\bigcap \{X\in Prop\mid \underset {g \in x_nf}{\bigcup }\phi g\subseteq X\}$ .

A frame is called full when $Prop$ is the set of every hereditary subset of K, and $PropFun$ contains every function from $U^\omega $ to $Prop$ .

Although the valuation function is officially extended in terms of propositional functions, we can define a relation $\vDash $ such that $a, f \vDash \mathcal {A}$ exactly when $a \in |\mathcal {A}|f$ . See [Reference Ferenz6] and [Reference Mares and Goldblatt12] for a list with the conditions for each formula shape.

A formula is satisfied by a variable assignment f in a model $\mathfrak {M}$ when $N \subseteq |\mathcal {A}|f$ . A formula is valid in a model $\mathfrak {M}$ when it is satisfied by every variable assignment in that model; valid in a frame when it is valid in every model based on that frame; valid in a class of frames when it is valid in every frame in that class.

The proof of this lemma is a standard induction on the complexity of formulas, the interesting cases being negation, and the modalities. Negation is given by condition (c4), and modalities by (c5) and (c6).

The proof of this lemma is as usual, using the hereditary lemma.

3 Axiomatization

Definition 3.8. We write a formula with a variable superscript to indicate that the variable does not occur free in the formula—e.g., x does not occur free in $\mathcal {A}^x$ . We use $\Rrightarrow $ as a separator for rules of proof: $\mathcal {A}_0,\dots , \mathcal {A}_n\Rrightarrow \mathcal {B}$ should be understood to mean “if $\mathcal {A}_0,\dots , \mathcal {A}_n$ are all theorems, then so is $\mathcal {B}$ ”.

The following axiom schemes and rules schemes generate the logic $\textbf {QBM.C}$ :

For (1), the proof is left to the reader, and uses fusion. Similarly, (2) follows by using left arrow and existential introduction. (RGC1) and (RGC2) follow from similar arguments to those in [Reference Mares and Goldblatt12].

Proposition 3.10. The following are theorems of QB.C (defined below), but not theorems of $\textbf {QBM.C}$ :

$$ \begin{align*} &(Dual1)\ \neg \forall x \neg \mathcal{A} \leftrightarrow \exists x \mathcal{A},\quad &(Dual3)\ \neg \forall x \mathcal{A} \leftrightarrow \exists x \neg \mathcal{A}, \\ &(Dual2)\ \neg \exists x \neg \mathcal{A} \leftrightarrow \forall x \mathcal{A},\quad &(Dual4)\ \neg \exists x \mathcal{A} \leftrightarrow \forall x \neg \mathcal{A}. \end{align*} $$

3.1 Extensions

An important class of extensions of the base logic add extensional confinement axioms. In the presence of a weak negation without double negation equivalence, the following axioms are not equivalent:

1. (EC1) $\forall x(\mathcal {A}\lor \mathcal {B}^x)\rightarrow \forall x\mathcal {A}\lor \mathcal {B}^x$ .

2. (EC2) $ \mathcal {A}^x \wedge \exists x \mathcal {B} \rightarrow \exists x (\mathcal {A}^x \wedge \mathcal {B})$ .

However, once we add double negation introduction and elimination, they are interderivable in any logic extending $\textbf {QBM.C}$ . These axioms are required to capture a certain classicality of the quantifiers. Furthermore, these axioms are the reasons for employing admissible propositional functions [Reference Goldblatt8, Reference Mares and Goldblatt12].

Definition 3.12. The logic $\textbf {BMQ.C}$ is the base logic $\textbf {QBM.C} +$ (EC1) $+$ (EC2).

The next lemma can be stated in a more fine-grained manner, separating (EC1) from (EC2), and vice versa, but we state it coarsely as follows.

Lemma 3.13. $\textbf {BMQ.C}$ is sound and complete with respect to the class of all $\textbf {QBM.C}$ -models that satisfy (cEC1) and (cEC2), where the latter as defined as follows: For every $\phi \in PropFun$ , $X, Y \in Prop$ , $n \in \omega $ , and $f \in U^{\omega }$ .

$$ \begin{align*} &\text{(cEC1) } \ \ \ X-Y \subseteq \underset{j \in U}{\bigcap}\phi (f[j/n]) \text{ only if } X-Y \subseteq (\forall_n \phi)f. &\text{ } \\ &\text{(cEC2) }\ \ \ \underset{j \in U}{\bigcup}\phi (f[j/n]) \subseteq X \cup \overline{Y} \text{ only if } |\exists_n \phi|f \subseteq X \cup \overline{Y}. \end{align*} $$

Although $\textbf {QBM.C}$ and $\textbf {BMQ.C}$ are our foundational logics, we will define a number of common propositional relevant logics and their extensions in the relevant logic literature using the following list of axioms and rules:

1. (DNE) $\mathcal {A} \leftrightarrow \neg \neg \mathcal {A}$ .

2. (Cont) $(\mathcal {A} \rightarrow \mathcal {B}) \rightarrow (\neg \mathcal {B} \rightarrow \neg \mathcal {A})$ .

3. (RCM) $\mathcal {A} \rightarrow \neg \mathcal {A} \Rrightarrow \neg \mathcal {A}$ .

4. (B) $(\mathcal {A} \rightarrow \mathcal {B}) \rightarrow ((\mathcal {C} \rightarrow \mathcal {A})\rightarrow (\mathcal {C} \rightarrow \mathcal {B})) $ .

5. (B′) $(\mathcal {A} \rightarrow \mathcal {B}) \rightarrow ((\mathcal {B} \rightarrow \mathcal {C})\rightarrow (\mathcal {A} \rightarrow \mathcal {C})) $ .

6. (W) $(\mathcal {A} \rightarrow (\mathcal {A} \rightarrow \mathcal {B}))\rightarrow (\mathcal {A} \rightarrow \mathcal {B})$ .

7. (C) $ (\mathcal {A} \rightarrow (\mathcal {B} \rightarrow \mathcal {C})) \rightarrow (\mathcal {B} \rightarrow (\mathcal {A} \rightarrow \mathcal {C}))$ .

The relevant logic BM (or rather BM with $\circ , \leftarrow , {\mkern 1mu\boldsymbol t}$ ) is defined (in the appropriate non-modal propositional language) as $\textbf {QBM.C}$ , but without the axioms and rules containing modalities and quantifiers. Some non-modal propositional extensions of BM (with $\circ , \leftarrow , {\mkern 1mu\boldsymbol t}$ ) are captured by the following list:

1. 1. B = BM + (DNE).

2. 2. DW = B + (Cont).

3. 3. T = DW + (RCM) + (B) + (B′) + (W).

4. 4. R = T + (C).

Where $\mathbb {L}$ is a propositional extension of the relevant logic $\textbf {B}$ , Q $\mathbb {L}.\textbf {C}$ and $\mathbb {L}$ Q.C denote the extensions of $\textbf {QBM.C}$ and $\textbf {BMQ.C}$ , respectively, by the same additional axiom and rule schemes.

The modal logic $\textbf {C}$ denotes the least regular modal logic, over some propositional logic. Namely, the result of adding ( $\Box \land $ ) and (R $\Box $ M). The extensions in the modal fragment of a regular modal logic are defined using the following, where $\Diamond \mathcal {A} =_{df} \neg \Box \neg \mathcal {A}$ :Footnote ³

A more complete list (in the background of relevant logics) can be found in several places, including [Reference Seki20, Reference Seki21]. It is assumed that the reader is familiar with the naming conventions for modal logics extending K, so we only offer the following list:

1. 1. K = C + ( $K_{\Box }$ ) + (RN).

2. 2. S4 = K + (T) + (4).

Note, importantly, that here we use these names only to refer to the set of modal axiom schemes, and not to a full propositional modal logic. That is, the name only refers to the set of axiom schemes with modal operators in their shape. For example, (BD) and (DB) are theorems of the K-ish extension of classical logic, but not of the K-ish extension of relevant logics.

Quantified and modal logics are obtained by taking a quantified relevant logic $\mathbb {L}$ and extending it with a set of modal axiom schemes. Where $\mathbb {M}$ is the name of a set of modal axiom schemes, the logic $\mathbb {L}.\mathbb {M}$ is the result of simply adding the modal axiom schemes to the axiomatization of $\mathbb {L}$ . In many cases this axiomatization will lack (BD) and (DB), making the modal fragment lack a certain “classicality”. The dot is removed when, in the terms of [Reference Ferenz6], the logic becomes sufficiently classical, in that it has both the duality of the modalities and (BD) and (DB) as theorem schemes.Footnote ⁴

A final note on these axiomatizations is that they make essential use of $\circ , \leftarrow $ , and ${\mkern 1mu\boldsymbol t}$ . There are quantified relevant logics where the addition these connectives does not result in a conservative extension—e.g., see the logic QB $^{-}$ in [Reference Tedder and Ferenz24] for a first-order relevant logic which is not conservatively extended by either $\circ $ or $\leftarrow $ .

4 Epistemic models with worlds

A possible world is a point in the model where the intensional connectives behave classically: that is, extensionally. Sedlár [Reference Sedlár17] and Sedlár and Vigiani [Reference Sedlár and Vigiani18] define worlds such that the negation and implication of the relevant fragment are truth-functional at a world. We will do the same by ensuring that the left-implication and fusion are also classical. However, for the first-order machinery, there are many choices to make in terms of “classicality”.

First, it is likely that a world should satisfy (EC1) and (EC2), as these axioms are decidedly classical. After that, we have options. Should we enforce the Tarskian truth condition, which can be succinctly paraphrased by and $\underset {i \in I}{\bigcup } X_i = \underset {i \in I}{\bigsqcup } X_i$ ? If we do, then worlds must be $\omega $ -complete: that is, a world-variable assignment pair cannot satisfy all instances of a universally quantified formula $\forall x \mathcal {A}$ without also satisfying $\forall x \mathcal {A}$ itself. Indeed, we suppose (and might even go as far as to claim) that there is good reason to believe that a robust possible world is $\omega $ -complete. However, issues of completeness lie in the direction of $\omega $ -complete possible worlds. So for the time being we do not assume this strong condition on possible worlds. The reader may look forward to Section 7, where this issue is highlighted, and where we develop the relation to Fine’s incompleteness results for constant domain (non-general frame) RQ.Footnote ⁶

Note that (EC1) and (EC2) are not sufficient to get a fully classical behavior of the quantifiers. For example, some formulas needed for prenex normal form are invalid. [Reference Meyer14] shows the following “lemons” are (and should be) invalid in any first-order relevant logic worth its weight in salt:

These formulas could be upgraded to axiom schemes, nonetheless invalid, simply by replacing ‘p’ with $\mathcal {B}^x$ uniformly. The remainder of the usual formulas required for prenex normal form are valid, including $\forall x (p \rightarrow Fx) \leftrightarrow (p \rightarrow \forall x Fx)$ [Reference Meyer14, p. 279].

Note that the possible worlds are all logically normal points with respect to the underlying relevant (subclassical) logic. This holds in the canonical model, but a word or two is in order. At a world the conditional is made truth-functional, and there is no way to falsify (using two truth values) a truth functional conditional corresponding to a relevant conditional, provided the relevant logic is a sublogic of classical logic. Thus, the worlds should make true at least all of the conditional theorems of the relevant logic. And so, by extension, all worlds should be logically normal points in the frame.

Unlike in [Reference Sedlár and Vigiani18], our inclusion of N and requirement that N is “seen in full by W” means that we do not need to consider variants of the usual frame conditions for extensions. In Table 1, we have provided a small list of axioms and rules together with their corresponding frame conditions. (That is, a modular frame-correspondence in the background of $\textbf {QBM.C}$ .) The conditions were shortened by adopting the following conventions of notation:

$$ \begin{align*} R^2abcd &=_{df} \exists x (Rabx \ \& \ Rxcd).\\ S_\Box^2ab &=_{df} \exists x(S_\Box ax \ \& \ S_\Box xb).\\ Ra(Rbc)d &=_{df} \exists x(Raxd \ \& \ Rbcx).\\ S_\Diamond ab &=_{df} S_\Box a^*b^*. \end{align*} $$

Note that $\Diamond $ is always assumed here to be the negation-dual of $\Box $ by being a notational variant. This is even despite the absence of double negation introduction/elimination.Footnote ⁷ The conditions for (BD) and (DB) are drawn directly from [Reference Ferenz6], which is a generalization of the condition given by Mares and Meyer [Reference Mares and Meyer13].

Table 1 Frame correspondence for extensions.

For some further extensions, the reader is directed to [Reference Ferenz5, Reference Ferenz6] for the quantified modal setting, [Reference Routley, Plumwood, Meyer and Brady16] for the proportional relevant setting, and [Reference Seki20, Reference Seki21] for propositional modal relevant setting.

Proof. The proof is as in [Reference Sedlár and Vigiani18]. Here we add states $0, 1$ and world w to the model $\mathfrak {M}$ , and show the resulting model is a W-model in which $\Box _{L} \mathcal {A}$ is not valid.

Suppose we have an $\mathbb {L}$ -model $\mathfrak {M}$ based on the frame

$$\begin{align*}F = \langle K', N', R', *', S^{\prime}_{\Box}, S^{\prime}_{\Box_{L}}, U, Prop', PropFun' \rangle \end{align*}$$

which invalidates $\mathcal {A}$ . Construct the new model as follows. First, define the W-frame $\mathbb {F}$ as follows:

1. 1. $W = W' \cup \{ 1, 0, w\}$ .

2. 2. $N = N' \cup \{ 1, w\}$ .

3. 3. $R = R' \cup \{ (w,w,w), (1,1,1), (1,0,0)\}$

   $\cup \{ (w,a,1) |a \in W \} \cup \{ (w,0,a) | \forall a \in W \}$

   $ \cup \{ (0,a,b), (a,0,b), (a,b,1) | a, b \in W\}$ .Footnote ⁸

4. 4. $* = *' \cup \{(w,w), (0,1), (1,0)\}$ .

5. 5. $S_{\Box } = S^{\prime }_{\Box } \cup \{ (w,w), (a,1), (0,b) | a, b \in W \}$ .

6. 6. $S_{\Box _{L}} = S^{\prime }_{\Box _{L}} \cup \{ (w,w), (a,1), (0,b) | a, b \in W \} \cup \{ (w,a) | a \in N\}$ .

7. 7. $U=U$ .

8. 8. For each $X' \in Prop'$ , if $N' \subseteq X'$ , add $X = X' \cup \{1,w\}$ to $Prop$ , and if $N' \not \subseteq X'$ , add $X = X' \cup \{1\}$ to $Prop$ .

9. Given a $X' \in Prop'$ , let $h(X')$ be the corresponding $X \in Prop$ .

10. 9. For each $\phi ' \in PropFun'$ , add the propositional function $\phi $ defined by, for all $f \in U^\omega $ , $\phi f = h(\phi ' f)$ .

First we show that this frame is an $\mathbb {L}$ -frame, then that it is a bounded frame, then that it is a W-frame.

As defined, (c1), (c2), (c4), (c5), (c6), and (c8) are straightforward. For (c3), adding $(0,a,b), (a,0,b), (a,b,1)$ ensures the tonicity w.r.t. $1$ and $0$ , and indirectly for $w$ , for which $0 \leq w \leq 1$ and $w \leq w$ are the only relevant orderings.

For (c7), first note that every element of $Prop$ is an upset. We show only the case for $X\rightarrow Y$ , as the rest are similar. Suppose that $X, Y \in Prop$ . We show that $X \rightarrow Y = h((X\rightarrow Y)')$ . Suppose that $N' \subseteq (X\rightarrow Y)'$ . (The other case is similar.) Then $h((X\rightarrow Y)') = (X\rightarrow Y)' \cup \{1,w\}$ . For each $a \in W'$ , $a \in (X\rightarrow Y)'$ iff ${a \in X \rightarrow Y}$ . The right-to-left direction is straightforward. For the left-to-right, assume that $a \not \in X \rightarrow Y$ . Then there is $b, c \in W (Rabc \ \& \ b \in X \ \& \ c \not \in Y)$ . If $b, c \in W'$ , then $a \not \in (X\rightarrow Y)'$ , as required. If at least one of $b,c \in \{ 1,0,w\}$ , then we know $b \neq 0$ , $c \neq 1$ . If $b=1$ , then by the tonicity conditions, we obtain the desired result. If $b=w$ , then by the definition of the model, $c=1$ , a contradiction. If $c=0$ , the result follows by tonicity. If $c=w$ , then by definition $b=1$ , a contradiction.

Thus let’s focus on $1$ and $w$ . It suffices to show that $w, 1 \in X \rightarrow Y$ —i.e., that $\forall b, c \in W ((Rabc \ \& \ b \in X) \Rightarrow c \in Y)$ , for $a = 1$ and $a=w$ . Note that the only R additions with $1$ in the first place are (1,1,1), (1,0,b), and (1,b,1). In each case, $(R1bc \ \& b \in X) \Rightarrow c \in Y)$ , as required. Now consider $w$ . We added $(w,w,w), (w,a,1), (w,0,a)$ to obtain R, as these also imply that $(Rwbc \ \& b \in X) \Rightarrow c \in Y)$ , again because $1$ is in every element of $Prop$ and $0$ is in no elements of $Prop$ .

For (c9), we may apply similar arguments, relying on (c7). It is straightforward to show that $\forall _n \phi f = h(\forall _n \phi ' f)$ , from which the (c10) follows.

To show that this is a bounded frame, we need to show (1)–(10) of Definition 4.14. (1)–(5), (7), and (9) are straightforward. We show only (8). Suppose that $Rab0$ . We only added (1,0,0), (0, a, 0), and (a,0,0), and in each case (8) is satisfied.

To show that this is a W-frame, we must show that w is a possible world (satisfying (1)–(9) of Definition 4.16), and that conditions (1) and (2) of Definition 4.17.

To show $w \in N$ is a possible world, (1) and (2) are trivial. Of (3)–(7), we only show (6). Suppose that $Rawt$ . We only added $(w,w,w), (w,w,1), (0, w, a)$ , and $(a, w, 1)$ and in each case the consequent of (6) is satisfied. Of (8) and (9), we only show (8). Suppose that $w \in X-Y \subseteq \underset {j \in U}{\bigcap }\phi (f[j/n])$ . For $w \in X-Y$ , we have that $w \in X$ and $N' \subseteq X'$ , but $w \not \in Y$ and so $N' \not \subseteq Y'$ . Now, if $w \in \underset {j \in U}{\bigcap }\phi (f[j/n])$ , then $w \in \phi (f[j/n])$ , for each $j \in U$ , which means that $N' \subseteq \phi '(f[j/n])$ . This entails that $\underset {j \in U}{\bigcap }\phi '(f[j/n])$ must be as large as the admissible proposition $N'$ . Thus, $(\forall _n \phi )'f$ either is just $N'$ or contains it properly. By definition, $(\forall _n \phi )f$ must include $w$ , as required.

For (1) and (2) of Definition 4.17, it is easy to see the construction ensures their satisfaction: w relates to all and only the elements of N.

Thus we have indeed constructed a W-frame. To extend this frame to a model, let the valuation function $|{-}|$ assign to constants the same objects as in the $\mathbb {L}$ -model. For n-ary predicates, lets $|P^n|(u_1, \dots , u_n) = h(|P^n|^{\mathfrak {M}}(u_1, \dots , u_n))$ . That is, add $1$ to the truth set of each atomic formula’s truth set, and also add $w$ if the truth set originally contained N. This model is a bounded model: $1$ is in every truth set and $0$ is in none of the truth sets.

What remains to be shown is that invalidity of $\mathcal {A}$ in $\mathfrak {M}$ implies the invalidity of $\Box _{L} \mathcal {A}$ is the constructed W-model. We show this in two steps: first, we show that, for every $a \in W'$ , $a \in |\mathcal {A}|^{\mathfrak {M}}f$ iff $a \in |\mathcal {A}|f$ . Then we use this to show the desired result.

We show that for every $a \in W'$ , $a \in |\mathcal {A}|^{\mathfrak {M}}f$ iff $a \in |\mathcal {A}|f$ , for every $f \in U^\omega $ by induction on the complexity of $\mathcal {A}$ . If $\mathcal {A}$ is atomic, either it is either of the form ${\mkern 1mu\boldsymbol t}$ , in which case the result follows trivially, or $P^n(\tau _1, \dots , \tau _n)$ . For the latter case, the only disagreement in the models, by definition, is for the elements outside $W'$ , and so the base cases are covered.

For the inductive cases, we demonstrate only a few.

Suppose that $\mathcal {A} = \mathcal {B} \circ \mathcal {C}$ . If $a \in W'$ is such that $a \in |\mathcal {B} \circ \mathcal {C}|^{\mathfrak {M}}f$ , then there are $b, c \in W'$ such that $R'bca$ , $b \in |\mathcal {B}|^{\mathfrak {M}}f$ , and $c \in |\mathcal {C}|^{\mathfrak {M}}f$ . The points b and c bear these relations and inclusions (in the new construction) by the inductive hypothesis, and so $a \in |\mathcal {B} \circ \mathcal {C}|f$ . For the converse, suppose that $a \in |\mathcal {B} \circ \mathcal {C}|f$ . It suffices to show that $R'abc$ for $b, c \in W'$ such that $b \in |\mathcal {B}|f$ , and $c \in |\mathcal {C}|f$ . The case to worry about is when we know that, in the constructed model, $Rbca$ , when b or c is one of $w$ or $0$ or $1$ . By construction, this is the case only with the added (0,c,a), and (b, 0, a). In both cases, $0 \not \in X \in Prop$ , in which case $a \in |\mathcal {B} \circ \mathcal {C}|f$ must be witnessed by a different pair, namely a pair of elements in $W'$ , as required.

Suppose that $\mathcal {A} = \forall x_n \mathcal {B}$ . For every $a \in W'$ :

Note that these “iff” cannot be turned into “ $=$ ”, as the second step would fail, as the induction hypothesis only applies to elements of $W'$ . However, the second step, using the induction hypothesis, does hold here, because

is just

with an extra element or two (of $1, w$ ).

On to the desired result. Suppose that $\mathcal {A}$ is not valid in the $\mathbb {L}$ -model $\mathfrak {M}$ . Then there is some $a \in N$ such that $a \not \in |\mathcal {A}|^{\mathfrak {M}} f$ for some f. In the constructed model, the last fact shown implies that $a \not \in |\mathcal {A}| f$ . Moreover, since $S_{\Box _{L}}wa$ , we have that $\Box _{L} \mathcal {A}$ is not valid in the constructed W-model.

4.1 Axiomatization

Before giving an axiomatization for the whole system, we need to identify a single system for quantified classical logic. There are many routes to go, and we elect for the route where we have a possibilist interpretation of the quantifiers. Thus the following definition.

Definition 4.22. The classical first-order logic CQ is defined (with some redundancies) by taking:

1. 1. The theorems of classical propositional logic, in the first-order language $\mathbb {L}_{FO}$ .Footnote ⁹

2. 2. The axioms ( $\forall $ E), ( $\exists $ I), (R $\circ $ ), (R $\leftarrow $ ), (R ${\mkern 1mu\boldsymbol t}$ ), (EC1), (EC2).

3. 3. The rules (R $\forall $ I), (R $\exists $ E), (MP).

Remark 4.23. Note that the axiom forms of contraposition and double negation elimination are available, so in $\mathbb {L}_{FO}$ (Dual1)–(Dual4) are derivable.

Lemma 4.24. The following formulas are theorem-schemes and admissible rules of CQ.

Proof. Using ( $\forall $ E) and (R $\forall $ I) we can derive any instance of (CQ). By rewriting a proof replacing a constant symbol for the quantified variable and then applying the appropriate generalization rule, we obtain (RGC1) and (RGC2). (UG), (VQ), (AI), (RTI), and (EXT) are straightforward. The final three, ( $\circ $ =), ( $\leftarrow $ =), and ( ${\mkern 1mu\boldsymbol t}$ =) show the provable reductions of the connectives not usually taken as primitive in classical logic.

It is straightforward to show, using the previous lemma, that the logic CQ is the logic QK + (CQ) + (R $\forall $ I) from [Reference Goldblatt8], but without the modal fragment. That is, by reducing the language to exclude modal operators, and deleting the K axiom and necessitation rule. (Note that our naming convention for the rules and axioms differs from Goldblatt’s.)

The presentation of $\textbf {CQ}$ is a bit odd in that it is in a language that includes $\circ , \leftarrow $ and ${\mkern 1mu\boldsymbol t}$ . However, these are definable in first-order classical logic, and such a presentation does not affect the system as a whole.

Definition 4.25. Let $\mathbb {L}$ be an axiom system for a quantified modal relevant logic as given in Section 3. The logic $\mathbb {CL}$ based on $\mathbb {L}$ is defined by:

1. 1. The theorems of CQ, with (MP), (R $\forall $ I), (R $\exists $ E), written in the language $\mathfrak {L}_{\textbf {QBM.C}}$ .

2. 2. For all axiom schemes $\mathcal {A}$ of $\mathbb {L}$ , and axiom scheme $\Box _{L} \mathcal {A}$ .

3. 3. For all rules $\mathcal {A}_1, \dots \mathcal {A}_n \Rrightarrow \mathcal {B}$ of $\mathbb {L}$ , a rule $\Box _{L}\mathcal {A}_1, \dots \Box _{L}\mathcal {A}_n \Rrightarrow \Box _{L}\mathcal {B}$ .

4. 4. The bridge rule (BR): $\Box _{L} (\mathcal {A} \rightarrow \mathcal {B}) \Rrightarrow \mathcal {A} \rightarrow \mathcal {B}$ .

The following lemma will be useful in the completeness proof below.

Lemma 4.26. The rule (RGC2)— $\mathcal {A}[c/x] \Rrightarrow \forall x \mathcal {A}$ —is derivable in any logic $\mathbb {CL}$ .

Proof. The proof has two steps. First, we note that the universal generalization rule is derivable. This follow from the definition of inferential behaviour of ${\mkern 1mu\boldsymbol t}$ , and the rule ( $\forall $ E), in $\mathbb {CL}$ . Second, we rewrite the terms in a proof of $\mathcal {A}[c/x]$ to obtain a proof of $\mathcal {A}[y/x]$ , for a brand new y, which allows us to apply ( $\forall $ E) for the desired result.

We now move on to showing that this axiom system is sound and complete with respect to the W-models defined above. However, before moving on, let’s address a worry that the reader may have at this point.

5 Soundness

As in [Reference Sedlár and Vigiani18], it is provable that the $\Box _{L}$ operator encodes $\mathbb {L}$ , as in the following.

6 Completeness

6.2 Canonical Model

Definition 6.35 (Canonical Model for CL).

Given a logic $\textbf {CL}$ based on the quantified modal relevant logic $\mathbb {L}$ extending $\textbf {QBM.C}$ , the canonical model is defined as follows:

$$ \begin{align*} \mathfrak{M}^{\mathbb{C}} &= \langle K^{\mathbb{C}}, N^{\mathbb{C}}, W^{\mathbb{C}}, R^{\mathbb{C}}, *^{\mathbb{C}}, S_{\Box}^{\mathbb{C}}, S_{\Box_{L}}^{\mathbb{C}}, U^{\mathbb{C}}, Prop^{\mathbb{C}}, PropFun^{\mathbb{C}} \rangle, \end{align*} $$

where:

1. 1. $K^{\mathbb {C}}$ is the set of prime $\mathbb {L}$ -theories.

2. 2. $N^{\mathbb {C}}$ is the set of all regular prime $\mathbb {L}$ -theories.

3. 3. $W^{\mathbb {C}}$ is the set of all regular prime CL-theories.

4. 4. $R^{\mathbb {C}}$ is the relation $R'$ restricted to $K^{\mathbb {C}}$ .

5. 5. $*^{\mathbb {C}}$ is given by $a^* = \{\mathcal {A} : \neg \mathcal {A} \not \in a \}$ .

6. 6. $S_{\Box }^{\mathbb {C}}$ is the relation $S_{\Box }'$ restricted to $K^{\mathbb {C}}$ .

7. 7. $S_{\Box _{L}}^{\mathbb {C}}$ is the relation $S_{\Box _{L}}'$ restricted to $K^{\mathbb {C}}$ .

8. 8. $U^{\mathbb {C}}$ is the infinite set of constants $Con$ .

9. 9. For every closed formula $\mathcal {A}$ , .

10. 10. .

11. 11. Given an $f \in U^\omega $ , $fn$ is a constant. For any formula $\mathcal {A}$ , let $\mathcal {A}^f$ be the closed formula that results from replacing every free occurrence of a variable $x_n$ with the constant $fn$ . That is, $\mathcal {A}^f =_{df} \mathcal {A}[f0/x_0, \dots , fn/x_n, \dots ]$ .

12. 12. For each formula $\mathcal {A}$ , the function $\phi _{\mathcal {A}}: U^\omega \longrightarrow Prop_{\mathbb {C}}$ is given by .

13. 13. $PropFun^{\mathbb {C}}$ is the set of all functions $\phi _{\mathcal {A}}$ , for each formula $\mathcal {A}$ .

14. 14. The canonical valuation function is given by:

    1. (a) $|c|=c$ .

    2. (b) .

    3. (c) The valuation is extended to all wff as before.

Lemma 6.36 (Underling quantified modal relevant structure).

The structure

$$\begin{align*}\langle K^{\mathbb{C}}, N^{\mathbb{C}}, R^{\mathbb{C}}, *^{\mathbb{C}}, S_{\Box}^{\mathbb{C}}, S_{\Box_{L}}^{\mathbb{C}}, U^{\mathbb{C}}, Prop^{\mathbb{C}}, PropFun^{\mathbb{C}} \rangle \end{align*}$$

is an $\mathfrak {L}$ -frame, in the sense of [Reference Ferenz6], with two box-like modalities. In particular, the following facts are established:

1. 1. $\leq = \subseteq $ .

2. 2. $\otimes \phi _{\mathcal {A}} = \phi _{\otimes \mathcal {A}}$ (for $\otimes \in \{\neg , \Box , \Box _{L}\}$ ).

3. 3. $\phi _{\mathcal {A}} \otimes \phi _{\mathcal {B}} = \phi _{\mathcal {A}\otimes \mathcal {B}}$ (for $\otimes \in \{\land , \lor , \rightarrow , \circ , \leftarrow \}$ ).

4. 4. $\forall _n \phi _{\mathcal {A}} = \phi _{\forall x_n \mathcal {A}}$ ; $\exists _n \phi _{\mathcal {A}} = \phi _{\exists x_n \mathcal {A}}$ .

5. 5. For closed $\forall x \mathcal {A}$ and $\exists x \mathcal {A}$ :

   1. (a) , and

   2. (b) .

6. 6. And (consequently) that (c1)–(c10) of Definition 2.2 hold.

The proof is an in [Reference Ferenz6], and will be omitted here.

Lemma 6.37. The canonical frame is a bounded frame, in the sense of Definition 4.14.

Proof. The empty theory and the full theory, which we will call $0$ and $1$ respectively, are both in the canonical frame. By Lemma 6.36(1), $0 \leq \alpha \leq 1$ . Using the arguments of Sedlár and Vigiani we may show (2)–(6), and the arguments for (7)–(10) are straightforwardly similar to (5)–(6) and left to the reader.

Lemma 6.38. Each $w \in W^{\mathbb {C}}$ is a world, in the sense of Definition 4.16.

Proof. Items (1)–(4) can be given by Sedlár and Vigiani’s arguments, and (5)–(7) are similar. Of the remaining cases, we show the case for (8), which is a modified and shortened version of the arguments of [Reference Mares and Goldblatt12, theorem 10.3], but with the restriction to $w \in W^{\mathbb {C}}$ .

Assume that $w \in X - Y \subseteq \underset {j \in U}{\bigcap } \phi (f[j/n])$ , for some $w \in W^{\mathbb {C}}$ . $Y \in Prop$ , so

for a closed $\mathcal {A}$ ; and $\phi = \phi _{\mathcal {B}}$ for some formula (possible open) $\mathcal {B}$ . We thus have, for every $c \in con$ ,

and so (since $\mathcal {A}$ is closed)

where $\mathcal {A}^{f\backslash n} = \mathcal {A}[f0/x_0, \dots f(n-1)/x_{(n-1)}, x_n/x_n, f(n+1)/x_{(n+1)}, \dots ] $ , and consequently $\mathcal {A}^{f\backslash n}[c/x_n] = \mathcal {A}^{f[c/n]}$ as well as $\forall x_n(\mathcal {A}^{f \backslash n}) = (\forall x_n \mathcal {A})^{f}$ . Since this entails that $(\mathcal {A} \lor \mathcal {B})^{f\backslash n}[c/x_n] \in w$ , for each $c \in con$ , by Lemma 6.36(v).(a) we have that $\forall x_n ((\mathcal {A} \lor \mathcal {B})^{f\backslash n})\in w$ . By extensional confinement, since $w \in W^{\mathbb {C}}$ , we have $\mathcal {A} \lor \forall x_n (\mathcal {B}^{f \backslash n}) \in w$ .

Since , $\forall x_n (\mathcal {B}^{f \backslash n}) \in w$ , and by an earlier equality we have $(\forall x_n \mathcal {B})^f \in w$ , and thus $w \in (\forall _n \phi _{\mathcal {B}})f$ , as required.

Lemma 6.39. The canonical model satisfies:

1. 1. $(\forall w \in W)(\forall u \in K)(S_{\Box _{L}}wu \Rightarrow u \in N)$ .

2. 2. $(\forall k \in N)(\exists w \in W) S_{\Box _{L}}ws $ .

Proof. For (1), suppose for some $w \in W^{\mathbb {C}}$ that $S_{\Box _{L}}wu$ for some $u \in K^{\mathbb {C}}$ . Then for every $\mathbb {L}$ -theorem $\mathcal {A}$ , $\Box _{L} \mathcal {A} \in w$ , and so then $\mathcal {A} \in u$ , making u a regular $\mathbb {L}$ -theory, and so a member of N, as required.

For (2), suppose that $\alpha \in N$ . (Suppose also that $\alpha \neq 1$ , in which case the result trivially follows.) We are required to find a world $w \in W^{\mathfrak {C}}$ such that, if $\Box _{L} \mathcal {A} \in w$ , then $\mathcal {A} \in \alpha $ . Let $\Gamma = \{ \mathcal {A} :\, \vdash _{CL} \mathcal {A}\}$ , which is clearly a non-empty, nontrivial $CL$ -theory, and thus an $\mathbb {L}$ -regular theory. Further let $\Delta = \{ \Box _{L} \mathcal {A} : \mathcal {A} \not \in \alpha \}$ . $\Delta $ is non-empty, since $\alpha $ is non-trivial.

It follows that $(\Gamma ,\Delta )$ is a CL-independent pair. Here we use the reasoning of Sedlár and Vigiani. If it were not a pair, then $\vdash _{\mathbb {CL}} \Box _{L} \mathcal {A}_1 \lor \dots \lor \Box _{L} \mathcal {A}_n$ . But then $\vdash _{\mathbb {CL}} \Box _{L} (\mathcal {A}_1 \lor \dots \lor \mathcal {A}_n)$ , which by Theorem 5.28 entails that $\vdash _{\mathbb {L}} (\mathcal {A}_1 \lor \dots \lor \mathcal {A}_n)$ . And so since $\alpha $ is prime and regular, one of $\mathcal {A}_1, \dots \mathcal {A}_n$ is in $\alpha $ , which gives the required contradiction.

Finally, by applying the extension Lemma 6.31(i), we obtain an prime, non-trivial maximally consistent $\mathbb {L}$ -theory, indeed $\mathbb {CL}$ -theory, $\Gamma ' \in W^{\mathbb {C}}$ such that $S_{\Box _{L}}^{\mathbb {C}} \Gamma ' \alpha $ , as required.

Lemma 6.40. For any extensions obtained using Table 1, the appropriate conditions are satisfied by the canonical model.

The proof of this lemma is standard and omitted.

Therefore the canonical frame is indeed a W-frame. What’s left to show is that it is also a W-model and that truth is membership. Mares and Goldblatt’s arguments establish the following lemma.

Lemma 6.41 (Atomic Propositional Functions).

For every n-ary predicate symbol P, every $f \in U^\omega $ , and every set of terms $\tau _1, \dots \tau _n$ :

1. 1. $P(\tau _1, \dots \tau _n)^f = P(|\tau _1|f, \dots , |\tau _n|f)$ .

2. 2. $|P(\tau _1, \dots \tau _n)| = \phi _{P(\tau _1, \dots \tau _n)}$ .

The above lemma ensures that all atomic formulas are mapped to members of $PropFun^{\mathbb {C}}$ , and then Lemma 6.36 extends this fact to all formulas. Thus the canonical model is a model.

Lemma 6.42 (Truth Lemma).

For any formula $\mathcal {A}$ , $|\mathcal {A}| = \phi _{\mathcal {A}}$ . This is, for every $f \in U^\omega $ , , which is $a \in |\mathcal {A}|f$ iff $\mathcal {A}^f \in a$ .

The proof of the truth lemma is by induction on the structural complexity of a formula. The arguments of [Reference Ferenz6] and [Reference Mares and Goldblatt12] can be employed, using the facts established in Lemma 6.36.

We thus have both that the canonical model is a model, and that truth is membership. Consequently, we obtain the following.

Theorem 6.43 (Completeness for $\mathbb {CL}$ and extensions).

For any $\mathbb {CL}$ based on an $\mathbb {L}$ obtained from $\textbf {QBM.C}$ (and Table 1), we have $\vDash _{\mathbb {CL}} \text { implies } \vdash _{\mathbb {CL}}$ .

Proof. Suppose that $\vDash _{\mathbb {CL}} \mathcal {A}$ . Then every regular prime $\mathbb {CL}$ -theory contains $\mathcal {A}^f$ , for each $f \in U^\omega $ . For every free variable in $\mathcal {A}$ , replace it with a new constant not in $\mathcal {A}$ . This formula belongs to every regular prime $\mathbb {CL}$ -theory, and is therefore a $\mathbb {CL}$ -theorem by Corollary 6.32. Repeated but finite applications of (RGC2) (see Lemma 4.26) followed by repeated but finite applications of the axiom ( $\forall $ E), will produce a proof of $\mathcal {A}$ .

7 Worlds and $\omega $ -completeness

In a canonical model, an $\omega $ -complete situation or world is such that, if it contains every instance $\mathcal {A}^f$ of $\forall x_n \mathcal {A}$ , then it also contains $\forall x_n \mathcal {A}$ . We also use the phrase $\omega $ -complete to describe points in any model such that, for $a \in K$ , if $a \in |\mathcal {A}|f$ for every f, then $a \in |\forall x_n \mathcal {A}|f$ , for every formula $\mathcal {A}$ and every variable assignment f. For simplicity, in all cases we will use the phrase $\omega $ -completeness as it is used in the canonical model. This is despite most models not having enough constant symbols for the substitutional view; however, the general idea is the same.

A Russellian and philosophical distinction between $\omega $ -complete and $\omega $ -incomplete situations is that the $\omega $ -complete situations have the extra information concerning what all the objects in the domain are. That is, it has a “that’s all”-clause. Now, one philosophical intuition one might profess is that robust possible worlds decide everything, but what exactly is meant by this? We discuss two possibilities here. First, one can mean that worlds decide anything and everything, including those “meta” properties such as that’s-all clauses. The second is that worlds decide every formula expressible in a language. At present, the author believes that neither of these views are correct (and for more than just a rejection of metaphysical intuitions on such things as possible worlds). The first seems to overload worlds with more than we may have reason to suppose. A stronger version of the first, which we shall explore a little here—and which the author also believes is incorrect—is that worlds decide every that’s-all clause. The second view appears to limit possible worlds to what we can express in a particular language, which may appeal to certain Ersatzist interpretations. While I am sympathetic to such linguistically based approaches to possible worlds, it doesn’t appear that the language of the logics presented here entail some consequences for $\omega $ -completeness. In fact, this second view can be seen to be present in the models constructed above, every formula is decided in every world. In short: the first is an ad-hoc delimitation of worlds, and the second is an ad-hoc limitation on possible worlds. Thus, for the remainder of this section, let’s consider the modification of the first view, and some formal troubles that arise.

In the completeness proof, for Lemma 6.39, in showing that every member of N has a world that can see it, we encounter an interesting problem in logics with the addition of the Barcan formula (for the $\Box _{L}$ operator). The $\mathbb {L}$ -regular theory $\alpha $ is not necessarily $\omega $ -complete as defined. Now, suppose that $\mathcal {A}^{f[j/x_n]}\in \alpha $ , for every $j \in Con$ , but $\forall x_n \mathcal {A}^f \not \in \alpha $ . Then $\Delta $ , as defined in the lemma, contains $\Box _{L}\forall x_n \mathcal {A}^f$ but never $\Box _{L} \mathcal {A}^{f[j/n]}$ . So $\Gamma $ can be extended by every instance $\Box _{L}\mathcal {A}^{f[j/x_n]}$ . Then, if $\Gamma '$ is $\omega $ -complete, then $\forall x_n \Box _{L}\mathcal {A} \in \Gamma '$ . Finally, from the Barcan formula we obtain a contradiction.

Having seen that part of the problem is that the theory $\alpha $ is not $\omega $ -complete (and not a possible world, in general), one might respond: “While I have some intuition that robust possible worlds ought to be $\omega $ -complete, I either have no intuition regarding situations one way or the other. That is, it appears to do no philosophical harm to the motivations for $\omega $ -complete worlds to require all ( $\mathbb {L}$ -normal) situations to also be $\omega $ -complete. Indeed, there may be some intuition that the so-called ‘logically normal’ points be $\omega $ -complete, for that is just part of what ‘logically-normal’ means.”

First, I wish to stave off the argument that logical normality entails $\omega $ -completeness in this setting. The so-called logically normal worlds are just the worlds where the logical operators behave according to logic. That is, these points make every theorem true. In other words, similar to the second view above, these points are normal with respect to the behavior of formulas, and not their meta properties such as $\omega $ -completeness.

Having prevented a certain misunderstanding, I now turn to the difficulties in carrying out the task of making all situations $\omega $ -complete. Then I will investigate the possibility of making only the situations in $N \ \omega $ -complete.

If we make every situation $\omega $ -complete, and thus require the Tarskian truth conditions for quantified formulas, then (even after adding the Barcan formula) the defined axiom systems will be incomplete for non-general frame semantics for sufficiently strong logics.Footnote ¹² Fine [Reference Fine, Norman and Sylvan7] has shown that Tarskian truth conditions plus non-general frames entails incompleteness for strong relevant logics including R, E, T, and others. Thus, requiring all points to be $\omega $ -complete should not be done in conjunction with giving up general frames. However, I conjecture the following:

This conjecture is suggested by some results of [Reference Goldblatt8] and [Reference Goldblatt and Mares9]. A couple of first-order modal classical logics are shown to be complete w.r.t. the MG semantics (and in one case with variable domain MG semantics). There logics are also known to be incomplete w.r.t. non-general frame, semantics with a Tarskian truth condition. The results in question, however, show completeness for general frame, Tarskian models. That is, for completeness for these logics, general frames are sufficient.

This conjecture remains to be proved or disproved. Moreover, (we have given) no particular philosophical explanation to settle the more interpretive questions corresponding to this conjecture.

8 Concluding remarks

Herein we have constructed first-order epistemic logics based on the propositional epistemic logics of [Reference Sedlár and Vigiani18]. In addition, we have proven modular soundness and completeness results, and further explored some key formal and philosophical difficulties. The systems defined here, as in [Reference Sedlár and Vigiani18], avoid some but not all of the problems of logical omniscience; beliefs are still closed under relevant implication. This problem may be further ameliorated by switching to neighbourhood-based semantics, so far as closing beliefs under relevant bi-implication improves matters.

On the first-order side of things, in addition to the $\omega $ -completeness, there are also the questions of constructing models with variable domains, identity, epistemic constructions such as being familiar with (or knowing) an object, and so forth. Variable domains should be constructible, following [Reference Mares11], by adding an existence predicate, adding a domain function that determines a subdomain of U for each situation, modifying the truth condition of a quantified formula, and appropriately replacing certain first-order axioms.

Identity, however, is not as straightforward. Traditional approaches to identity in relevant logics leads to irrelevant logics—i.e., the validity of implications such as $p \rightarrow x=x$ . Several MG-based approaches to identity in relevant logics have been recently developed, such as in [Reference Ferenz4] (based on Kremer’s relevant indiscernibility interpretation of identity [Reference Kremer10]) and [Reference Standefer22]. These are starting points for identity adding identity to the epistemic logics here.

It might be supposed that being familiar with an object in some respect is a precondition for knowing that the object has or lacks certain properties. A logic of familiarity is developed, e.g., in [Reference Syverson23]. Developing the constructions of this paper to include predicate(s) for familiarity would allow us to further deal with forms of logical omniscience. For an agent to know that $P(\tau )$ , we could require the agent to be familiar with the object $\tau $ .

The present paper thus serves as a starting point for several philosophical and formal projects in epistemic logic.