2 Basic quantified modal relevant logics

For quantified modal relevant logics, we begin with a denumerable set of variables, Var, which will be conveniently denoted by lowercase letters near the end of the alphabet (e.g., $x, y, z, x_n, w_1$ ). A possibly denumerable set $\mathcal {L}$ of predicate symbols, and individual constants shall be called a signature. Each predicate symbol is of the form $P^{n}$ , where n is the arity of the predicate. Often I will omit the superscript if either the arity is obvious or the arity is irrelevant. Each signature is denumerable at most, so the set of predicate symbols can be ordered. For every signature $\mathcal {L}$ , its set of individual constants shall be denoted by $Con$ . I shall denote individual constants by c, with or without subscripts.

A term will be denoted by $\tau $ with or without subscripts. An $\mathcal {L}$ -term, relative to a signature $\mathcal {L}$ , is defined as follows. Every variable $v_n$ is an $\mathcal {L}$ -term. Every member c of $Con$ is an $\mathcal {L}$ -term. No other expression is a term. A term is closed when it contains no variables. A term is open when it is not closed.

For a given signature $\mathcal {L}$ , the atomic formulas (atomic $\mathcal {L}$ -formulas) are those of the form $P^n(\tau _1,\dots ,\tau _n)$ , where $P^n \in \mathcal {L}$ and each of $\tau _1, \dots , \tau _n$ is an $\mathcal {L}$ -term. The set of well-formed formula of a quantified logic with signature $\mathcal {L}$ (denoted by ${{wff}}_{\mathcal {L}}$ or simply wff) is defined inductively using the connectives $\rightarrow $ (relevant implication), $\wedge $ (extensional conjunction), $\vee $ (extensional disjunction), $\neg $ (negation), $\circ $ (fusion or intensional conjunction), ${ {\mkern 1mu\boldsymbol t}}$ (intensional truth) and, for modal propositional logics, $\Diamond $ (possibility), $\Box $ (necessity) and $\forall x$ and $\exists x$ , for each variable $x \in $ Var. The biconditional, $\leftrightarrow $ , is taken to be defined in the usual way. In general, I will use capital letters near the beginning of the English alphabet to denote or range over the well-formed formulas of a language.

An instance of a variable x is bound in the wff $\mathcal {A}$ if either (1) the instance is the x of an expression $\forall x$ or $\exists x$ occurring in $\mathcal {A}$ or (2) the instance of x occurs within the scope of a quantifier, $\forall x$ or $\exists x$ . An instance of a variable is free when it is not bound. A formula with no free variables is called a sentence.

A term $\tau $ is free for (or freely substitutable for) x in wff $\mathcal {A}$ if, for every variable y in $\tau $ , there are no free occurrences of x in $\mathcal {A}$ that are within the scope of a quantifier $\forall y$ or $\exists y$ .

A shorthand for substitutions will be convenient for our purposes. We shall write $\mathcal {A}[\tau /x]$ for the result of replacing every free occurrence of x in $\mathcal {A}$ with the term $\tau $ . It will also be convenient to have a notation for the operation of several simultaneous substitutions. 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 assignment, f, assigns to each variable an element of the domain of individuals, U, as follows. There are a denumerable number of variables which can be ordered as $x_1, x_2, \dots $ , and a variable assignment is an ordered denumerable list of individuals. In other words, a variable assignment is a member of $U^\omega $ , where the nth individual in the ordering is the individual assigned to the variable $x_n$ . The set of all variable assignments, relative to a domain U, is the set $U^\omega $ .

An x-variant of a variable assignment $f \in U^\omega $ for a domain of individuals U is a variable assignment that differs from f only in the individual assigned to the variable x. The set of all x-variants of f will be denoted by $xf$ .

By convention, we write:

$$ \begin{align*} R^2xyzw &=_{df} \exists v(Rxyv \wedge Rvzw),\\ S^2xy &=_{df} \exists z(Sxz \wedge Szy). \end{align*} $$

3 The logics ${\bf QB}.{\bf C}_{\Box \Diamond }$ and ${\bf BQ}.{\bf C}_{\Box \Diamond }$

Here, the base quantified modal relevant logic is ${\bf QB}.{\bf C}_{\Box \Diamond }$ , the implicational fragment of which is the basic affixing logic B.Footnote ³ The logic ${\bf QB}.{\bf C}_{\Box \Diamond }$ extends the regular modal relevant logic B.C as defined in [Reference Seki30]. The logic ${\bf BQ}.{\bf C}_{\Box \Diamond }$ , as we will see, extends ${\bf QB}.{\bf C}_{\Box \Diamond }$ so that the quantifiers are more classical.

The following axioms schemes and rules define ${\bf QB}.{\bf C}_{\Box \Diamond }$ .

1. (A1) $\mathcal {A}\rightarrow \mathcal {A}$ Identity

2. (A2) $\mathcal {A}\rightarrow (\mathcal {A} \vee \mathcal {B})$ Disjunction Introduction (left)

3. (A3) $\mathcal {B}\rightarrow (\mathcal {A} \vee \mathcal {B})$ Disjunction Introduction (right)

4. (A4) $(\mathcal {A}\wedge \mathcal {B})\rightarrow \mathcal {A}$ Conjunction Elimination (left)

5. (A5) $(\mathcal {A}\wedge \mathcal {B})\rightarrow \mathcal {B}$ Conjunction Elimination (right)

6. (A6) $\mathcal {A}\wedge (\mathcal {B} \vee \mathcal {C})\rightarrow ((\mathcal {A}\wedge \mathcal {B})\vee (\mathcal {A}\wedge \mathcal {C}))$ $\wedge \vee $ -Distribution

7. (A7) $((\mathcal {A}\rightarrow \mathcal {B})\wedge (\mathcal {A}\rightarrow \mathcal {C}))\rightarrow (\mathcal {A}\rightarrow (\mathcal {B} \wedge \mathcal {C}))$ Conjunction Introduction

8. (A8) $((\mathcal {A}\rightarrow \mathcal {C})\wedge (\mathcal {B}\rightarrow \mathcal {C}))\rightarrow ((\mathcal {A}\vee \mathcal {B})\rightarrow \mathcal {C})$ Disjunction Elimination

9. (A9) $\neg \neg \mathcal {A}\rightarrow \mathcal {A}$ Double Negation Elimination

10. (A10) $\forall x \mathcal {A} \rightarrow \mathcal {A}[\tau /x]$ , where $\tau $ is free for x in $\mathcal {A}$ Universal Instantiation

11. (A11) $\mathcal {A}[\tau /x] \rightarrow \exists x \mathcal {A}$ , where $\tau $ is free for x in $\mathcal {A}$ Existential Introduction

12. (A12) $(\Box \mathcal {A} \wedge \Box \mathcal {B}) \rightarrow \Box (\mathcal {A} \wedge \mathcal {B})$ $\Box \wedge ^{-}$ -Distribution

13. (A13) $\Diamond (\mathcal {A} \vee \mathcal {B}) \rightarrow (\Diamond \mathcal {A} \vee \Diamond \mathcal {B})$ $\Diamond \vee $ -Distribution

14. (A14) $\forall x (\mathcal {A} \rightarrow \mathcal {B})\rightarrow (\exists x \mathcal {A} \rightarrow \mathcal {B})$ where x is not free in $\mathcal {B}$

Footnote ⁴

The conditions on $\exists $ -Intro and $\forall $ -Intro are that x is not free in $\mathcal {B}$ for $\exists $ -Intro and x is not free in $\mathcal {A}$ for $\forall $ -Intro. The rules $\Box $ -M and $\Diamond $ -M stand for $\Box $ -Monotonicity and $\Diamond $ -Monotonicity.

Note that axiom (A14) is provable from the other axioms is systems whose propositional fragment includes the axiom form of contraposition, $(\mathcal {A} \rightarrow \mathcal {B}) \rightarrow (\neg \mathcal {B} \rightarrow \neg \mathcal {A})$ , given the duality of the quantifiers (see Lemma 3.3). A related formula, $\forall x (\mathcal {A} \rightarrow \mathcal {B})\rightarrow (\mathcal {A} \rightarrow \forall x \mathcal {B})$ , where x is not free in $\mathcal {A}$ , is derivable in the defined system due to the presence of fusion. Moreover, (A14) is derivable in the system defined as ${\bf QB}.{\bf C}_{\Box \Diamond }$ plus the left arrow governed by following rules:

${\bf QB}.{\bf C}_{\Box \Diamond }$ is defined with fusion and without the left arrow, so (A14) is adopted as an axiom, and the related $\forall x (\mathcal {A} \rightarrow \mathcal {B})\rightarrow (\mathcal {A} \rightarrow \forall x \mathcal {B})$ is not.

The logic ${\bf BQ}.{\bf C}_{\Box \Diamond }$ results from adding to ${\bf QB}.{\bf C}_{\Box \Diamond }$ the extensional confinement axiom scheme (EC $_{\forall }$ ), or any equivalent scheme.

1. EC_∀ $\forall x (\mathcal {A} \vee \mathcal {B})\rightarrow (\mathcal {A} \vee \forall x \mathcal {B})$ , where x is not free in $\mathcal {A},$

2. EC_∃ $(\mathcal {A} \wedge \exists x \mathcal {B})\rightarrow \exists x (\mathcal {A} \wedge \mathcal {B})$ , where x is not free in $\mathcal {A}.$

Strictly speaking, the existential (or universal) quantifier can be taken as defined, and the resulting logic will contain the same theorems (under the usual translation). Under the usual translation, the axiom schemes and rules for the defined quantifier are derivable.

The propositional logic $\textbf {B}$ , the basis over which we get ${\bf QB}.{\bf C}_{\Box \Diamond }$ , is defined using a propositional language by axioms (A1)–(A9), and rules MP, AJD, Prefix, Suffix, and Contraposition. ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ defined by extending $\textbf {B}$ with the rules for ${ {\mkern 1mu\boldsymbol t}}$ and $\circ $ .

For first order relevant logics ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ , we extend ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ with (A10) and (A11) with rules $\forall $ -Intro and $\exists $ -Intro. The logic ${\bf BQ}^{\circ { {\mkern 1mu\boldsymbol t}}}$ extends ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ with the extensional confinement axioms.

Seki uses the phrase “regular modal logic over $\mathbb {L}$ ” to describe the modal relevant logics including the axioms and rules of $\mathbb {L}$ , axioms (A12) and (A13), and rules $\Box $ -M and $\Diamond $ -M. The least regular modal logic over $\mathbb {L}$ is denoted $\mathbb {L}.\textbf {C}$ . Here, I will generally omit the adjective ‘regular’, opting instead for “quantified modal logic over $\mathbb {L.}$ ”

In the least regular modal logic over ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ , and over ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ , the formulas $\Box \mathcal {A} \leftrightarrow \neg \Diamond \neg \mathcal {A}$ and $\Diamond \mathcal {A} \leftrightarrow \neg \Box \neg \mathcal {A}$ are not theorems. Thus, two additional modalities are introduced by Seki by definitions:

1. $\diamond\kern-6pt\cdot \mathcal {A} =_{def}\neg \Box \neg \mathcal {A},$

2. $\boxdot \mathcal {A} =_{def} \neg \Diamond \neg \mathcal {A}.$

It is worth noting that modal relevant logics, especially stronger ones, are often defined taking only one modality as primitive, and defining the other. Strictly speaking, these logics employ the modalities $\Box $ and $\diamond\kern-4pt\cdot$ (or $\Diamond $ and $\boxdot $ ). In the frames for these logics, we typically only only see a single binary relation for both modalities, which is sufficient to guarantee the kind of duality/interdefinability that the modalities share.Footnote ⁵ However, in general the classical behavior of the primitive $\Box $ and $\Diamond $ in regular modal relevant logics requires addition axioms.

The dot in the name of the logics signifies that the modal fragment is not “sufficiently classical,” which means here that there are identifiable formulas that are theorems of the modal classical logic that are not theorems (under suitable translation) of the corresponding modal relevant logic. The axiom $\Box (\mathcal {A} \vee \mathcal {B}) \rightarrow (\Diamond \mathcal {A} \vee \Box \mathcal {B})$ , for example, has been added to the modal relevant logic NR and logic of entailment ${\bf E}$ in order to capture modal fragment of S4 (see [Reference Routley and Meyer25], p. 69–70). Mares has pointed out that this axiom, first suggested by Belnap, bears a striking resemblance to the confinement axioms for the quantifiers. As we will only have means to analyze what it means for a logic to be sufficiently classical in this sense when we consider extensions to the modal fragments in Section 8, the explanation of the dot/dotless convention is left until Section 9 where I will further discuss the interactions between $\Box $ and $\Diamond $ .

3.1 Some Proofs

Given the relative weakness of the logic ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ , it is worth noting a few theorems of ${\bf QB}.{\bf C}_{\Box \Diamond }$ . In particular, note the duality of the quantifiers. In contrast, as just noted, the modalities $\Box $ and $\Diamond $ are not provably dual. The following lemmas serve to highlight features of ${\bf QB}.{\bf C}_{\Box \Diamond }$ , some of which will be used in later proofs.

The rules $\forall $ -Intro(con), UG(con), and $\exists $ -Intro(Con) are as follows:

The rule $\forall $ -Intro(Con) has the requirement that c is not in $\mathcal {A}$ or $\mathcal {B}$ and x is not free in $\mathcal {A}$ , UG(Con) the requirement that c is not in $\mathcal {A}$ , and $\exists $ -Intro(Con) the requirement that c is not in $\mathcal {A}$ or $\mathcal {B}$ and x is not free in $\mathcal {B}$ .

The following lemmas will be useful in completeness proofs below.

Lemma 3.1. For both ${\bf QB}.{\bf C}_{\Box \Diamond }$ and ${\bf BQ}.{\bf C}_{\Box \Diamond }$ ,

1. 1. $\forall y(\mathcal {A}[y/x]) \rightarrow \forall x \mathcal {A}$ is a theorem if y is not free in $\mathcal {A}$ .

2. 2. $\exists y(\mathcal {A}[y/x]) \rightarrow \exists x \mathcal {A}$ is a theorem if y is not free in $\mathcal {A}$ .

Lemma 3.2. The rules $\forall $ -Intro(con), UG(con), and $\exists $ -Intro(Con) are derivable.

The proof of 3.1.1 and the $\forall $ -Intro(con), UG(con) cases for 3.2 are by the arguments given by Mares and Goldblatt Mares and Goldblatt [Reference Mares and Goldblatt20] for ${\bf RQ}{\textbf {4}}^{\circ { {\mkern 1mu\boldsymbol t}}}$ in Lemmas 6.1, 6.3, 6.5, and 6.6. (By expanding some of the condensed steps in the proofs, it is clear that the proofs apply to ${\bf QB}.{\bf C}_{\Box \Diamond }$ ). The proof for 3.1.2 and $\exists $ -Intro(Con) is by similar arguments.

Lemma 3.3. The following are theorems of ${\bf QB}.{\bf C}_{\Box \Diamond }$

1. 1. $\forall x (\mathcal {A} \rightarrow \mathcal {B})\rightarrow (\mathcal {A} \rightarrow \forall x \mathcal {B})$ , where x is not free in $\mathcal {A}$

2. 2. $\forall x \mathcal {A} \rightarrow \neg \exists x \neg \mathcal {A}$

3. 3. $ \neg \exists x \neg \mathcal {A} \rightarrow \forall x \mathcal {A}$

4. 4. $\exists x \mathcal {A} \rightarrow \neg \forall x \neg \mathcal {A}$

5. 5. $ \neg \forall x \neg \mathcal {A} \rightarrow \exists x \mathcal {A}$

Proof. A proof for 1. can be found in [Reference Mares and Goldblatt20], expanding their arguments to confirm that the axioms and rules used are available in ${\bf QB}.{\bf C}_{\Box \Diamond }$ . For the remaining cases, I only show two.

The Barcan formulas have been of interest in quantified modal logic. The Barcan Formula (BF), the Converse Barcan Formula (CBF), and their duals with the existential quantifier and diamonds (BF $_{\exists \Diamond }$ , CBF $_{\exists \Diamond }$ ) are as follows:

• BF  $\forall x \Box \mathcal {A} \rightarrow \Box \forall x \mathcal {A},$

• CBF  $\Box \forall x \mathcal {A} \rightarrow \forall x \Box \mathcal {A},$

• BF_∃◇  $\Diamond \exists x \mathcal {A}\rightarrow \exists x \Diamond \mathcal {A} ,$

• CBF_∃◇  $\exists x \Diamond \mathcal {A} \rightarrow \Diamond \exists x \mathcal {A}.$

Lemma 3.4. The Converse Barcan Formula and its dual are theorems of ${\bf QB}.{\bf C}_{\Box \Diamond }$ .

Proof.

The proof for CBF $_{\exists \Diamond }$ is similar, but using axiom A11 and rules $\Diamond $ -M and $\exists $ -Intro.

The Barcan Formula and its dual are not theorems ${\bf QB}.{\bf C}_{\Box \Diamond }$ . However, this is a corollary of a result below, which demonstrates that the Barcan Formula is not a theorem of a much stronger QMRL.

4 Semantics for ${\bf QB}.{\bf C}_{\Box \Diamond }$ and ${\bf BQ}.{\bf C}_{\Box \Diamond }$ .

To construct semantic for ${\bf QB}.{\bf C}_{\Box \Diamond }$ and ${\bf BQ}.{\bf C}_{\Box \Diamond }$ , I combine the Mares–Goldblatt semantics for quantified relevant logics with Seki’s semantics for modal relevant logics. As such, I will first explicate general frames for propositional relevant logic ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ . Following that, propositions and propositional functions are explained, giving particular emphasis to the operations on propositions used by Mares and Goldblatt to model the quantifiers.

4.1 General Frame Semantics and ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ .

First, a definition of frames for the logic B is given. Given the set of primitive connectives $\rightarrow , \neg , \wedge $ and ${ {\mkern 1mu\boldsymbol t}}$ , the rest are definable, so for this section we make the simplification to the fragment of ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ containing just these connectives. From there, general frames are introduced.

Definition 4.5. A B-frame is a tuple $\mathfrak {F} = \langle K, 0, R, * \rangle $ , where K is a non-empty set, $0 \subseteq K$ , $R \subseteq K^3$ , and $*$ is a unary function on K such that a list of postulates to follow are satisfied.

A binary relation on K is defined via $0$ and R by the definition:

$$ \begin{align*} a \leq b =_{df} \exists y \in 0(Ryab). \end{align*} $$

Given this definition, where $a, b, c, d \in K$ , the following postulates are satisfied by every B-frame:

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

2. (p2) $0$ is closed by $\leq $ in the upwards direction

3. (p3) if $a \leq b$ and $Rbcd$ then $Racd$

4. (p4) if $a \leq c$ and $Rbcd$ then $Rbad$

5. (p5) if $d \leq a$ and $Rbcd$ then $Rbca$

6. (p6) if $a \leq b$ then $b^* \leq a^{*}$

7. (p7) $a^{**} = a$

Using the ternary relation R, we can define a binary operation $\Rightarrow $ on the powerset $\wp (K)$ . For every $X, Y \subseteq K$ , let

$$ \begin{align*} X \Rightarrow Y = \{ a \in K: \forall x \forall y (Raxy \text{ and }x \in X \text{ implies } y \in Y) \}. \end{align*} $$

It can be shown that if X and Y are up-sets, then so is $X \Rightarrow Y$ , where up-sets are sets of worlds or situations closed under upwardly under the defined $\leq $ relation. That is, if $a \in X$ and $a \leq b$ implies $b \in X$ , then X is an up-set. A binary relation for fusion is defined such that, for every $X, Y \subseteq K$ ,

$$ \begin{align*} X \cdot Y = \{ a \in K: \exists b \exists c (Rbca \text{ and } b \in X \text{ and } c \in Y ) \}. \end{align*} $$

We can define a unary operation on subsets of $\wp (K)$ using the $*$ as follows. For every $X \subseteq K$

$$ \begin{align*} X^* = \{ a \in K: a^* \not \in X \}. \end{align*} $$

Similarly, if X is an up-set, then so is $X^*$ .

Definition 4.6. A B-model is a tuple $\mathfrak {M} = \langle K, 0, R, *, |{-}|^{\mathfrak {M}} \rangle $ , where $\langle K, 0, R, * \rangle $ is a B-frame and $|{-}|^{\mathfrak {M}}$ is a valuation that maps each atomic proposition to a up-set of K, and is extended to all wff inductively as follows:

$$ \begin{align*} |{{\mkern1mu\boldsymbol t}}|^{\mathfrak{M}} &= 0 \\ |\mathcal{A} \wedge \mathcal{B}|^{\mathfrak{M}} &= |\mathcal{A}|^{\mathfrak{M}} \cap |\mathcal{B}|^{\mathfrak{M}}\\ |\mathcal{A} \vee \mathcal{B}|^{\mathfrak{M}} &= |\mathcal{A}|^{\mathfrak{M}} \cup |\mathcal{B}|^{\mathfrak{M}}\\ |\neg \mathcal{A}|^{\mathfrak{M}} &= (|\mathcal{A}|^{\mathfrak{M}})^* \\ |\mathcal{A} \rightarrow \mathcal{B}|^{\mathfrak{M}} &= |\mathcal{A}|^{\mathfrak{M}} \Rightarrow |\mathcal{B}|^{\mathfrak{M}} \\ |\mathcal{A} \circ \mathcal{B}|^{\mathfrak{M}} &= |\mathcal{A}|^{\mathfrak{M}} \cdot |\mathcal{B}|^{\mathfrak{M}} \\ \end{align*} $$

Finally, we say that a formula $\mathcal {A}$ is true in the model $\mathfrak {M}$ if $0 \subseteq |\mathcal {A}|^{\mathfrak {M}}$ . $\mathcal {A}$ is valid on a frame if it is true in every model based on that frame, and $\mathcal {A}$ is valid in a class of frames if it is valid in every frame in that class.

General frame semantics, introduced in [Reference Thomason31] for modal logics, are a generalization of the usual Kripke-style relational frames, but are closely related to Boolean algebras with operators.Footnote ⁶ General frames are interesting for a number of reasons. Many find relational semantics quite intuitive, and the general frame semantics appear much like the typical relational semantics. However, they are also natural duals of algebras. This fact can be quite useful. For example, we can obtain completeness results for many modal logics using general frames and their dual algebras.

General frame add to the typical frames a restriction on the possible valuations. This set of admissible propositions, $Prop$ , can be described as “(the carrier of) a complex algebra over [the Kripke-style relation frame]” [Reference Blackburn, de Rijke and Venema3, p. 304]. Models are general frames with (admissible) valuations whose range is the set of admissible propositions. Validity and related notions are defined as expected. The canonical general frame can be constructed from the Kripke-style canonical frame on which it is based, taking the admissible propositions to be the sets of worlds containing each formula. We define the set of worlds containing $\mathcal {A}$ by $||\mathcal {A}||_{\mathfrak {C}}= \{a \in K : \mathcal {A} \in a \}$ , and then the admissible propositions in the canonical frame by $Prop = \{ ||\mathcal {A}||_{\mathfrak {C}} : \mathcal {A} \text { is a formula} \}$ . Or more simply we take $Prop_{\mathfrak {C}} = \{ |\mathcal {A}| : \mathcal {A}$ is a wff $\}$ .

Extending the general frame treatment to ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ , we thus get the following definition.

Definition 4.7. A general-B-frame is a tuple

$$\begin{align*}\mathfrak{F} = \langle K, 0, R, *, Prop\rangle,\end{align*}$$

where $\langle K, 0, R, * \rangle $ is a B-frame and $Prop$ is a subset of the up-sets of K called the admissible propositions which is closed under $\cap , \cup , \Rightarrow $ and $*$ and contains $0$ .

A model based on a general frame is given by a valuation that assigns to each propositional variable a member of $Prop$ . This is extended as before. Finally, truth in a model, a frame, and a class of frames is defined as usual.

The canonical general frame is obtained from the canonical frame as follows. We obtain $Prop_{\mathfrak {C}}$ by setting $Prop_{\mathfrak {C}} = \{ |\mathcal {A}| : \mathcal {A}$ is a wff $\}$ .

4.2 Propositions

The propositions in the models for relevant logics are sets of situations closed under $\leq $ , and are often called hereditary sets or up-sets. The relations between situations, such as $R, *$ , and $\cap $ , are type-lifted to propositions. Already we have seen the operations $\Rightarrow $ and $*$ . Operations $\cap $ and $\cup $ are defined as expected. Here is a list of all the remaining operations of propositions corresponding to the connectives of ${\bf QB}.{\bf C}_{\Box \Diamond }$ . The operations $\Box $ and $\Diamond $ responding to $S_\Box $ and $S_\Diamond $ , given by their usual definitions in general frames, are not to be confused with the unary connectives of the logic using the same symbol. For $X, Y \in \wp (K)$

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

2. $\Diamond X = \{a \in K: \exists b (S_\Diamond a b \ \& \ b \in X) \}.$

To model the quantifiers, Mares and Goldblatt introduce operations from sets of sets of situations to sets of situations. That is, from sets of propositions to propositions. This operation is determined by $Prop$ . When $Prop$ is a set of hereditary subsets of possible worlds, an operation $\sqcap $ of type $\sqcap :\wp \wp K\longrightarrow \wp K$ such that, for every $S \subseteq \wp K$

$$ \begin{align*} \sqcap S = \cup \{X\in Prop: X \subseteq \cap S \}. \end{align*} $$

Additionally, an operation $\sqcup $ of the same type is defined by:

$$ \begin{align*} \sqcup S= \cap\{ X \in Prop : \cup S \subseteq X \} \end{align*} $$

for every $S \subseteq \wp K$ .

The $\sqcap $ is explained as being “motivated by the intuition that the sentence $\forall x \phi $ expresses the conjunction of all the sentences $\phi [a/x]$ ” [Reference Goldblatt11, p. 17]. The problem with using the arbitrary conjunction of the sentences $\phi [a/x]$ is that this conjunction is not guaranteed to be admissible. We only guarantee that the binary conjunction of two members of $Prop$ is also in $Prop$ . Thus, Goldblatt explains that a notion of entailment between propositions (of the sort considered) will work in this case. First, given our notion of proposition, a proposition X entails a proposition Y if $X \subseteq Y$ , for whenever you have a world at which X is true, Y is also true. Goldblatt also calls Y weaker than X, and X stronger than Y [Reference Goldblatt11, p. 17]. Next, the operation is similar enough to the arbitrary conjunction of a collection of elements of $Prop$ is a member of $Prop$ that entails every member of the collection. In particular, it is the weakest member of $Prop$ that entails every member of the collection. That is, for a collection of members of $Prop \ \{X_i: i \in I \}$ , the proposition sufficiently expressing their conjunction is the X in $Prop$ such that,

(i) $X \subseteq X_i$ for each $i \in I$ and

(ii) if $Z \in Prop$ and $Z \subseteq X_i$ for all $i \in I$ , then $Z \subseteq X$ [Reference Goldblatt11, p. 17]

The key point here is that this conjunction-like operation always results in a subset of $\cap _{i \in I} X_i$ , but not necessarily identical. The latter ( $\cap $ ) is not guaranteed to be a member of $Prop$ , while we require that the former ( $\sqcap $ ) is. This conjunction-like operator is denoted by $\sqcap _{i \in I}X_i$ .

Similarly, we can think of $\sqcup $ as expressing the strongest member of $Prop$ that is entailed by every member. More explicitly, using this to model the existential quantifier intuitively expresses that the proposition corresponding to $\exists x \mathcal {A}$ is the strongest proposition implied by every instantiation of the formula.

The following lemma is crucial, as it entails that on the Mares–Goldblatt approach using $\sqcap $ or $\sqcup $ any quantified relevant logic extending ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ is sound and complete for the Mares–Goldblatt models. The reader is reminded that the duality of the modalities $\Box $ and $\Diamond $ break down over the weak ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ , while the duality of the quantifiers is provable in ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ .

Lemma 4.8. Given only the properties of $\cap , \cup $ , and $*$ in ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ ,

1. 1. $\sqcup S = (\sqcap (S^*))^*$

2. 2. $\sqcap S = (\sqcup (S^*))^*$

Proof. Mares and Goldblatt prove the $\sqcup S = (\sqcap (S^*))^*$ for ${\bf RQ}^{\circ { {\mkern 1mu\boldsymbol t}}}$ . By expanding the details of their proof, the lemma follows by observing that their proof uses only the classicality of $\cap $ and $\cup $ , and properties of $*$ available to us in ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ . In particular, the steps of the proof involving $*$ are are follows. First, demonstrating that $(\cup S)^* = \cap \{ X^* : X \in S \}$ , which uses the fact that $a = {a^*}^*$ . Second, showing that $ - X \subseteq Y$ iff $-Y \subseteq X$ , which uses the fact that $a = b^*$ iff $a^* = b$ .

Propositional Functions

Propositional functions, on the other hand, are functions from value assignments for variables to admissible propositions. In addition to using a set $Prop$ of admissible propositions, Mares and Goldblatt also use a set $PropFun$ of admissible propositional functions.

A propositional function for classical logic is a function from value assignments for the variables into the set $\{ True, False\}$ , where a proposition is either true or false. For logics with possible world semantics, propositional functions are functions into the set of propositions, where propositions are taken to be a subset of the powerset of worlds. For example, consider the propositional function x is a human. The result of applying this function to a value assignment to the variables that assigns to x the object Socrates is a proposition. In classical logic, this application of a function would result in either $True$ or $False$ . In the case of quantified relevant logic, this function application returns the set of upwardly closed worlds in which “Socrates is a human” is true.

A propositional function in the context of the semantics of Mares and Goldblatt is a function from value assignments of the variables to admissible propositions. That is, a propositional function $\phi $ is of type $\phi $ : $U^\omega \longrightarrow Prop$ , where U is the domain of individuals in a model. While admissible propositional functions are required for the semantics of ${\bf RQ}^{\circ { {\mkern 1mu\boldsymbol t}}}$ , motivations for adopting admissible propositions can be turned into motivations for admissible propositional functions.

Definition 4.9. For any two elements $\phi $ and $\psi $ of $PropFun$ , the functions $\phi \cap \psi , \phi \cup \psi , \phi ^*, \phi \Rightarrow \psi , \phi \cdot \psi ,\Box \phi , \Diamond \phi , \forall _n \phi $ and $\exists _n \phi $ of the same type are defined by, for every value assignment to the variables $f \in U^\omega $ :

$$ \begin{align*} (\phi \cap \psi)f &= \phi f \cap \psi f \\ (\phi \cup \psi)f &= \phi f \cup \psi f \\ (\phi^*) f &= (\phi f)^* \\ (\phi \Rightarrow \psi)f &= \phi f \Rightarrow \psi f \\ (\phi \cdot \psi)f &= \phi f \cdot \psi f \\ (\Box \phi)f &= \Box (\phi f)\\ (\Diamond \phi)f &= \Diamond (\phi f)\\ (\forall_n \phi)f &= \underset{j \in I}{\sqcap} \phi(f[j/n]) \\ (\exists_n \phi)f &= \underset{j \in I}{\sqcup} \phi(f[j/n]) \end{align*} $$

4.3 First order relevant logics

The Mares–Goldblatt semantics has yet been shown to apply to propositional relevant logics weaker than ${\bf QR}^{\circ { {\mkern 1mu\boldsymbol t}}}$ . While Goldblatt and Kane’s use of this semantic approach for propositionally quantified relevant logics in [Reference Goldblatt and Kane13] is highly suggestive, here I show that the Mares–Goldblatt semantics works for ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ and ${\bf BQ}^{\circ { {\mkern 1mu\boldsymbol t}}}$ , and their extensions.

Definition 4.10. A ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ frame is a tuple

$$\begin{align*}\mathfrak{F} = \langle K, 0, R, *, U, Prop, PropFun \rangle, \end{align*}$$

where $\langle K, 0, R, * \rangle $ is an ${\bf B}$ -frame, U is a non-empty set, $Prop$ is a subset of the up-sets of K which contains $0$ , $PropFun$ is a subset of the functions of type $U^\omega \longrightarrow Prop$ , and the following conditions are satisfied:

• (c1)  if $a \in 0$ and $a \leq b$ then $b \in 0$ ;

• (c2)  $\leq $ is reflexive and transitive;

• (c3)  if $a \leq b $ and $Rbcd$ , then $Racd$ ;

• (c4)  if $a \leq c $ and $Rbcd$ , then $Rbad$ ;

• (c5)  if $ d \leq a $ and $Rbcd$ , then $Rbca$ ;

• (c6)  if $a \leq b$ then $b^* \leq a^*$ ;

• (c7)  $a^{**}=a$ ;

• (c8)  if $X, Y \in Prop$ , then $X \cup Y$ , $X \cap Y$ , $X \Rightarrow Y$ , $X \cdot Y$ , $X^* \in Prop$ , where these operations are defined as before;

• (c9)  the constant function $\phi _0$ is in $PropFun$ ;

• (c10)  if $\phi , \psi \in PropFun$ , then $\phi \cup \psi $ , $\phi \cap \psi $ , $\phi \Rightarrow \psi $ , $\phi ^* \in PropFun$ ; and

• (c11)  if $\phi \in PropFun$ , then $\exists _n \phi $ , $\forall _n \phi \in PropFun$ , for every $n \in \omega $ .

Using condition c4, and the fact that $0$ is an up-set, we can derive the transitivity requirements of $\leq $ . A ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ -frame is called full if the set $Prop$ contains every hereditary subset of K, and $PropFun$ contains every function from $U^\omega $ to $Prop$ .

Definition 4.11. A pre-model for ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ is a tuple

$$\begin{align*}\mathfrak{M} = \langle K, 0, R, *, U, Prop, PropFun, |{-}|^{\mathfrak{M}} \rangle, \end{align*}$$

where $\langle K, 0, R, *, U, Prop, PropFun \rangle $ is a ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ -frame and $|{-}|^{\mathfrak {M}}$ is a value assignment that assigns

1. 1. an element $|c|^{\mathfrak {M}} \in U$ to each constant symbol c;

2. 2. a function $|P|^{\mathfrak {M}} :U^n \longrightarrow \wp (K)$ to each n-ary predicate symbol P; and

3. 3. a propositional function $|\mathcal {A}|^{\mathfrak {M}} : U^{\omega } \longrightarrow \wp (K)$ to each formula $\mathcal {A}$ such that, when $\mathcal {A}$ is the atomic $P\tau _1, \dots , \tau _n$ , the propositional function assigned to it is given by, for each $f \in U^{\omega }$ ,

   $$\begin{align*}|P\tau_1, \dots, \tau_n|^{\mathfrak{M}} f = |P|^{\mathfrak{M}} (|\tau_1|^{\mathfrak{M}} f, \dots, |\tau_n|^{\mathfrak{M}} f).\end{align*}$$

Further, when $\mathcal {A}$ is not atomic, the function assigned to the formula is given by the following:

$$ \begin{align*} |{{\mkern1mu\boldsymbol t}}|^{\mathfrak{M}} &= \phi_0 \\ |\mathcal{A} \wedge \mathcal{B} |^{\mathcal{M}} &= |\mathcal{A}|^{\mathcal{M}} \cap |\mathcal{B} |^{\mathcal{M}} \\ |\mathcal{A} \vee \mathcal{B} |^{\mathcal{M}} &= |\mathcal{A}|^{\mathcal{M}} \cup |\mathcal{B} |^{\mathcal{M}} \\ |\neg \mathcal{A}|^{\mathcal{M}} &= (|\mathcal{A}|^{\mathcal{M}})^*\\ |\mathcal{A} \rightarrow \mathcal{B} |^{\mathcal{M}} &= |\mathcal{A}|^{\mathcal{M}} \Rightarrow |\mathcal{B} |^{\mathcal{M}} \ \ \ \ \ \ \ \ \ \ \\ |\mathcal{A} \circ \mathcal{B} |^{\mathcal{M}} &= |\mathcal{A}|^{\mathcal{M}} \cdot |\mathcal{B} |^{\mathcal{M}} \ \ \ \ \ \ \ \ \ \ \\ |\forall x_n \mathcal{A}|^{\mathcal{M}} &=\forall_n |\mathcal{A}|^{\mathcal{M}} \\ |\exists x_n \mathcal{A}|^{\mathcal{M}} &=\exists_n |\mathcal{A}|^{\mathcal{M}}. \end{align*} $$

Definition 4.12. A model for ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ is a pre-model for ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ that assigns a member of $PropFun$ to each atomic formula.

The following theorems are provable using the arguments from later sections of the paper, ignoring the modal machinery. The proofs are only given in later sections to avoid unnecessary repetition.

Theorem 4.13 (Soundness).

All of the theorems of ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ ( ${\bf BQ}^{\circ { {\mkern 1mu\boldsymbol t}}}$ ) are valid in every ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ -model ( ${\bf BQ}^{\circ { {\mkern 1mu\boldsymbol t}}}$ -model).

Theorem 4.14 (Completeness for QB∘ t (BQ∘ t )).

If $\mathcal {A}$ is valid in every ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ -model ( ${\bf BQ}^{\circ { {\mkern 1mu\boldsymbol t}}}$ -model), then $\mathcal {A}$ is a theorem of ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ ( ${\bf BQ}^{\circ { {\mkern 1mu\boldsymbol t}}}$ ).

Let $\mathbb {L}$ be a propositional relevant logic extending ${\bf B}^{\circ { {\mkern 1mu\boldsymbol t}}}$ . We may define $\mathbb {L}$ Q and Q $\mathbb {L}$ by adding frame conditions for the relevant logic fragment.

Corollary 4.15. The logic $\mathbb {L}$ Q (Q $\mathbb {L}$ ) is sound and complete for the $\mathbb {L}$ Q-models (Q $\mathbb {L}$ -models).

Table 1 contains a list of some common axioms for propositional relevant logics and their corresponding frame conditions.

Table 1 Frame conditions for axioms of relevant logics

^a A more complete treatment of axioms and their corresponding frame conditions can be found in [Reference Routley, Plumwood, Meyer and Brady27], particularly in Sections 4.1 and 4.4.

4.4 Frames and Models for ${\bf QB}.{\bf C}_{\Box \Diamond }$ and ${\bf BQ}.{\bf C}_{\Box \Diamond }$

Definition 4.16. A ${\bf QB}.{\bf C}_{\Box \Diamond }$ frame is a tuple

$$\begin{align*}\mathfrak{F} = \langle K, 0, R, *, S_{\Box}, S_{\Diamond}, U, Prop, PropFun \rangle, \end{align*}$$

where $\langle K, 0, R, *, U, Prop, PropFun \rangle $ is an ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ -frame, $S_{\Box }, S_{\Diamond } \subseteq K^2$ , U is a non-empty set, $Prop$ is a subset of the up-sets of K which contains $0$ , $PropFun$ is a subset of the functions of type $U^\omega \longrightarrow Prop$ , and the following conditions are satisfied:

• (c12a)  if $a \leq b$ and $S_\Box bc$ then $S_\Box ac$ ;

• (c12b)  if $a \leq b$ and $S_\Diamond ac$ then $S_\Diamond bc$ ;

• (c13) if $X \in Prop$ , then $\Box X, \Diamond X \in Prop$ ; and

• (c14) if $\phi \in PropFun$ , then $\Box \phi $ , $\Diamond \phi \in PropFun$ .

A ${\bf QB}.{\bf C}_{\Box \Diamond }$ -frame is called full if the set $Prop$ contains every hereditary subset of K, and $PropFun$ contains every function from $U^\omega $ to $Prop$ .

Definition 4.17. A pre-model for ${\bf QB}.{\bf C}_{\Box \Diamond }$ is a tuple

$$\begin{align*}\mathfrak{M} = \langle K, 0, R, *, S_{\Box}, S_{\Diamond}, U, Prop, PropFun, |{-}|^{\mathfrak{M}} \rangle, \end{align*}$$

where $\langle K, 0, R, *, S_{\Box }, S_{\Diamond }, U, Prop, PropFun \rangle $ is a ${\bf QB}.{\bf C}_{\Box \Diamond }$ -frame and where $|{-}|^{\mathfrak {M}}$ is a value assignment as in definition 4.11, with the exceptions/additions that

$$ \begin{align*} |\Box \mathcal{A}|^{\mathcal{M}} &= \Box|\mathcal{A}|^{\mathcal{M}},\\ |\Diamond \mathcal{A}|^{\mathcal{M}} &= \Diamond|\mathcal{A}|^{\mathcal{M}}.\\ \end{align*} $$

Definition 4.18. A model for ${\bf QB}.{\bf C}_{\Box \Diamond }$ is a pre-model for ${\bf QB}.{\bf C}_{\Box \Diamond }$ that assigns a member of $PropFun$ to each atomic formula.

As shown by Seki [Reference Seki30], binary relations for the dual modalities $\diamond\kern-4pt\cdot$ and $\boxdot $ can be defined by, for every $a, b \in K$ :

1. $S_{\diamond\kern-2.7pt\cdot} ab \text { iff } S_\Box a^*b^*,$

2. $S_\boxdot ab \text { iff } S_\Diamond a^*b^*.$

Given the functions determined by a (pre-)model, we can then consider the truth sets of each function as it is applied to a variable assignment. These truth sets are given, for each $f \in U^\omega $ , as follows:

$$ \begin{align*} |{{\mkern1mu\boldsymbol t}}|^{\mathcal{M}}f&= 0 \\ |\mathcal{A} \wedge \mathcal{B} |^{\mathcal{M}}f &= |\mathcal{A}|^{\mathcal{M}}f \cap |\mathcal{B} |^{\mathcal{M}}f \\ |\mathcal{A} \vee \mathcal{B} |^{\mathcal{M}}f &= |\mathcal{A}|^{\mathcal{M}}f \cup |\mathcal{B} |^{\mathcal{M}}f \\ |\neg \mathcal{A}|^{\mathcal{M}}f &= (|\mathcal{A}|^{\mathcal{M}}f)^*\\ |\mathcal{A} \rightarrow \mathcal{B} |^{\mathcal{M}}f &= |\mathcal{A}|^{\mathcal{M}}f \Rightarrow |\mathcal{B} |^{\mathcal{M}}f \\ |\mathcal{A} \circ \mathcal{B} |^{\mathcal{M}}f &= |\mathcal{A}|^{\mathcal{M}}f \cdot |\mathcal{B} |^{\mathcal{M}}f \\ |\Box\mathcal{A}|^{\mathcal{M}}f &= \Box(|\mathcal{A}|^{\mathcal{M}}f)\\ |\Diamond\mathcal{A}|^{\mathcal{M}}f &= \Diamond(|\mathcal{A}|^{\mathcal{M}}f)\\ |\forall x \mathcal{A}|^{\mathcal{M}}f &=\sqcap_{g \in xf} |\mathcal{A}|^{\mathcal{M}}g \\ |\exists x \mathcal{A}|^{\mathcal{M}}f &=\sqcup_{g \in xf} |\mathcal{A}|^{\mathcal{M}}g. \end{align*} $$

Finally, a familiar looking $\vDash _{\mathfrak {M}}$ relation — or simply $\vDash $ for convenience — is determined as follows:

• (i) $ a, f \vDash P\tau _1, \dots , \tau _n$ iff $a \in |P\tau _1, \dots , \tau _n|^{\mathfrak {M}}f$

• (ii) $a, f \vDash { {\mkern 1mu\boldsymbol t}}$ iff $a \in 0$

• (iii) $a, f \vDash \mathcal {A} \wedge \mathcal {B}$ iff $a, f \vDash \mathcal {A}$ and $a, f \vDash \mathcal {B}$

• (iii) $a, f \vDash \mathcal {A} \vee \mathcal {B}$ iff $a, f \vDash \mathcal {A}$ or $a, f \vDash \mathcal {B}$

• (iv) $a, f \vDash \neg \mathcal {A}$ iff $a^*, f \not \vDash \mathcal {A}$

• (v) $ a, f \vDash \mathcal {A} \rightarrow \mathcal {B}$ iff $\forall b, c ((Rabc \text { and }b, f \vDash \mathcal {A})\Rightarrow c, f \vDash \mathcal {B})$

• (v) $ a, f \vDash \mathcal {A} \circ \mathcal {B}$ iff $\exists b, c (Rbca \text { and }b, f \vDash \mathcal {A} \text { and } c, f \vDash \mathcal {B})$

• (vi) $a, f \vDash \Box \mathcal {A}$ iff $\forall b (S_\Box a b \Rightarrow b, f \vDash \mathcal {A})$

• (vii) $a, f \vDash \Diamond \mathcal {A}$ iff $\exists b (S_\Diamond a b \ { {\mathbin {\&}}} \ b, f \vDash \mathcal {A})$

• (viii) $a, f \vDash \forall x \mathcal {A}$ iff there is an $X \in Prop$ such that $X \subseteq \underset {g \in x_nf}{\bigcap }|\mathcal {A}|^{\mathfrak {M}}g$ and $a \in X$

• (ix) $a, f \vDash \exists x \mathcal {A} $ iff, for every $X \in Prop$ such that $a^* \in X$ , there is a $b \in X$ and x-variant such that $b^* \in |\mathcal {A}|^{\mathfrak {M}}g$

Cases (viii) and (ix) are as they are in [Reference Mares and Goldblatt20].

A formula $\mathcal {A}$ is satisfied by a variable assignment f in a model $\mathfrak {M}$ if $a, f \vDash \mathcal {A}$ , for every $a \in 0$ . A formula $\mathcal {A}$ is valid in the model $\mathfrak {M}$ , if it is satisfied by every variable assignment in that model. A formula $\mathcal {A}$ is valid in a frame, if it is valid in every model based on the frame. Further, a formula is valid is a class of frames, if it is valid in every frame in the class.

Definition 4.19. For the logic ${\bf BQ}.{\bf C}_{\Box \Diamond }$ , frames and models are defined as above, with the addition for the following frame condition:

1. c15 $X-Y\subseteq \cap _{a \in U}\phi (f[a/n])$ implies $X-Y \subseteq (\forall _n\phi )f.$

As the extensional confinement axioms are equivalent in ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ , and this single frame condition taken from [Reference Mares and Goldblatt20] is sufficient for the validity (and for completeness results).

The following lemmas are useful in establishing soundness results. When unspecified, the lemmas apply to both ${\bf QB}.{\bf C}_{\Box \Diamond }$ and ${\bf BQ}.{\bf C}_{\Box \Diamond }$ .

Lemma 4.20 (Semantic Entailment).

In a model $\mathfrak {M}$ , a formula $\mathcal {A} \rightarrow \mathcal {B}$ is satisfied by the variable assignment f iff for every $a \in K$ , if $a, f \vDash \mathcal {A}$ , then $a, f \vDash \mathcal {B}$ .

Proof. The original statement of this lemma (for a propositional relevant logic) and its proof can be found as Lemmas 2 and 3 in [Reference Routley, Meyer and Leblanc26].

Lemma 4.21. For any formula $\mathcal {A}$ , if f and g agree on all free variable of $\mathcal {A}$ , then $|\mathcal {A}|f = |\mathcal {A}|g$ .

Proof. The proof is by induction on the complexity of $\mathcal {A}$ . The arguments of Mares and Goldblatt may be used for most cases. The remaining cases are shown here.

If $\mathcal {A} = \exists x_n \mathcal {B}$ , then a variable in $\mathcal {B}$ is free if either it is free in $\mathcal {A}$ or it is the variable $x_n$ . It follows that for every $j \in U$ , $f[j/n]$ and $g[j/n]$ agree on all free variables of $\mathcal {B}$ . By the induction hypothesis, we get that $|\mathcal {B}|f[j/n]=|\mathcal {B}|g[j/n]$ , and thus

$$ \begin{align*}|\mathcal{A}|f =\sqcup_{j \in I}|\mathcal{B}|f[j/n] = \sqcup_{j \in I}|\mathcal{B}|g[j/n] = |\mathcal{A}|g,\end{align*} $$

as required.

If $\mathcal {A} = \Box \mathcal {B}$ , then $|\Box \mathcal {B}|f = \Box |\mathcal {B}|f$ . By the induction hypothesis $|\mathcal {B}|f = |\mathcal {B}|g$ , so $\Box |\mathcal {B}|f = \Box |\mathcal {B}|g$ . The case of $\mathcal {A} = \Diamond \mathcal {B}$ is similar to the case for $\Box $ .

Lemma 4.22. Let $\tau $ be free for x in a formula $\mathcal {A}$ . If $g \in xf$ and $|x|g = |\tau |f$ , then $|\mathcal {A}[\tau /x]|f = |\mathcal {A}|g$ in a model $\mathfrak {M}$ .

Proof. The proof is by induction on the complexity of $\mathcal {A}$ . The arguments of Mares and Goldblatt [Reference Mares and Goldblatt20, p. 177] can be used for all cases except for $\mathcal {A} = \Box \mathcal {B}$ , $\mathcal {A} = \Diamond \mathcal {B}$ , and $\mathcal {A} = \exists x \mathcal {B}$ . Here I show this remaining case.

Let $\mathcal {A} = \Box \mathcal {B}$ and assume the result holds for $\mathcal {B}$ . If x is free for $\tau $ in $\Box \mathcal {B}$ , then x is free for $\tau $ in $\mathcal {B}$ . By the induction hypothesis, $|\mathcal {B}[\tau /x]|f = |\mathcal {B}|g$ . Thus, $\Box |\mathcal {B}[\tau /x]|f = \Box |\mathcal {B}|g$ . From this we get that $|\Box \mathcal {B}[\tau /x]|f = |\Box \mathcal {B}|g$ , as required.

The case for $\mathcal {A} = \Diamond \mathcal {B}$ is similarly straightforward.

For $\mathcal {A} = \exists x \mathcal {B}$ , the proof is obtained by modifying the Mares–Goldblatt proof for the universal quantifier case. Assume that the result holds for $\mathcal {B}$ as the induction hypothesis. Either x is free in $\mathcal {A}$ or it isn’t. If it isn’t, then $\mathcal {A}[\tau /x]=\mathcal {A}$ . Since g is an x-variant of f, the result is immediate.

On the other hand, if x is free in $\mathcal {A}$ , then $x \neq y$ . Further, $\mathcal {A}[\tau /x] = \exists y \mathcal {B}[\tau /x]$ . Because x is free for $\tau $ , it follows that $y \neq \tau $ and x is free for $\tau $ in $\mathcal {B}$ . Let y be the variable $x_n$ . We have the following identities:

$$ \begin{align*} |\mathcal{A}[\tau/x]|^{\mathfrak{M}} f &= \sqcup_{i \in U} |\mathcal{B}[\tau/x]|^{\mathfrak{M}} f[i/n],\\ |\mathcal{A}|^{\mathfrak{M}} g &= \sqcup_{i \in U} |\mathcal{B}|^{\mathfrak{M}} g[i/n]. \end{align*} $$

To complete the proof we show that the two right sides are identical, as in the previous case.

Again, note that for any $i \in U$ , the assignment $f[i/n]$ is an x-variant of $g[i/n]$ , as they are x-variants before the substitution, and the substitution is applied to each of them. From $x_n \neq \tau $ and $x \neq x_n$ it follows that $|\tau |f[i/n] = |\tau |f = |x|g = |x|g[i/n]$ . Using the induction hypothesis we get that

$$\begin{align*}|\mathcal{B}[\tau/x]|^{\mathfrak{M}} f[i/n] = |\mathcal{B}|^{\mathfrak{M}} g[i/n]. \end{align*}$$

The proof is completed as in the previous case, thus concluding the induction.

5 Soundness

The proof of this is standard using the typical methods. The interesting cases for soundness are the axioms and rules with quantifiers and modalities.

Proof. The proofs for (A10) and (A11) are similar. The arguments from Mares and Goldblatt [Reference Mares and Goldblatt20] can be used for the case of (A10). That is, their proof is does not use any requirements beyond what is available for for ${\bf QB}^{\circ { {\mkern 1mu\boldsymbol t}}}$ -models. Thus, I will only show the case for (A11), which is similar.

Let $a, f \vDash \mathcal {A}[\tau /x]$ and let $\tau $ be free for x in $\mathcal {A}$ . That is, that $a \in |\mathcal {A}[\tau /x]|^{\mathfrak {M}}f $ . Let g be an x-variant of f such that $|x|g = |\tau |f$ . It follows that $a, g \vDash \mathcal {A}$ . That is, $| \mathcal {A}[\tau /x]|f = | \mathcal {A}|g$ . Thus, $a \in | \mathcal {A}|g$ . It follows that $a \in \cup _{g \in xf}| \mathcal {A}|g$ . Thus, a is in every proposition X such that $\cup _{g \in xf}| \mathcal {A}|g \subseteq X$ . Therefore $a \in \sqcup _{g \in xf}| \mathcal {A}|g$ . By Semantic Entailment the axiom (A11) is valid.

For (A14), the proof is made simpler using the duality of the quantifiers, and prove that $\vDash \forall x (\mathcal {A} \rightarrow \mathcal {B})\rightarrow (\neg \forall x \neg \mathcal {A} \rightarrow \mathcal {B})$ where x is not free in $\mathcal {B}$ . Assume that this is not the case. Then (i) $a, f, \vDash \forall x (\mathcal {A} \rightarrow \mathcal {B})$ , (ii) $Rabc$ , (iii) $b, f \vDash \neg \forall x \neg A$ and (iv) $c, f \not \vDash \mathcal {B}$ . Thus, (v) $a \in |\mathcal {A} \rightarrow \mathcal {B}|g$ for all $g \in xf$ . From (ii), we get that

$$ \begin{align*} b, f \vDash \neg \forall \neg \mathcal{A} &\text{ iff } b*, f \not \vDash \forall x \neg \mathcal{A} \\ &\text{ iff } b* \not \in \sqcap_{g \in xf} |\neg \mathcal{A}|g\\ &\text{ iff } b* \not \in |\neg \mathcal{A}|g' \text{ for some particular }g' \in xf\\ &\text{ iff } b*, g' \not \vDash \neg \mathcal{A} \\ &\text{ iff }b, g' \vDash \mathcal{A.} \end{align*} $$

Given the last fact, (ii), and (v), we get $c, g' \vDash \mathcal {B}$ . Moreover, since there are no free occurrences of x in $\mathcal {B}$ , we obtain our contradiction with $c, f \vDash \mathcal {B}$ and (iv). Thus, the result follows by Semantic Entailment.

In summary, I record that:

6 Theories

For notational convenience, let $\Gamma \gg _{\mathbb {L}} \Delta $ mean that there are some $\mathcal {A}_1, \dots , \mathcal {A}_n \in \Gamma $ and $\mathcal {B}_1, \dots , \mathcal {B}_m \in \Delta $ such that $\vdash _{\mathbb {L}}(\mathcal {A}_1\wedge \dots \wedge \mathcal {A}_n)\rightarrow (\mathcal {B}_1 \vee \dots \vee \mathcal {B}_m)$ , where $\Gamma $ and $\Delta $ are sets of formulas and $\mathbb {L}$ is a logic.

Finally, the extension lemma, is needed to show that, if a formula is not a theorem, then there is a regular prime theory that does not contain the formula.

The proof of this lemma for the logic ${\bf RQ}$ is due to Belnap (but the result is unpublished) [Reference Dunn, Restall, Gabbay and Guenthner7, p. 41]. Roughly, one way to prove this lemma is to take the closure of $\Delta $ under disjunction, and consider all theories extending $\Gamma $ that do not include any element of the closure of $\Delta $ . We apply Zorn’s lemma to get a maximal theory, and then prove that it is prime.

7 Completeness

The proof of completeness for ${\bf QB}.{\bf C}_{\Box \Diamond }$ and ${\bf BQ}.{\bf C}_{\Box \Diamond }$ in this section will again follow Mares and Goldblatt, making adjustments where appropriate for the added necessity operator. I will take the usual detour through theories in what Mares and Goldblatt call a “Henkin–Lemmon–Scott–Routley–Meyer canonical model construction” [Reference Mares and Goldblatt20], p. 178. For the construction of a canonical model, we either assume that the set of constants $Con$ is denumerable, or we add a denumerable number of constants to the set $Con$ in the usual way.

Let $K^{\prime}_{\mathfrak {C}} $ be the set of all ${\bf QB}.{\bf C}_{\Box \Diamond }$ -theories, and let $R'$ , $S_{\Box }$ , and $S_{\Diamond }$ be defined on $K^{\prime}_{\mathfrak {C}} $ as in definition 6.34, with $\mathbb {L} = {\bf QB}.{\bf C}_{\Box \Diamond }$ .

Definition 7.35. A canonical frame for ${\bf QB}.{\bf C}_{\Box \Diamond }$ is a tuple,

$$\begin{align*}\mathfrak{F}_{\mathfrak{C}} = \langle K_{\mathfrak{C}}, 0_{\mathfrak{C}}, R_{\mathfrak{C}}, *_{\mathfrak{C}}, S_{\Box \mathfrak{C}}, S_{\Diamond \mathfrak{C}}, U_{\mathfrak{C}}, Prop_{\mathfrak{C}}, PropFun_{\mathfrak{C}} \rangle \end{align*}$$

where

• • $K_{\mathfrak {C}} \subseteq K^{\prime}_{\mathfrak {C}} $ is the set of all prime ${\bf QB}.{\bf C}_{\Box \Diamond }$ -theories.

• • $0_{\mathfrak {C}} $ is the set of all regular prime ${\bf QB}.{\bf C}_{\Box \Diamond }$ -theories.

• • $R_{\mathfrak {C}} $ is the relation $R'$ restricted to $K_{\mathfrak {C}}$ .

• • $S_{\Box \mathfrak {C} }$ is the relation $S_{\Box }$ restricted to $K_{\mathfrak {C}} $ .

• • $S_{\Diamond \mathfrak {C} }$ is the relation $S_{\Diamond }$ restricted to $K_{\mathfrak {C}} $ .

• • $*_{\mathfrak {C}} $ is defined by $a^* = \{ \mathcal {A} : \neg \mathcal {A} \not \in a \}$ .

• • $U_{\mathfrak {C}} $ is the infinite set of constants Con.

• • For every closed formula $\mathcal {A}$ , $||\mathcal {A}||_{\mathfrak {C}} $ is defined to be the set $\{a \in K : \mathcal {A} \in a \}$ .

• • $Prop_{\mathfrak {C}} $ is defined as the set $\{ ||\mathcal {A}||_{\mathfrak {C}} :\mathcal {A} \text { is a closed formula} \}$ .

• • Given a variable assignment f, the value $fn$ is a constant. Substituting each variable in a formula $\mathcal {A}$ with the constant assigned to it by a variable assignment f results in a closed formula which will be denoted $\mathcal {A}^f$ . Therefore $\mathcal {A}^f = \mathcal {A}[f0/x_0, \dots , fn/x_n, \dots ]$ .

• • To each formula $\mathcal {A}$ , there is a corresponding function $\phi _{\mathcal {A}}$ of type $U^\omega \longrightarrow K$ given by $\phi _{\mathcal {A}}f = ||\mathcal {A}^f||_{\mathfrak {C}} $ . $PropFun_{\mathfrak {C}} $ is the set of all functions $\phi _{\mathcal {A}}$ , where $\mathcal {A}$ is a formula.

Definition 7.36. A canonical model for ${\bf QB}.{\bf C}_{\Box \Diamond }$ is a tuple,

$$\begin{align*}\mathfrak{M}_{\mathfrak{C}} = \langle K_{\mathfrak{C}} , 0_{\mathfrak{C}} , R_{\mathfrak{C}} , *_{\mathfrak{C}} , S_{\Box \mathfrak{C} }, S_{\Diamond \mathfrak{C} }, U_{\mathfrak{C}} , Prop_{\mathfrak{C}} , PropFun_{\mathfrak{C}} , |{-}|^{\mathfrak{M}}_{\mathfrak{C}} \rangle \text{, where}\ \end{align*}$$

• • $\langle K_{\mathfrak {C}} , 0_{\mathfrak {C}} , R_{\mathfrak {C}} , S_{\Box \mathfrak {C} }, *_{\mathfrak {C}} , U_{\mathfrak {C}} , Prop_{\mathfrak {C}} , PropFun_{\mathfrak {C}} \rangle $ is the canonical frame.

• • $|c|_{\mathfrak {C}} = c$ , for every constant symbol c.

• • $|P|_{\mathfrak {C}} (c_0, \dots , c_n) = ||P(c_0, \dots , c_n)||_{\mathfrak {C}} $ .

• • The valuation is extended to every wff as before.

Of the following squeeze lemmas for $R_{\mathfrak {C}} , S_{\Box \mathfrak {C} }$ , and $S_{\Diamond \mathfrak {C} }$ , the former has a fairly standard proof. The proof of the latter two can be found in [Reference Seki30]. Here, the proofs are omitted.

The conditions c1–c7 can be shown to hold by the usual arguments, which will also demonstrate that $\langle K_{\mathfrak {C}}, 0_{\mathfrak {C}}, R_{\mathfrak {C}}, *_{\mathfrak {C}} \rangle $ is a ${\bf B}$ -frame and that $a \leq b$ iff $a \subseteq b$ .

Proof. It is sufficient to show that the following equalities hold.

$$ \begin{align*} ||\neg \mathcal{A}^f||_{\mathfrak{C}} &= ||\mathcal{A}^f||^*_{\mathfrak{C}} \\ ||\mathcal{A} \vee \mathcal{B}^f||_{\mathfrak{C}} &= ||\mathcal{A}^f ||_{\mathfrak{C}} \cup ||\mathcal{B}^f||_{\mathfrak{C}} \\ ||\mathcal{A} \wedge \mathcal{B}^f||_{\mathfrak{C}} &= ||\mathcal{A}^f ||_{\mathfrak{C}} \cap ||\mathcal{B}^f||_{\mathfrak{C}} \\ ||\mathcal{A} \circ \mathcal{B}^f||_{\mathfrak{C}} &= ||\mathcal{A}^f ||_{\mathfrak{C}} \cdot ||\mathcal{B}^f||_{\mathfrak{C}} \\ ||\mathcal{A} \rightarrow \mathcal{B}^f||_{\mathfrak{C}} &= ||\mathcal{A}^f ||_{\mathfrak{C}} \Rightarrow ||\mathcal{B}^f||_{\mathfrak{C}}. \end{align*} $$

The proof of these equalities is straightforward by the standard arguments Routley and Meyer.

Proof. For $\Box $ , it is sufficient to show that if $||\mathcal {A}||_{\mathfrak {C}} \in Prop$ , then so is $\Box ||\mathcal {A}||_{\mathfrak {C}}$ . It is enough here to show that $\Box ||\mathcal {A}||_{\mathfrak {C}} = ||\Box \mathcal {A}||_{\mathfrak {C}}$ . For every f,

$$ \begin{align*} &(1) &\Box||\mathcal{A}^f||_{\mathfrak{C}} &= \{ a : \forall b (S_{\Box \mathfrak{C}}ab \Rightarrow b \in ||\mathcal{A}^f||_{\mathfrak{C}}) \} \\ &(2) &||\Box \mathcal{A}^f||_{\mathfrak{C}} &= \{ a : \Box \mathcal{A}^f \in a\} \end{align*} $$

We show that the left-hand of each equation is equal by showing the right-hand of the equations are equal. The direction from (2) to (1) is fairly trivial, given the definition of $S_{\Box \mathfrak {C}}$ . For the other direction, assume that $ c \in \{ a : \forall b (S_{\Box \mathfrak {C}}ab \Rightarrow b \in ||\mathcal {A}^f||_{\mathfrak {C}}) \}$ . For reductio, further assume that $\Box \mathcal {A}^f \not \in c$ . Let’s construct the theory d by defining it as $\{ \mathcal {A} : \Box \mathcal {A} \in c \}$ . Clearly $S_{\Box }cd$ . By the squeeze lemma, there is a prime theory $d'$ extending d such that both $S_{\Box \mathfrak {C}}cd'$ and $d'$ does not contain $\mathcal {A}^f$ . However, by our first assumption, $d'$ does contain $\mathcal {A}^f$ , giving us a contradiction, so $\Box \mathcal {A}^f \in c$ .

For $\Diamond $ , I am required to show that $\Diamond ||\mathcal {A}^f||_{\mathfrak {C}} = ||\Diamond (\mathcal {A})^f||_{\mathfrak {C}}$ . We first note the following equalities given by the definition of the canonical frame and the $\Diamond $ operator.

$$ \begin{align*} \Diamond ||\mathcal{A}^f||_{\mathfrak{C}} &= \{a: \exists b(S_{\Diamond \mathfrak{C}}a b \ \& \ b \in ||\mathcal{A}^f||_{\mathfrak{C}} )\}, \\ ||\Diamond (\mathcal{A})^f||_{\mathfrak{C}}&= \{ a : \Diamond \mathcal{A}^f \in a \}. \end{align*} $$

For one direction, let $c \in \{a: \exists b(S_{\Diamond \mathfrak {C}}a b \ \& \ b \in ||\mathcal {A}^f||_{\mathfrak {C}}) \} $ . Then $\exists b(S_{\Diamond \mathfrak {C}}c b \ \& \ b \in ||\mathcal {A}^f||_{\mathfrak {C}})$ . It follows that $\{\Diamond \mathcal {A} : \mathcal {A} \in b \} \subseteq c$ . Thus, $\Diamond \mathcal {A}^f \in c$ , as required.

For the other direction, let $c \in \{ a : \Diamond \mathcal {A}^f \in a \}$ . Thus, $\Diamond \mathcal {A}^f \in c$ . We are required to show that there is a b such that $S_{\Diamond \mathfrak {C}} c b$ and $\mathcal {A}^f \in b$ .

Let $e = \{\mathcal {B} | \vdash \mathcal {A}^f \rightarrow \mathcal {B} \}$ , where $\mathcal {A}^f $ is the formula in question. It follows that e is a theory. For adjunction, assume that $\mathcal {B}, \mathcal {C} \in e$ . Then $\vdash \mathcal {A}^f \rightarrow \mathcal {B}$ and $\vdash \mathcal {A}^f \rightarrow \mathcal {C}$ , and so $\vdash \mathcal {A}^f \rightarrow (\mathcal {B} \wedge \mathcal {C})$ From this last fact, $(\mathcal {B} \wedge \mathcal {C}) \in e$ . For closure under conditional theorems, suppose that $\mathcal {B} \in e$ and $\vdash \mathcal {B} \rightarrow \mathcal {C}$ . Then $\vdash \mathcal {A}^f \rightarrow \mathcal {B}$ , and so $\vdash \mathcal {A}^f \rightarrow \mathcal {C}$ , as required.

Further, $S_{\Diamond } ce$ , which is straightforward from the definition of $S_{\Diamond }$ and the fact that, using $\Diamond \mathcal {A}^f \in c$ and ( $\Diamond $ -M), we have that every $\mathcal {B} \in e$ is such that $\Diamond \mathcal {B} \in c$ . Using the appropriate squeeze lemma, we obtain $e'$ , an prime extension of e, such that $S_{\Diamond \mathfrak {C}} ce'$ . Moreover, $ \mathcal {A}^f \in e'$ due to $\vdash \mathcal {A}^f \rightarrow \mathcal {A}^f$ .

Proof. The arguments given by by Mares and Goldblatt [Reference Mares and Goldblatt20], Lemma 9.2 can be used for every case except the $\Box $ and $\Diamond $ cases. For $\Box $ , we have to show that $\Box \phi _{\mathcal {A}} = \phi _{\Box \mathcal {A}}$ . For every f,

$$ \begin{align*} \phi_{\Box \mathcal{A}}f &= ||\Box \mathcal{A}^f||_{\mathfrak{C}} &\text{by definition of }\phi_{\mathcal{B}}\\ &= \Box ||\mathcal{A}^f||_{\mathfrak{C}} &\text{lem 7.43} \\ &= \Box\phi_{\mathcal{A}}f&\text{by definition of }\phi_{\mathcal{B}} \end{align*} $$

For $\Diamond $ , the argument is similar and establishes the more general equality $\Diamond \phi _{\mathcal {A}} = \phi _{\Diamond \mathcal {A}}$ . For every f,

$$ \begin{align*} \phi_{\Diamond \mathcal{A}}f&= ||\Diamond \mathcal{A}^f||_{\mathfrak{C}} &\text{By definition of }\phi_{\mathcal{B}}\\ &= \Diamond ||\mathcal{A}^f||_{\mathfrak{C}} &\text{lem 7.43}\\ &=\Diamond \phi_{\mathcal{A}} f &\text{by definition of }\phi_{\mathcal{B}} \end{align*} $$

To show that PropFun in closed under $\forall _n$ , the following sub-lemma proved by Mares and Goldblatt is convenient.

Lemma 7.46. If $\forall x \mathcal {A}$ is a sentence, then, for every prime theory a, $\forall x \mathcal {A} \in a$ iff there is an $X \in Prop$ such that, for ever constant c, $a \in X$ and $X \subseteq ||\mathcal {A}[c/x]||_{\mathfrak {C}}$ . That is,

$$\begin{align*}||\forall x \mathcal{A}||_{\mathfrak{C}} = \sqcap_{c \in con}||\mathcal{A}[c/x]||_{\mathfrak{C}} .\end{align*}$$

The proof is thus sub-lemmas is an in [Reference Mares and Goldblatt20, Lemma 9.3], and as such is omitted. The remaining detail of Lemma 7.45 is included here, which includes the introduction of some notation.

Here we will show that, for every $n \in \omega $ , for any $\mathcal {A}$ , $\forall _n \phi _{\mathcal {A}} = \phi _{\forall _{x_n}\mathcal {A}}$ . Mares and Goldblatt introduce another notation for this proof. We will write $\mathcal {A}^{f\backslash n}$ for the formula

$$\begin{align*}\mathcal{A}[f0/x_0, \dots, f(n-1)/x_{n-1}, x_n/x_n, f(n+1)/x_{n+1}, \dots]. \end{align*}$$

This formula is the result of applying the substitution determined by f with the exception of $x_n$ . Given this, it follows that $\mathcal {A}^{f\backslash n}[c/x_n] = \mathcal {A}^f{c/ n}$ . It can also be seen that $\forall x_n(\mathcal {A}^{f\backslash n}) = (\forall x_n \mathcal {A})^f$ . Given these two facts, the following derivation from Mares and Goldblatt is possible.

$$ \begin{align*} (\forall_n \phi_{\mathcal{A}})f &= \phi_{\mathcal{A}}(f[c/n]) &\text{by the definition of }\forall_n\\ &= \sqcap_{c \in U}||\mathcal{A}^{f[c/n]}||_{\mathfrak{C}} &\text{by definition of }\phi_A\\ &= \sqcap_{c \in U}||\mathcal{A}^{f\backslash n}[c/x_n]||_{\mathfrak{C}} &\text{by an equality just established} \\ &= ||\forall x_n (\mathcal{A}^{f\backslash n}) ||_{\mathfrak{C}} &\text{by our sub-lemma}\\ &= || (\forall x_n \mathcal{A})^f ||_{\mathfrak{C}} &\text{by an equality just established} \\ &= \phi_{\forall x_n \mathcal{A}}f &\text{by definition of }\phi_{\forall x_n \mathcal{A}} \end{align*} $$

Thus $PropFun$ is closed under $\forall _n$ for every $n \in \omega $ .

A similar proof can be given for the definable $\exists _n$ . Thus the proof of Lemma 7.45 is completed.

The proof is omitted as it is by the arguments of Mares and Goldblatt [Reference Mares and Goldblatt20], which are applicable for ${\bf BQ}.{\bf C}_{\Box \Diamond }$ .

To show that this canonical model is in fact a model for ${\bf QB}.{\bf C}_{\Box \Diamond }$ ( ${\bf BQ}.{\bf C}_{\Box \Diamond }$ ), the next lemma suffices.

Mares and Goldblatt’s arguments may be used here.

Our final step before completeness is again a truth lemma.

Proof. The proof is by induction on the complexity of $\mathcal {A}$ . Again, the arguments for the cases covered by Mares and Goldblatt can be verified to work in ${\bf QB}.{\bf C}_{\Box \Diamond }$ ( ${\bf BQ}.{\bf C}_{\Box \Diamond }$ ). The new cases are those of $\Box $ and $\Diamond $ . For $\Box $ we have the following:

The following argument is enough for the $\Diamond $ case.

$$ \begin{align*} |\mathcal{A}| &= |\Diamond \mathcal{B}| &\text{Case Hyp} \\ &= \Diamond |\mathcal{B}| &\text{Definition of } |{-}| \\ &= \Diamond \phi_{\mathcal{B}} &\text{Inductive Hypothesis}\\ &= \phi_{\Diamond \mathcal{B}} &\text{lem 7.44}\\ &= \phi_{\mathcal{A}}&\text{Case Hyp} \end{align*} $$

Similarly, and condensed, the case for $\Box $ is as follows. Let $\mathcal {A}=\Box \mathcal {B}$ , and assume the inductive hypothesis. That is, $|\mathcal {B}|= \phi _{\mathcal {B}}$ . It follows that $|\mathcal {A}|=\Box |\mathcal {B}| = \Box \phi _{\mathcal {B}}=\phi _{\Box \mathcal {B}}$ .

The semantics of Mares and Goldblatt for ${\bf QR}$ and ${\bf RQ}$ improves on Fine’s more complicated semantics, and provides a natural way of interpreting the quantifiers.Footnote ⁷ Further, the semantics of Goldblatt and Mares [Reference Goldblatt and Mares14] for quantified modal (classical) logics, in which the universal quantifier is treated similarly, provides completeness results for a wide range of quantified modal logics. The canonical models don’t require $\omega $ -complete theories, and the usual incompleteness (which results from conflicting requirements in the truth lemma for $\Box $ and $\forall x$ ) is bypassed. This kind of semantics for quantified modal logics is powerful, as seen in here, and in [Reference Goldblatt11, Reference Goldblatt and Mares14]. However, despite how natural and useful the semantics are, it is an open question how it can be used to model quantified relevant logics with non-dual quantifiers. In particular, there is work to be done developing an constructivist or intuitionistic approach to both quantifiers and modalities in relevant logics.

8 Extensions of ${\bf QB}.{\bf C}_{\Box \Diamond }$ and ${\bf BQ}.{\bf C}_{\Box \Diamond }$ .

The extensions of ${\bf QB}.{\bf C}_{\Box \Diamond }$ and ${\bf BQ}.{\bf C}_{\Box \Diamond }$ I consider here extend either the modal or implicational fragments of the logics.

Table 2 Frame conditions for modal axioms

Finally, we will show that the canonical model corresponding to various extensions of ${\bf QB}.{\bf C}_{\Box \Diamond }$ and ${\bf BQ}.{\bf C}_{\Box \Diamond }$ satisfies the conditions corresponding to the additional axioms or rules. For the axioms of the relevant fragment, the proof is standard. Thus, we turn to the modal axioms. In Section 4.7, the Barcan formula is briefly given some attention.

Let $\mathbb {L}$ be a quantified relevant logic and $\mathbb {A}$ be a set of axioms and rules from Table 2:

1. 1. the logic $\mathbb {L}.\textbf {C}$ is the regular modal logic over $\mathbb {L}$ and

2. 2. the logic $\mathbb {L}.\mathbb {A}$ is the quantified modal relevant logic that results from adding the axioms and rules of $\mathbb {A}$ to $\mathbb {L}$ .

We say that $\mathbb {A}$ corresponds with duality to a named modal classical logic $\mathbb {M}$ when both (1) if $\mathcal {A} \in \mathbb {A}$ , then the dual of $\mathcal {A}$ is also in $\mathbb {A}$ , and (2) $\mathbb {M}$ can be defined by extending classical propositional logic with the set $\mathbb {A}$ . In this case, we have

1. 3. the logic $\mathbb {L}.\mathbb {M}$ is the quantified modal relevant logic that results from adding the axioms and rules of $\mathbb {A}$ , where $\mathbb {A}$ corresponds with duality to $\mathbb {M}$ .

For example, KT can be defined using necessitation, plus the K, T, $K_\Diamond $ and $T_\Diamond $ axioms. It follows that $\mathbb {L}.\textbf {KT}$ is defined by adding necessitation, K, T, $K_\Diamond $ and $T_\Diamond $ to $\mathbb {L}$ . The logics denoted by $\mathbb {L}\mathbb {M}$ (with no dot) will be defined in Section 9

This notation for the names of logics is not particularly pretty, especially when considering each has a corresponding name without the dot, but it take advantage of the known names for relevant logics and modal logics to give a somewhat intuitive grasp of the axiomatization. Moreover, because the dot/dotless notation is in keeping with the literature on modal relevant logics, the author has chosen to keep this notation (and make the convention more precise) rather than introduce a new notation in order to reduce alternative notations.

For any logic $\mathbb {L}$ that extends ${\bf QB}.{\bf C}_{\Box \Diamond }$ (or ${\bf BQ}.{\bf C}_{\Box \Diamond }$ ) with a set of axioms (with out without the necessitation rule) from Table 2, we define $\mathbb {L}$ -models to be the ${\bf QB}.{\bf C}_{\Box \Diamond }$ -models (or ${\bf BQ}.{\bf C}_{\Box \Diamond }$ -models) that satisfy the corresponding conditions from Table 2. For these logics, the set of which we will denote by $\mathfrak {B}$ , we record soundness and completeness.

Proofs are as usual, and as in [Reference Seki30].

Given this list of correspondences, I will now isolate a couple of interesting extensions of B.C $_{\Box \Diamond }$ . As described by Seki [Reference Seki30], p. 408, the logic ${\bf R}.$ K is obtained from B.C $_{\Box \Diamond }$ by deleting ${ {\mkern 1mu\boldsymbol t}}$ and $\Diamond $ (and using $\diamond\kern-4pt\cdot$ as a replacement) from the logic’s signature, removing the axioms ${ {\mkern 1mu\boldsymbol t}}$ and $\Diamond (\mathcal {A} \vee \mathcal {B})\rightarrow (\Diamond \mathcal {A} \vee \Diamond \mathcal {B})$ , and the rule $\Diamond $ -monotonicity, extending the relevant logic fragment from B to ${\bf R}$ , and adding the axiom (K $\Box $ ) and the rule of necessitation. The logic ${\bf R}$ K results from adding the axiom $(\Diamond \mathcal {A} \wedge \Box \mathcal {B}) \rightarrow \Diamond (\mathcal {A} \wedge \mathcal {B})$ to ${\bf R}.$ K. Finally, R4 is obtained by adding to ${\bf R}$ K the axioms $\Box \mathcal {A} \rightarrow \mathcal {A}$ and $\Box {\mathcal {A}} \rightarrow \Box \Box \mathcal {A}$ .

There are two interesting types of axioms to consider. The first are axioms with both of a non-dual pair $\Box $ and $\Diamond $ . Some sentences of this kind are highlighted in the next section. The other kind of axiom of interest are axioms in which both quantifiers and modalities appear, such as the Barcan Formulas. The next after next will deal with these.

9 Dropping the Dot

The dot/dotless notation for a logics name is used in the modal relevant logic literature, but it is not entirely precise. Sometimes, the dot is removed when the modal fragment is sufficiently similar to the modal fragment of the corresponding modal classical logic (as in, for example, in [Reference Seki29, Reference Seki30]). This convention is not entirely standard. Mares and Tanaka [Reference Mares and Tanaka23] use the name ${\bf R}$ .K $^-$ , with the minus symbol indicating the lack of the axiom $K\Box $ , for a logic that here we would denote without the dot. It have also been common to use the name NR for our ${\bf R}.\textbf {4}$ without primitive $\Diamond $ . Here, however, my aim is to both make rigorous the dotting convention as used consistently with Seki, and to motivate interest in the distinction picked out by the convention. My hope is that this interest will standardize once and for all the dotting convention. As mentioned above, the dot is removed from a logic’s name when it is sufficiently classical. We are now in a position to explain what is meant by this, which is roughly that the diamond and box to behave sufficiently like they do in modal classical logic.

Relevant logicians have been interested in when a relevant modal logic contains the theorems of a modal logic whose base is classical logic. We shall often call modal logics with a classical base modal classical logics (cf. modal relevant logics), which are not to be confused with the established term ‘classical modal logics.’Footnote ⁸ That is, when the theorems of a modal logic with a classical base, written in $\sim $ , $\wedge $ , and $\Box $ , are theorems of the modal relevant logic. Mares and Meyer have been at the forefront of research in this area. In [Reference Mares18], it is proved that a number of modal relevant logics are conservative extensions of modal logics. Similar results, including conservative extension by Boolean negation, can be found in [Reference Mares and Meyer21–Reference Mares and Tanaka23]. There is therefore an interest the ‘classicality’ of the modal fragments of relevant logics.

The dot notation identifies a certain degree of classicality in the modal fragment of relevant logics, and it is this degree which is necessary, though not sufficient, to ensure that a relevant modal logic is a conservative extension of its classical counterpart. As this fragment includes negation, weaker logics such as B have no hope of containing the theorems of a modal classical logic. On the other hand, the axioms below required for ‘dropping to dot’ are exactly the postulates Dunn [Reference Dunn6] identifies as required for positive modal logics (without implication). Without these postulates, a positive modal logic would lack theorems (in $\wedge , \vee , \Box , \Diamond $ ) that are theorems of the corresponding modal classical logic. Therefore, for weaker relevant logics there are interesting results for be found in the positive modal fragments, and it is only fitting that the frame conditions given below are suitable for positive fragments of the logics considered. So let us make rigorous the dotting convention.

To warrant the removal of the dot from a logic’s name, we must add $\Box (\mathcal {A} \vee \mathcal {B})\rightarrow (\Box \mathcal {A} \vee \Diamond \mathcal {B})$ or the dual $(\Diamond \mathcal {A} \wedge \Box \mathcal {B} )\rightarrow \Diamond (\mathcal {A} \wedge \mathcal {B})$ , and we must have the duality of the modalities $\Box $ and $\Diamond $ . For a (classical) regular modal logic to be contained in a corresponding relevant modal logic, all the theorems must be included under translation. The duality of the quantifiers is a theorem of classical regular modal logics. Moreover, $(\Diamond \mathcal {A} \wedge \Box \mathcal {B} )\supset \Diamond (\mathcal {A} \wedge \mathcal {B})$ is a theorem of all classical regular modal logics (as in [Reference Chellas5], Theorem 8.12). Thus, only the dotless logics can contain their classical counterparts.

Here we establish frame conditions for these axioms.

The condition from [Reference Mares and Meyer22]—if $S_\Box ab$ , then $\exists x \leq b(Tax)$ , with $Tab =_{def} Sab \ \& \ Sa^*b^*$ —is used to validate $\Box (\mathcal {A} \vee \mathcal {B})\rightarrow (\Box \mathcal {A} \vee \Diamond \mathcal {B})$ in a modal relevant logic in which the box is primitive, and the diamond is a defined dual. The T relation here is used in particular because of the essential role of negation in defining the diamond. The proof requires looking at star worlds. However, the condition I give above can be used in both positive fragments and in logics without the duality of the modalities. The conditions above are essentially the Mares–Meyer condition restricted to the relations for two possibly non-dual modalities. The conditions above becomes the Mares–Meyer condition when $S_\Diamond ab$ iff $S_\Box a^*b^*$ . Moreover, the duality of the modalities collapses the corresponding relations, as recorded below.

Proof. Lemmas 9.53 and 9.54 demonstrate the soundness claim. For completeness, we define the canonical modal as earlier, but for the appropriate logic. The completeness proofs, of which we will only show that for the axiom $\Box (\mathcal {A} \vee \mathcal {B})\rightarrow (\Box \mathcal {A} \vee \Diamond \mathcal {B})$ , are essentially the proof given by Mares and Meyer [Reference Mares and Meyer22, Lemma 4.5], with obvious modifications to handle the star-less condition given above.

First, assume that $S_\Box ab$ . That is, if $\Box \mathcal {A} \in a$ , then $\mathcal {A} \in b$ . We show that there is a prime theory $ x \subseteq b$ such that $S_\Box ax$ and $S_\Diamond ax$ . Let c be the set of formulas $\mathcal {A}$ such that $\Diamond \mathcal {A} \not \in a$ , and let $a'$ be the set of formulas $\mathcal {A}$ such that $\Box \mathcal {A} \in a$ . Thus, $a' \subseteq b$ , and is a theory. Further suppose that d is the set of formulas not in b. We have here that the pair ( $a', c\cup d$ ) is independent by the following:

Suppose for reductio that the pair is not independent. Then there are $\mathcal {A}_1, \dots , \mathcal {A}_n \in a'$ , $\mathcal {B}_1, \dots , \mathcal {B}_m \in d$ and $\mathcal {D}_1, \dots , \mathcal {D}_l \in c$ such that

$$\begin{align*}\vdash (\mathcal{A}_1 \wedge, \dots, \wedge \mathcal{A}_n)\rightarrow (\mathcal{B}_1 \vee, \dots, \vee \mathcal{B}_m \vee \mathcal{D}_1 \vee, \dots, \vee \mathcal{D}_l) \end{align*}$$

from which we can infer

$$\begin{align*}\vdash \Box(\mathcal{A}_1 \wedge, \dots, \wedge \mathcal{A}_n)\rightarrow \Box(\mathcal{B}_1 \vee, \dots, \vee \mathcal{B}_m \vee \mathcal{D}_1 \vee, \dots, \vee \mathcal{D}_l). \end{align*}$$

Then, given the axiom in question, we can derive

$$\begin{align*}\vdash \Box(\mathcal{A}_1 \wedge, \dots, \wedge \mathcal{A}_n)\rightarrow \Box(\mathcal{B}_1 \vee, \dots, \vee \mathcal{B}_m) \vee \Diamond(\mathcal{D}_1 \vee, \dots, \vee \mathcal{D}_l). \end{align*}$$

The primeness of the element a further implies either the $\Box (\mathcal {B}_1 \vee , \dots , \vee \mathcal {B}_m) \in a$ or that $\Diamond (\mathcal {D}_1 \vee , \dots , \vee \mathcal {D}_l) \in a$ . If the latter, then $\Diamond \mathcal {D}_i \in a$ for some $i \leq l$ , which entails $\mathcal {D}_i \in c$ , a contradiction. On the other hand, $\Box (\mathcal {B}_1 \vee , \dots , \vee \mathcal {B}_m) \in a$ , then $\mathcal {B}_1 \vee , \dots , \vee \mathcal {B}_m \in b$ , which also leads to contradiction. Thus, ( $a', c\cup d$ ) is independent. Using the extension lemma, There is a prime theory x extending $a'$ such that the pair ( $x,c\cup d$ ) is independent. It is obvious that $S_\Box ax$ by our definition of $a'$ . To show that $S_\Diamond ax$ , suppose that it did not hold. Then there is a formula $\mathcal {A}$ such that $ \mathcal {A} \in x$ but $\Diamond \mathcal {A} \not \in a$ . Such formulas make up the set c, as defined above. All such formulas were excluded from x in the extension lemma. So $S_\Diamond ax$ .

This brings us to the title of the current section. In the naming scheme of the logics here, my convention is to drop the dot in the name of the logic when (1) the logic contains both the diamond and the box (with possibly one being defined), (2) the diamond and box are duals, and (3) both the formula schemes discussed in this section are theorems. The result is that logics whose name has dropped the dot have a certain degree of classicality.

From here, further research is motivated into exactly what degree of classicality this convention picks out. One line of investigation is to see which of these logics can be proven to admit $\gamma $ — from $\neg \mathcal {A} \vee \mathcal {B}$ and $\mathcal {A}$ to infer $\mathcal {B}$ . Following the arguments of Mares [Reference Mares18], $\gamma $ -admissibility may lead to conservative extension results over modal relevant logics. Moreover, for quantified modal logics, a natural starting point is to consider the quantified extensions of the logics in [Reference Mares18], and to determine whether they conservatively extend their corresponding quantified modal classical logics.

10 Barcan formula

Here we briefly discuss the role of the Barcan formula in modal relevant logics. In the logics defined above, using UI, the Barcan formula is not derivable. However, as we say earlier, the Converse Barcan Formula is derivable in our basic logic ${\bf QB}.{\bf C}_{\Box \Diamond }$ .

In classical logics, the Barcan formula is related to models in which $Prop$ and $PropFun$ are the set of all subsets of worlds and set of all functions from variable assignments into $Prop$ , respectively. These models are called Kripkean or full (due to $Prop$ and $PropFun$ being the largest sets they can be). Here, $\sqcap S = \cap S$ . Consequently, the verification conditions for the quantifiers for Kripkean models collapse into the Tarskian verification conditions. For the universal quantifier, namely

$$\begin{align*}a, f, \vDash \forall x A \text{ iff, for every }g \in xf\text{, }g, a \vDash A \end{align*}$$

since $\sqcap S = \cap S$ and $|\forall x \mathcal {A}|^{\mathcal {M}}f =\sqcap _{g \in xf} |\mathcal {A}|^{\mathcal {M}}g $ .

In [Reference Goldblatt and Mares14], a Tarskian General Frame is defined as a frame for $Prop$ is closed under which arbitrary (infinite) intersection. In these frames, the Tarskian verification condition is derivable. Moreover, they show that, for a class of frames $\mathbb {C}$ of modal classical logics, a formula $\mathcal {A}$ is valid in all standard constant domain models based on members of $\mathbb {C}$ iff $\mathcal {A}$ is valid in all Tarskian general frames based on members of $\mathbb {C}$ iff $\mathcal {A}$ is valid in all full general frames based on members of $\mathbb {C}$ [Reference Mares and Goldblatt20, Theorem 7]. They go on to show that models that are not Tarskian can validate the Barcan Formula, showing that “the Tarskian condition is sufficient to ensure validity of BF, but it is not necessary” [Reference Goldblatt and Mares14, p. 14].

The question then remains as to what the role of the Barcan formula is in modal relevant logics.

Note that, in [Reference Goldblatt and Hodkinson12], it is shown that Kripkean models also validate commuting quantifiers (CQ— $\forall x \forall y \mathcal {A} \rightarrow \forall y \forall x \mathcal {A}$ ) in modal classical logics. In the relevant logics we consider, we can prove that $\vdash $ CQ using UI (and $\forall $ -Intro) without the Barcan Formula [Reference Mares and Goldblatt20, Lemma 6.3 (d)].

What is left to do is prove, of certain classes of models, that the relevant logics considered plus the Barcan Formula are characterized by these models. That is, give soundness and completeness results for whichever classes of models we are able. Here, we must be careful that the class of models we choose does not imply incompleteness for the quantified relevant fragment of the logic by, for example, becoming vulnerable to Fine’s incompleteness proof as in [Reference Fine, Norman and Sylvan9].

Although Goldblatt [Reference Goldblatt11], Goldblatt and Mares [Reference Goldblatt and Mares14], and Mares and Goldblatt [Reference Mares and Goldblatt20] prove many relations between logics with the Barcan Formula (and CQ), the tightest characterization so far is not the most illuminating. That characterization, for relevant logics, is given in the following theorem. While related to Kripkean models with Tarskian conditions, the following fact about relevant logics with the Barcan formula is the furthest we will venture into the Barcan formula in this work.

Theorem 10.59. Where $\mathbb {L}$ is a quantified modal relevant logic without BF, the logic $\mathbb {L}+$ BF is characterized by the class of all admissible function models that satisfy

$$\begin{align*}\forall_x \Box \phi \subseteq \Box \forall_x \phi,\end{align*}$$

and are based on a general $\mathbb {L}$ -frame. (Where $\Box $ in the condition above is the type-lifted operation on propositional functions.)

Proof. The proof is essentially unaltered from [Reference Goldblatt11]. For soundness, we have the following:

$$ \begin{align*} |\forall x \Box \mathcal{A}|f &= \forall_x \Box |\mathcal{A}|f\\ &\subseteq \Box \forall_x |\mathcal{A}|f \\ &= |\Box \forall x \mathcal{A}|f. \end{align*} $$

For completeness, the goal is to show that $\phi _{\forall x \Box \mathcal {A} } \subseteq \phi _{\Box \forall x \mathcal {A}}$ using the fact that ${\vdash \forall x \Box \mathcal {A} \rightarrow \Box \forall x \mathcal {A} }$ . For this, it is sufficient to show that, if $\vdash \mathcal {A} \rightarrow \mathcal {B}$ , then $\phi _{\mathcal {A}} \subseteq \phi _{\mathcal {B}}$ . Take an arbitrary $a \in K$ and $f \in U^\omega $ , and suppose that $a \in \phi _{\mathcal {A}}f$ . By definition, this is $a \in ||\mathcal {A}^f||_{\mathfrak {C}}$ , and so $\mathcal {A}^f \in a$ . But a is a theory, and so $\mathcal {B}^f \in a$ . This gives us $a \in \phi _{\mathcal {B}}$ , as required.

This theorem might not seem very insightful for the role the Barcan formula plays. Indeed, the condition appears as the axiom written in a semantic dialect. Similarly, we could offer the condition $\Box \phi \subseteq \phi $ for the axiom T, and give a similar proof. While we have a deeper understanding of the T axiom because of its corresponding condition of reflexivity, such an insight is hidden in the condition $\Box \phi \subseteq \phi $ . As such, conditions written in a semantic dialect, such as for the Barcan formula above, often fall short of providing the philosophical explanations that we are after. The proof above is quite modular, and is applicable to any axiom of a conditional form, taking advantage of the fact that the axiom being provable implies the corresponding subset relation holds. Consequently, it is a powerful formal technique that appears to offer no philosophical insight into the nature of the Barcan formula.

Goldblatt proves a similar theorem [Reference Goldblatt11, Theorem 4.5.4]. Goldblatt explains the importance of this and related theorems.

Thus, proving this theorem will at least be a good starting point in exploring characterizations of relevant logics with the Barcan Formula.

The Barcan formula’s dual, with $\exists $ and $\Diamond $ can be given a similar characterization. Both results follow from a more general fact about the relation of propositional functions and provable conditionals. What is desired, ideally, is a semantic condition with more explanatory power. The relation, for example, of the Barcan formulas to the contraction and expansion of domains provides some explanatory insight which is missing in the straightforward algebraic translation (perhaps transliteration?) of the axiom. This motivates the following lines of investigation for future work:

1. 1. Find a semantic condition for the Barcan formula that provides more insight into the nature of the Barcan formula in relevant logics.

2. 2. Develop systems for quantified modal relevant logics in which both the Barcan formula and its converse fail. For example, using the restricted universal elimination axiom $\forall y (\forall x \mathcal {A} \rightarrow \mathcal {A}[y/x])$ instead of the unrestricted $\forall x \mathcal {A} \rightarrow \mathcal {A}[\tau /x]$ , with other axiomatic adjustments, can ensure that the Converse Barcan formula is not a theorem.

Goldblatt [Reference Goldblatt11] provides an excellent starting point for pursuing the latter project, as a large portion of the book is dedicated to logics defined using the restricted universal elimination axiom.