of a wide range of propositional relevant logics for which excluded middle is valid (with fusion and the Ackermann truth constant), the first-order extensions 
and 
admit 
1 Introduction
The admissibility of
$\gamma $
in relevant logics remains an important question. With recent interest in quantified (modal) relevant logics, attention is turned to
$\gamma $
-admissibility in these logics. A particular boon in this research is the semantic framework for the quantified relevant logics QR and RQ introduced by Mares & Goldblatt [Reference Mares and Goldblatt16], which has been extended more generally to first-order and first-order modal relevant logics sound and complete for ternary relational frames by Ferenz [Reference Ferenz8].Footnote
1
Here we employ this Mares–Goldblatt semantics as generalized by Ferenz to investigate which first-order relevant logics admit
$\gamma $
using the method of normal models, which was introduced by Sylvan (né Routley) and Meyer [Reference Routley and Meyer25]. This provides a foundation to explore
$\gamma $
-admissibility in first-order modal relevant logics, taking advantage of the general framework provided by the Mares–Goldblatt interpretation of quantifiers.
Ackermann’s rule
$\gamma $
, originally given in [Reference Ackermann1], is a form of disjunctive syllogism (or, classically, detachment/modus ponens). In the tradition of relevant logic,
$\gamma $
ought to be rejected when formulated as a rule under which theories are closed. This would entail that from inconsistent theories anything is derivable, which is anathema to the relevantist project. However, it is another story if we take
$\gamma $
to close the set of theorems. Thus,
$\gamma $
is presented follows:
$$\begin{align*}\neg \mathcal{A} \vee \mathcal{B}, \mathcal{A} \Rrightarrow \mathcal{B}.\end{align*}$$
The symbol ‘
$\Rrightarrow $
’ here indicates a rule of proof in the sense of Humberstone [Reference Humberstone14]; Smiley [Reference Smiley33]: That is,
$\mathcal {A}_1,\dots , \mathcal {A}_n\Rrightarrow \mathcal {B}$
means that if each
$\mathcal {A}_i$
is a theorem of the logic in question, then so is
$\mathcal {B}$
. The rule
$\gamma $
is typically not given in the definition of a relevant logic; it is, however, sometimes an admissible rule. That is, in particular, the addition of the rule does not result in new theorems. The question of which relevant logics admit
$\gamma $
is an interesting and significant question, and has been in the crosshairs of relevantists since the beginning.
We present logics as Hilbert-style axiom systems with axiom and rule schemes defining a set of theorems. We use the usual notion of a proof (of
$\mathcal {A}$
) in this setting as a sequence of formulas (ending with
$\mathcal {A}$
) where each formula is either an instance of an axiom scheme or follows from previous formulas by application of an instance of a rule scheme. As our interest is in the set of theorems and not a consequence relation, we set our focus on rules of proof (defined above). In defining a logic, the rules explicitly given in the statement of the logic we call the primitive rules of the systems. Similar to primitive rules are the derived rules, whose form can be captured exactly by a series of axioms and primitive rule applications. For example, a rule of reiteration of the form
$\mathcal {A} \Rrightarrow \mathcal {A}$
, if not primitive, can be shown to be derivable using modus ponens and the axiom
$\mathcal {A} \rightarrow \mathcal {A}$
. Finally, a rule is admissible if there exists a proof of the conclusion of the rule whenever there are proofs of the premises.Footnote
2
In this paper we will give all primitive rules using the
$\Rrightarrow $
notation, but the distinction between primitive and admissible rules is worth noting. One way to expand relevant logics is by the addition of proper axioms, with the notion of derivation suitable altered to include the additional proper axioms. These need not be schematic, and can allow relevant logic to represent reasoning from theories such as set theory, Peano Arithmetic, or even just a small set of beliefs. Part and parcel to the relevant approach is that inconsistent theories do not imply every formula, and so
$\gamma $
is not desirable as a primitive rule in these cases. On the other hand, the rules taken as primitive, although presented as rules of proof, are taken to apply in these extended cases.Footnote
3
Meyer et al. [Reference Meyer, Dunn and Leblanc21, p. 120] note, “the cut theorem…is for classical theories simply
$\gamma $
is peculiar notation.” This is emphasized in Urquhart [Reference Urquhart and Bimbo35], summarizing the history and importance of
$\gamma $
, where he suggests additional similarities. Notably he conjectures a speed-up theorem for
$\gamma $
is relevant logics, in analogy to speedup theorems for the rule cut in classical logics (as shown in, e.g., Pudlák [Reference Pudlák and Buss23]).Footnote
4
The admissibility of
$\gamma $
, if Urquhart’s conjecture is proven, has significant consequences for proof-theoretic presentations of first-order relevant logics.
While some logics admit
$\gamma $
, such as R and E, several do not. In particular, several contraction-less relevant logics extended by Boolean negation do not admit
$\gamma $
Meyer et al. [Reference Meyer, Giambrone and Brady22]. The naïve set theory of Brady [Reference Brady, Priest, Routley and Norman3] also fails to admit
$\gamma $
, but in this case the failure of
$\gamma $
is a feature and not a bug; on the other hand, the proof in Friedman & Meyer [Reference Friedman and Meyer13] showing the failure of
$\gamma $
for Meyer’s relevant arithmetic
$\mathbf {R}^{\sharp }$
was a catastrophic event for the development of
$\mathbf {R}^{\sharp }$
. Meyer & Dunn [Reference Meyer and Dunn20] first showed that R, E, and T—the favorite children of Anderson and Belnap—admit
$\gamma $
using algebraic techniques. Later, additional techniques were found, such as normal models [Reference Routley, Meyer and Leblanc26], metavaluations [Reference Meyer19], and reduced frames [Reference Slaney32]. Although the technique of normal models is the basis of the techniques of this paper, metavaluations involve defining valuations mapping formulas to the values
$0$
or
$1$
based on the relationship they bear to a regular theory. For the interested reader, the method is elegantly described in [Reference Dunn, Restall, Gabbay and Guenthner6]. Note that the normal models method is restricted by the requirement of the principle of excluded middle as an axiom. For relevant logics without this requirement, one turns to the other methods referenced in this paragraph.
For a detailed account of the history of
$\gamma $
in propositional relevant logics, the reader is directed to Urquhart [Reference Urquhart and Bimbo35] and the references therein. Many modal propositional logics have also been shown to admit
$\gamma $
; e.g., see Mares & Meyer [Reference Mares and Meyer17]; Routley & Meyer [Reference Routley and Meyer25]; Seki [Reference Seki29–Reference Seki31]. The Mares–Goldblatt style semantics of Ferenz [Reference Ferenz8] for first-order modal relevant logics combines the Mares-Goldblatt machinery with the general frames of Seki [Reference Seki28], the latter of which is used to obtain
$\gamma $
-admissibility results for a wide class of modal relevant logics. Thus, Ferenz [Reference Ferenz8] has laid the groundwork for using the method of normal models in both the first-order and the first-order modal settings. Here we pursue the former.
For quantified relevant logics, as far as we know, only a handful have been shown to admit
$\gamma $
. The first, and most relevant to this paper, is the proof of
$\gamma $
-admissibility in RQ in [Reference Meyer, Dunn and Leblanc21, Theorem 6]. The method of proof is by an algebraic semantics for RQ. The Mares–Goldblatt interpretation of the quantifiers introduces a natural semantics for RQ, defined as a Hilbert style axiom system. The genesis of such a semantics was due to the fact that the most straightforward way of defining a constant domain, ternary relational semantics extending the semantics for R validated formulas which were not theorems of RQ. This is the incompleteness result of Fine [Reference Fine, Norman and Sylvan12].Footnote
5
The set of validities of the class of the most straightforward constant domain, ternary relational models (semantically) determines a logic, and we will call this logic
$\overline {\textbf {RQ}}$
. This properly contains the theorems of RQ, and was shown by Weiss [Reference Weiss36] to admit
$\gamma $
. However, giving an axiomatization (finite or otherwise) of this set of validities is still an open question.
In Kripke [Reference Kripke and Bimbó15], a method of proving
$\gamma $
-admissibility for first-order extensions of R and E using semantic tableaux is stated; however, no proof is given in detail. Kripke, however, fails to establish which of RQ/
$\overline {\textbf {RQ}}$
and EQ/
$\overline {\textbf {EQ}}$
his proof is applicable to.
The paper is divided as follows. We begin by introducing preliminaries such as the definitions of languages, logics, semantics, and key notions. Then we tackle proving
$\gamma $
-admissibility by generalizing the normal models method. Here we use the Mares–Goldblatt style semantics. Finally we make concluding remarks concerning future directions.
2 Preliminaries
We jump straight into a presentation of first-order relevant logics. For the reader not familiar with propositional relevant logics, one may consult one of Dunn & Restall [Reference Dunn, Restall, Gabbay and Guenthner6]; Bimbó [Reference Bimbó, Jacquette, Gabbay, Thagard and Woods2] for an excellent overview. Some familiarity with propositional relevant logics and ternary relational semantics is assumed, but such knowledge is not required.
2.1 First-order relevant logics
2.1.1 Language
A first-order language (with constants and without function symbols) is built up from a set of symbols divided as follows:
-
1. A denumerable set of variables
$Var = \{x_0, x_1, \dots \}$
. Here we assume a fixed but arbitrary ordering of the elements of
$Var$
, which is tracked by variable subscripts. -
2. An at most denumerable signature
$\mathbb {S}$
consisting of-
(a) a set of constant symbols
$Con^{\mathbb {S}} = \{c_0, c_1, \dots \}$
, -
(b) a non-empty set of predicate symbols
$Pred^{\mathbb {S}}$
, where
$P^n \in Pred^{\mathbb {S}}$
is an n-ary predicate. The set of n-ary predicates shall be written as
$Pred^n \subseteq Pred^{\mathbb {S}}$
,
-
-
3. A constant symbol
-
4. Binary operators
$\land , \lor , \rightarrow , \circ $
-
5. Unary operator
$\neg $
-
6. Quantifier symbols
$\forall $
,
$\exists $
.
The notion of being a term, relative to a signature, is defined as usual, and we will use
$\tau $
with decorations varying over terms. A signature will henceforth be assumed fixed, and we will cease to mention signatures unless such a remark is required.Footnote
6
Given a set U of individuals, a variable assignment is a denumerable sequence of individuals,
$f \in U^\omega $
, such that the n-th element in the sequence (written as
$fn$
) is the individual assigned to the n-th variable
$x_n$
given by the assumed fixed ordering. Given a variable assignment f, an
$x_n$
-variant of f differs from f in at most the assignment to the variable
$x_n$
. We write
$f \sim _n f'$
(or
$f \sim _{x_n} f'$
) to denote that f and
$f'$
are
$x_n$
variants of one another. We will write
$f[j/n]$
(or
$f[j/x_n]$
), with
$j \in U$
to denote the result of replacing the n-th element of f with the individual j.
Definition 2.1 (The First-Order Relevant Language).
The basic first-order relevant language
$\mathfrak {L}$
, or well-formed formulas (hereby wff) is defined in Backus-Naur form as follows:
Implicit is the use of parentheses around each construction with a binary connective. That is, we assume that all unary operators (including quantifiers) bind more strongly than binary operators. Moreover, we assume the right arrow binds weaker than fusion, which itself binds weaker than the extensional conjunction and disjunction.
We write
$\mathcal {A}[\tau /x]$
to denote the result of substituting 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. The usual definitions of bound and free variables are assumed. A term
$\tau $
is free for x (or freely substitutable for x) in
$\mathcal {A}$
if
$\tau $
does not become bound in the resulting formula
$\mathcal {A}[\tau /x]$
.Footnote
7
When we write a formula with a variable superscript, such as
$\mathcal {A}^x$
, this means that x does not occur free in
$\mathcal {A}$
.
2.1.2 Axiomatic presentations
Although no propositional language was defined, we first axiomatize a wide class of propositional relevant logics.Footnote 8 Although alternative axiom systems can define several of the logics we present, a singular modular system extending a base logic is used.
Definition 2.2 (Propositional Logics).
The base propositional logic 
is defined by the following axioms and rules:Footnote
9
-
(ID)
$\mathcal {A} \rightarrow \mathcal {A}$
-
(
$\land $
E)
$\mathcal {A} \land \mathcal {B} \rightarrow \mathcal {A}$
-
(
$\land $
E)
$\mathcal {A} \land \mathcal {B} \rightarrow \mathcal {B}$
-
(
$\lor $
I)
$\mathcal {A} \rightarrow \mathcal {A} \lor \mathcal {B}$
-
(
$\lor $
I)
$\mathcal {B} \rightarrow \mathcal {A} \lor \mathcal {B}$
-
(
$\land $
I)
$((\mathcal {A} \rightarrow \mathcal {B}) \land (\mathcal {A} \rightarrow \mathcal {C})) \rightarrow (\mathcal {A} \rightarrow (\mathcal {B} \land \mathcal {C}))$
-
(
$\lor $
E)
$((\mathcal {A} \rightarrow \mathcal {C}) \land (\mathcal {B} \rightarrow \mathcal {C})) \rightarrow ((\mathcal {A} \lor \mathcal {B}) \rightarrow \mathcal {C})$
-
(
$\land $
-
$\lor $
)
$\mathcal {A} \land (\mathcal {B} \lor \mathcal {C}) \rightarrow (\mathcal {A} \land \mathcal {B}) \lor (\mathcal {A} \land \mathcal {C})$
-
(
$DNE$
)
$\neg \neg \mathcal {A} \leftrightarrow \mathcal {A}$
-
(MP)
$\mathcal {A}, \mathcal {A} \rightarrow \mathcal {B} \Rrightarrow \mathcal {B}$
-
(ADJ)
$\mathcal {A}, \mathcal {B} \Rrightarrow \mathcal {A} \land \mathcal {B}$
-
(Prefix)
$\mathcal {A} \rightarrow \mathcal {B} \Rrightarrow (\mathcal {C} \rightarrow \mathcal {A}) \rightarrow (\mathcal {C} \rightarrow \mathcal {B})$
-
(Suffix)
$\mathcal {A} \rightarrow \mathcal {B} \Rrightarrow (\mathcal {B} \rightarrow \mathcal {C}) \rightarrow (\mathcal {A} \rightarrow \mathcal {C})$
-
(RCont)
$\mathcal {A} \rightarrow \mathcal {B} \Rrightarrow \neg \mathcal {B} \rightarrow \neg \mathcal {A}$
-
(R
$\circ $
)
$\mathcal {A} \rightarrow (\mathcal {B} \rightarrow \mathcal {C}) \Lleftarrow \Rrightarrow (\mathcal {A} \circ \mathcal {B})\rightarrow \mathcal {C}$
-
(R
)
) 
Each of the logics of interest is a first-order extension of some propositional extension of 
. The propositional extensions are defined using the following list of axioms and rules:
-
(A1)
$\mathcal {A} \vee \neg \mathcal {A}$
-
(A2)
$\mathcal {A} \wedge (\mathcal {A} \rightarrow \mathcal {B}) \rightarrow \mathcal {B}$
-
(A3)
$(\mathcal {A} \rightarrow \mathcal {B}) \wedge (\mathcal {B} \rightarrow \mathcal {C})\rightarrow (\mathcal {A} \rightarrow \mathcal {C})$
-
(A4)
$(\mathcal {A} \rightarrow (\mathcal {A} \rightarrow \mathcal {B})) \rightarrow (\mathcal {A} \rightarrow \mathcal {B})$
-
(A5)
$\mathcal {A} \rightarrow ((\mathcal {A} \rightarrow \mathcal {B})\rightarrow \mathcal {B})$
-
(A6)
$\mathcal {A} \rightarrow (\mathcal {B} \rightarrow \mathcal {B})$
-
(A7)
$\mathcal {A} \rightarrow (\mathcal {B} \rightarrow \mathcal {A})$
-
(A8)
$(\mathcal {A} \rightarrow \mathcal {B})\rightarrow ((\mathcal {A} \rightarrow \mathcal {C})\rightarrow (\mathcal {A} \rightarrow \mathcal {B} \wedge \mathcal {C}))$
-
(A9)
$\mathcal {A} \rightarrow (\mathcal {A} \rightarrow \mathcal {A})$
-
(A10)
$\mathcal {A} \vee \mathcal {B} \rightarrow ((\mathcal {A} \rightarrow \mathcal {B})\rightarrow \mathcal {B})$
-
(A11)
$(\mathcal {A} \wedge \mathcal {B} \rightarrow \mathcal {C})\rightarrow (\mathcal {A} \wedge \neg \mathcal {C} \rightarrow \neg \mathcal {B})$
-
(A12)
$\mathcal {A} \rightarrow \neg (\mathcal {A} \rightarrow \neg \mathcal {A})$
-
(A13)
$(\mathcal {A} \rightarrow \neg \mathcal {A} )\rightarrow \neg \mathcal {A}$
-
(A14)
$(\mathcal {A} \rightarrow \mathcal {B}) \rightarrow (\neg \mathcal {B} \rightarrow \neg \mathcal {A})$
-
(A15)
$\mathcal {A} \rightarrow \mathcal {B} \vee \neg \mathcal {B}$
-
(A16)
$\mathcal {A} \rightarrow (\neg \mathcal {A} \rightarrow \mathcal {B})$
-
(A17)
$(\mathcal {A} \rightarrow \mathcal {B})\rightarrow ((\mathcal {B} \rightarrow \mathcal {C}) \rightarrow (\mathcal {A} \rightarrow \mathcal {C}))$
-
(A18)
$(\mathcal {A} \rightarrow \mathcal {B})\rightarrow ((\mathcal {C} \rightarrow \mathcal {A}) \rightarrow (\mathcal {C} \rightarrow \mathcal {B}))$
-
(A19)
$(\mathcal {A} \rightarrow (\mathcal {B} \rightarrow \mathcal {C})) \rightarrow (\mathcal {B} \rightarrow (\mathcal {A} \rightarrow \mathcal {C}))$
-
(A20)
$(\mathcal {A} \rightarrow (\mathcal {B} \rightarrow \mathcal {C})) \rightarrow ((\mathcal {A} \rightarrow \mathcal {B}) \rightarrow (\mathcal {A} \rightarrow \mathcal {C}))$
-
(A21)
$(\mathcal {A} \rightarrow \mathcal {B}) \rightarrow ((\mathcal {A} \rightarrow (\mathcal {B} \rightarrow \mathcal {C})) \rightarrow (\mathcal {A} \rightarrow \mathcal {C}))$
-
(A22)
$(\mathcal {A} \wedge \mathcal {B} \rightarrow \mathcal {C})\rightarrow (\mathcal {A} \rightarrow (\mathcal {B} \rightarrow \mathcal {C}))$
-
(R1)
$\mathcal {C} \vee \mathcal {A} \Rrightarrow \mathcal {C} \vee \neg (\mathcal {A} \rightarrow \neg \mathcal {A})$
-
(R2)
$ \mathcal {C} \vee (\neg \mathcal {A} \rightarrow \mathcal {A})\Rrightarrow \mathcal {C} \vee \mathcal {A} $
-
(R3)
$\mathcal {C} \vee \mathcal {A}, \mathcal {C} \vee ( \mathcal {A} \rightarrow \mathcal {B})\Rrightarrow \mathcal {C} \vee \mathcal {B}$
-
(R4)
$\mathcal {C} \vee (\mathcal {A} \rightarrow \mathcal {B}) \Rrightarrow \mathcal {C} \vee (\neg \mathcal {B} \rightarrow \neg \mathcal {A})$
-
(R5)
$\mathcal {A} \Rrightarrow (\mathcal {A} \rightarrow \mathcal {B})\rightarrow \mathcal {B}$
-
(R6)
$\mathcal {C} \vee (\mathcal {A} \rightarrow \mathcal {B}), \mathcal {C} \vee (\mathcal {D} \rightarrow \mathcal {E}) \Rrightarrow \mathcal {C} \vee ((\mathcal {B} \rightarrow \mathcal {D}) \rightarrow (\mathcal {A} \rightarrow \mathcal {E}))$
Some familiar and noteworthy logics are defined as follows:
Because all of the results given in this paper are for logics with fusion and the Ackermann truth constant, we save on notation by dropping the superscript. Except for when otherwise stated, we take L to denote 
. Importantly, we have to extend known
$\gamma $
-admissibility results for propositional results to include
$\circ $
and 
. We do so in the appendix, where we drop this notational convention.
Note that the base logic for the paper is 
, which contains the two disjunctive rules (R3) and (R4). It is pointed out in Seki [Reference Seki29] that these two rules are required for the normal models method to work for logics with both fusion and left implication. These logics, in Seki’s terminology are L3 logics. As far as the authors can tell, both rules are required for each of fusion and left implication.
Proposition 2.3 (Conventionally Normal Propositional Logics).
The propositional relevant logic
$\mathbf {G}^{g}$
, any extension of
$\mathbf {G}^{g}$
by axioms and rules with frame postulates being conjunctions of R and N statements (or implications with a single R statement in the antecedent), and several extensions of
$\mathbf {G}^{g}$
with implicational frame conditions with two R statements in which (R3) and (R1) are derivable admit
$\gamma $
[Reference Routley, Plumwood, Meyer and Brady27, Section 5.6]. (See Seki [Reference Seki29] for the refinement from G to
$\mathbf {G}^{g}$
.)
Such logics are also called Conventionally Normal in Routley et al. [Reference Routley, Plumwood, Meyer and Brady27].
Theorem 2.4. For any conventionally normal logic L with (R3) and (R4) admitting
$\gamma $
, the logic L
also admits
$\gamma $
.
Proof. See the appendix.
This last theorem is needed because we include both fusion and little 
in our first-order formulations. We will say more about this fact later.
Definition 2.5 (First-Order Logics).
Let L be a propositional relevant logic (with fusion and 
) defined above. The logic LQ is defined by adding the following axioms and rule schemes, in the first-order language:Footnote
10
-
(
$\forall $
E)
$\forall x \mathcal {A} \rightarrow \mathcal {A}[\tau /x]$
, where
$\tau $
is free for x in
$\mathcal {A}$
-
(
$\exists $
I)
$ \mathcal {A}[\tau /x]\rightarrow \exists x \mathcal {A}$
, where
$\tau $
is free for x in
$\mathcal {A}$
-
(EC)
$\forall x(\mathcal {A}\lor \mathcal {B}^x)\rightarrow \forall x\mathcal {A}\lor \mathcal {B}^x$
-
(dEC)
$ \mathcal {A}^x \wedge \exists x \mathcal {B} \rightarrow \exists x (\mathcal {A}^x \wedge \mathcal {B}) $
-
(A
$\exists $
E)
$\forall x (\mathcal {A} \rightarrow \mathcal {B}^x) \rightarrow (\exists x\mathcal {A} \rightarrow \mathcal {B}^x)$
-
(R
$\forall $
I)
$\mathcal {A}^x \rightarrow \mathcal {B} \Rrightarrow \mathcal {A}^x \rightarrow \forall x\mathcal {B}$
-
(R
$\exists $
E)
$\mathcal {A} \rightarrow \mathcal {B}^x \Rrightarrow \exists x \mathcal {A} \rightarrow \mathcal {B}^x$
Moreover, the logic QL is defined similarly, but without (EC) and (dEC).
The principle (EC) is often desribed as the extensional confinement axiom; together with (dEC), we consider these both to be the extensional confinement axioms.
An important restriction for us is primitive inclusion of
$\circ $
in each of the defined logics. In some first-order logics, an extension with either
$\circ $
or even
$\leftarrow $
(the inclusion of which makes (A
$\exists $
E) derivable) is not a conservative extension [Reference Tedder and Ferenz34]. With fusion, the following formula become a theorem (scheme):
-
(A
$\forall $
I)
$\forall x (\mathcal {A}^x \rightarrow \mathcal {B}) \rightarrow (\mathcal {A}^x \rightarrow \forall x \mathcal {B})$
.
Moreover, with (EC) and (dEC) as the only ‘toggle’ considered in this paper, there are many first-order relevant logics that we do not consider. In a neighbourhood setting, e.g., we can drop (A
$\exists $
E) and (A
$\forall $
I). We may also be able, though not in this paper, to define and explore
$\gamma $
-admissibility in additional first-order relevant logics. We briefly discuss some of this freedom.
The following is a list of further rules and meta-rules to consider.
-
(
${}^d\textrm {R}\forall $
G)
$\mathcal {C}^x \vee \mathcal {B} \Rrightarrow \mathcal {C}^x \vee \forall x\mathcal {B}$
-
(
${}^d\textrm {R}\exists $
G)
$\mathcal {C}^x \vee \mathcal {B} \Rrightarrow \mathcal {C}^x \vee \exists x\mathcal {B}$
-
(
${}^d\textrm {R}\forall $
I)
$\mathcal {C}^x \vee (\mathcal {A}^x \rightarrow \mathcal {B}) \Rrightarrow \mathcal {C}^x \vee (\mathcal {A}^x \rightarrow \forall x\mathcal {B})$
-
(
${}^d\textrm {R}\exists $
E)
$\mathcal {C}^x \vee (\mathcal {A} \rightarrow \mathcal {B}^x) \Rrightarrow \mathcal {C}^x \vee (\exists x \mathcal {A} \rightarrow \mathcal {B}^x)$
-
MR1 If
$\mathcal {A} \Rrightarrow \mathcal {B}$
, then
$\mathcal {C} \vee \mathcal {A} \Rrightarrow \mathcal {C} \vee \mathcal {B}$
, where universal generalization (here, (R
$\forall $
I)Footnote
11
) is not used on a free variable in
$\mathcal {A}$
to obtain
$\mathcal {B}$
. -
MR2 If
$\mathcal {A} \Rrightarrow \mathcal {B}$
, then
$\exists x \mathcal {A} \Rrightarrow \exists x \mathcal {B}$
, where universal generalization is not used on a free variable in
$\mathcal {A}$
to obtain
$\mathcal {B}$
.
It is easy to show that (
${}^d\textrm {R}\forall $
G) is a derivable rule in every first order logic LQ, due to the presence of (EC). (A quick proof uses (EC), (MP), and the derivable (R
$\forall $
G).) In a logic QL, it remains an open question whether or not this rule is derivable/admissible. The rule (
${}^d\textrm {R}\exists $
G) is derivable in every first-order logic, due to (
$\exists $
I). Moreover, since
$\forall x (\mathcal {A}^x \rightarrow \mathcal {B}) \rightarrow (\mathcal {A}^x \rightarrow \forall x \mathcal {B})$
is a theorem of any first-order logic (as defined in this paper), it is easy to show that (
${}^d\textrm {R}\forall $
I) is also a derivable rule with (R3). The case is similar for (
${}^d\textrm {R}\exists $
E), requiring (R3) again. Note, however, that (EC) and (dEC) are not needed for (
${}^d\textrm {R}\forall $
I) and (
${}^d\textrm {R}\exists $
E).
We therefore know then that LQ will have each of the four disjunctive rules above, and that QL sometimes has some of these rules. In 3, we show
$\gamma $
-admissibility for QL and LQ, provided that L admits
$\gamma $
by normal models.
Finally, note that, as shown in Ferenz [Reference Ferenz8], (A
$\exists $
E) and (A
$\forall $
I) are valid in the Mares-Goldblatt semantics for relational semantics. In contrast, in Brady’s presentation of the content semantics of Brady [Reference Brady4], the base first-order relevant logics do not include these axioms (but do include the extensional confinement axiom(s)), although the later presentation in Brady [Reference Brady5] incorporates (A
$\exists $
E) and (A
$\forall $
I) into the setting of content semantics. While we get (A
$\forall $
I) for free using fusion, (A
$\exists $
E) is nonetheless valid on the Mares–Goldblatt semantics. (This also means that fusion does not conservatively extend Brady’s base system.) This contrast shows that the Mares–Goldbatt semantics and Brady’s content semantics diverge for first-order logics based on weak propositional relevant logics (at least for those captured by a relational semantics).
2.2 Mares–Goldblatt semantics
The target semantics is based on ternary relational semantics.
Definition 2.6 (Ternary Relational Frames).
A ternary relational frame for B
is a tuple
$\mathfrak {F} = \langle W, N, R, *\rangle $
where
$\emptyset \neq N \subseteq W$
,
$R \subseteq W^3$
,
$*:W\longrightarrow W$
, and we further define, for each
$a, b \in W$
,
$ a \leq b =_{df} \exists x \in N(Rxab)$
. Moreover, the following conditions are satisfied:
-
(
$c1$
)
$\leq $
is a preorder on W; -
(
$c2$
) N is an (
$\leq $
-)upset;Footnote
12
-
(
$c3$
) If
$a \leq a', b \leq b', c' \leq c,$
and
$Ra'b'c'$
, then
$Rabc$
(
$R\downarrow \downarrow \uparrow $
) -
(
$c4$
)
$b\leq c$
implies
$c^*\leq b^*$
; -
(
$c5$
)
$a^{**} = a$
.
A ternary relational model for B
is a frame with a valuation function
$||{-}||$
that assigns an upset
$||p|| \subseteq W$
to each propositional variable p. This assignment is extended to all formulas by the following:Footnote
13
For models for logics extending B: we provide the following list of frame conditions (saving space by writing an axiom’s name instead of the entire axiom):
-
(cA1)
$a\in N\mbox { }\Rightarrow \mbox { }a^*\leq a$
-
(cA2)
$Raaa$
-
(cA3)
$Rabc\mbox { }\Rightarrow \mbox { }\exists x\in W(Rabx\mbox { }\&\mbox { }Raxc)$
-
(cA4)
$Rabc\mbox { }\Rightarrow \mbox { }\exists x\in W(Rabx\mbox { }\&\mbox { }Rxbc)$
-
(cA5)
$Rabc\mbox { }\Rightarrow \mbox { }Rbac$
-
(cA6)
$Rabc\mbox { }\Rightarrow \mbox { }b\leq c$
-
(cA7)
$Rabc\mbox { }\Rightarrow \mbox { }a\leq c$
-
(cA8)
$Rabc\mbox { }\&\mbox { }Rcdf\mbox { }\Rightarrow \mbox { }Radf\mbox { }\&\mbox { }Rbdf$
-
(cA9)
$Rabc\mbox { }\Rightarrow \mbox { }a\leq c\mbox { or }b\leq c$
-
(cA10)
$Rabc\mbox { }\Rightarrow \mbox { }Rbac\mbox { }\&\mbox { }a\leq c$
-
(cA11)
$Rabc\mbox { }\Rightarrow \mbox { }\exists x\in W(b\leq x\mbox { }\&\mbox { }c^*\leq x\mbox { }\&\mbox { }Raxb^*)$
-
(cA12)
$Ra^*aa^*$
-
(cA13)
$Raa^*a$
-
(cA14)
$Rabc\mbox { }\Rightarrow \mbox { }Rac^*b^*$
-
(cA15)
$a^{*}\leq a$
-
(cA16)
$Rabc\mbox { }\Rightarrow \mbox { }a\leq b^{*}$
-
(cA17)
$Rabc\mbox { }\&\mbox { }Rcdf\mbox { }\Rightarrow \mbox { }\exists x\in W(Radx\mbox { }\&\mbox { }Rbxf)$
-
(cA18)
$Rabc\mbox { }\&\mbox { }Rcdf\mbox { }\Rightarrow \mbox { }\exists x\in W(Rbdx\mbox { }\&\mbox { }Raxf)$
-
(cA19)
$Rabc\mbox { }\&\mbox { }Rcdf\mbox { }\Rightarrow \mbox { }\exists x\in W(Radx\mbox { }\&\mbox { }Rxbf)$
-
(cA20)
$Rabc\mbox { }\&\mbox { }Rcdf\mbox { }\Rightarrow \mbox { }\exists x,y\in W(Radx\mbox { }\&\mbox { }Rbdy\mbox { }\&\mbox { }Rxyf)$
-
(cA21)
$Rabc\mbox { }\&\mbox { }Rcdf\mbox { }\Rightarrow \mbox { }\exists x,y\in W(Radx\mbox { }\&\mbox { }Rbdy\mbox { }\&\mbox { }Ryxf)$
-
(cA22)
$Rabc\mbox { }\&\mbox { }Rcdf\mbox { }\Rightarrow \mbox { }\exists x\in W(b\leq x\mbox { }\&\mbox { }d\leq x\mbox { }\&\mbox { }Raxf)$
-
(cR1)
$a\in N\mbox { }\Rightarrow Ra^*aa^*$
-
(cR2)
$a\in N\mbox { }\Rightarrow \mbox { }Raa^*a$
-
(cR3)
$a\in N\mbox { }\Rightarrow \mbox { }Raaa$
-
(cR4)
$a\in N\mbox { }\&\mbox { }Rabc\mbox { }\Rightarrow \mbox { }Rac^*b^*$
-
(cR5)
$\exists x\in N(Raxa)$
-
(cR6)
$a\in N\mbox { }\&\mbox { }Rabc\mbox { }\&\mbox { }Rcdf\mbox { }\Rightarrow \mbox { }\exists x,y\in W(Radx\mbox { }\&\mbox { }Rbxy\mbox { }\&\mbox { }Rayf)$
(This list is to be read as
$(cX)$
is the frame condition corresponding to the axiom of rule scheme (X).)
Definition 2.7 (Models for LQ).
A Mares–Goldblatt frame for LQ
(an LQ-frame), for a propositional relevant logic L is a tuple
$\mathfrak {F} = \langle W, N, R, *, U, Prop, PropFun\rangle $
, where
$\langle W, N, R, *\rangle $
is an
$\textbf {L}$
-frame, U is a non-empty set, and we have that
$ Prop \subseteq \wp (W)^{\uparrow }$
,
$PropFun \subseteq \{\varphi : U^\omega \longrightarrow Prop\}$
. Moreover, the following conditions are satisfied:
-
(
$cq1$
)
$Prop$
contains N, and is closed under
$\cap , \cup , \neg , \rightarrow , \circ $
; -
(
$cq2$
)
$PropFun$
contains a constant function
$\varphi _N \ (\varphi _Nf = N)$
, and is closed under
$\cap , \cup , \neg \rightarrow , \circ , \forall _n$
and
$\exists _n$
, for every
$n \in \omega $
, where-
(a)
$(\neg \varphi ) f = \neg (\varphi f)$
-
(b)
$( \varphi \otimes \psi ) f = \varphi f \otimes \psi f$
, for each
$\otimes \in \{\cap , \cup , \rightarrow , \circ \}$
-
(c)
-
(d)
$(\exists _n\varphi )f=\underset {g \sim _{x_n} f}{\bigsqcup }\varphi g=\bigcap \{X\in Prop\mid \underset {g \sim _{x_n} f}{\bigcup }\varphi g\subseteq X\}.$
-
-
(
$cq3$
) For every
$\varphi \in PropFun$
,
$X, Y \in Prop$
,
$n \in \omega $
, and
$f \in U^{\omega }$
Footnote
14
-
(cEC)
$X-Y \subseteq \underset {j \in U}{\bigcap }\varphi (f[j/n]) \text { only if } X-Y \subseteq (\forall _n \varphi )f$
-
(cdEC)
$ \underset {j \in U}{\bigcup }\varphi (f[j/n]) \subseteq X \cup \overline {Y} \text { only if } (\exists _n \varphi )f \subseteq X \cup \overline {Y.}$
-
A pre-model for LQ
is a tuple
$ \mathfrak {M} = \langle F, |{-}| \rangle $
such that F is a Mares–Goldblatt frame for LQ and
$|{-}|$
is a valuation function that assigns:
-
1. an individual
$|c| \in U$
to each constant symbol c; -
2. a function
$|P^n|: U^n \longrightarrow \wp (W)$
to each n-ary predicate symbol
$P^n$
; and -
3. a propositional function
$|\mathcal {A}|: U^\omega \longrightarrow \wp (W)$
to each formula
$\mathcal {A}$
such that, when
$\mathcal {A}$
is atomic, for every
$f \in U^\omega $
: where “
$$ \begin{align*} |P^n\tau_1, \dots, \tau_n|f &= |P^n|(|\tau_1|f, \dots |\tau_n|f) \end{align*} $$
$|\tau |f$
” is
$fn$
when
$\tau $
is the variable
$x_n$
, and
$|c|$
when
$\tau $
is constant symbol c. Moreover, when
$\mathcal {A}$
is not atomic (or ), the valuation is extended as follows:
), the valuation is extended as follows:
A model for LQ
is a pre-model for LQ that assigns an element of
$Prop$
to each atomic formula.
A formula
$\mathcal {A}$
is satisfied by a variable assignment f in a model
$\mathfrak {M}$
, written
$\mathfrak {M}, f \vDash \mathcal {A}$
, when
$N \subseteq |\mathcal {A}|f$
. A formula is valid in a model
$\mathfrak {M}$
(
$\mathfrak {M} \vDash \mathcal {A}$
) when it is satisfied by every variable assignment in that model; valid in a frame
$\mathfrak {F}$
(
$\mathfrak {F} \vDash \mathcal {A}$
) when it is valid in every model based on that frame; valid in a class of frames
$\mathbb {C}$
(
$\mathbb {C} \vDash \mathcal {A}$
) when it is valid in every frame in that class. Admissibility of a rule in the semantic context is understood as the preservation of validity.
Proposition 2.8 (Soundness and Completeness for LQ).
For a wide class of logics including B and its usual extensions, Ferenz [Reference Ferenz8] has shown that LQ is sound and complete w.r.t. the class of LQ-frames.
To prepare the reader for the proof of
$\gamma $
-admissibility, we will briefly sketch the technique of normalization and describe its history. Although the problem of
$\gamma $
-admissibility was tackled by Meyer & Dunn [Reference Meyer and Dunn20], the algebraic techniques employed there are relatively involved. Routley & Meyer [Reference Routley, Meyer and Leblanc26] offered a new technique of normalization as a simpler and more elegant form of argument of
$\gamma $
-admissibility whose development would continue in Routley & Meyer [Reference Routley and Meyer25] and Routley et al. [Reference Routley, Plumwood, Meyer and Brady27]. The shape of the technique is straightforward: A Routley–Meyer model is described as normal if for some normal point a,
$a=a^{\ast }$
, i.e., some normal point is its own star point.Footnote
15
Not all R models are normal (and a fortiori for weaker relevant logics), but surprisingly Routley & Meyer [Reference Routley, Meyer and Leblanc26] describe a recipe through which one can pick an arbitrary point
$o \in N$
and normalize a model to include a point
$0 \in N$
such that
$o^{\ast }\leq 0=0^{\ast }\leq o$
. In particular, the condition for the excluded middle entails that
$o^{\ast } \leq o$
, and we ensure that the new
$0$
is a negation–consistent point. We may think of
$0$
as a consistentized version of o. If the logic is sound and complete with respect to normal models with appropriate frame conditions, then, if
$\neg \mathcal {A}\vee \mathcal {B}$
and
$\mathcal {A}$
are theorems, they will be true in
$0$
. Since
$0=0^{\ast }$
, we can conclude that
$\mathcal {A}$
is not true at
$0$
, whence by the truth conditions for disjunction,
$\mathcal {B}$
will be true at
$0$
and also at o. As o was arbitrarily selected, this means that
$\mathcal {B}$
is semantically valid and thus a theorem by completeness.
This sketch, of course, has a great many subtleties and nuances. It is the task of the next section to fill in the gaps and transform this sketch into a proof.
3
$\gamma $
-Admissibility for QL and LQ logics
While explicitly stated in some definitions and lemmata, in this section we assume L to denote a propositional relevant logic that admits
$\gamma $
via the normal models method and contains (R3) and (R4): that is, a conventionally normal L3 extension of
$\mathbf {G}^{g,d}$
. The keystone of this paper is the method of normal models, so we present the crucial definition.
Definition 3.9 (Normal Models).
For any logic LQ or QL (based on a propositional relevant logic L with (R3) and (R4) admitting
$\gamma $
by the normal models method) defined above, an LQ-(QL-)model (-frame) is normal if it satisfies the following:
-
(Norm)
$a=a^*$
, for some
$a \in N$
.
Definition 3.10 (Normalization of a frame
$\mathfrak {F}$
).
Where L is a conventionally normal L3 logic,
$0 \not \in W$
and
$o \in N$
, the normalization of a QL-frame or LQ-frame
$\mathfrak {F} = \langle W, N, R, *, U, Prop, PropFun \rangle $
is a frame
$\langle W', N', R', *', U, Prop', PropFun' \rangle $
, defined by:Footnote
16
-
1.
$W' = W \cup \{0\}$
; -
2.
$N' = N \cup \{0\}$
; -
3.
$R'$
is given by
$R'abc$
iff
$Rabc$
, whenever
$a, b, c \in W$
, and when
$a, b \in W$
,
$R'$
satisfies the following-
(a)
$R'000$
; -
(b)
$R'00a$
iff
$R'ooa$
; -
(c)
$R'0a0$
iff
$R'oao^*$
; -
(d)
$R'a00$
iff
$R'aoo^*$
; -
(e)
$R'0ab$
iff
$R'oab$
; -
(f)
$R'a0b$
iff
$R'aob$
; -
(g)
$R'ab0$
iff
$R'abo^*$
;
-
-
4.
$*'$
is defined by:-
(a)
$a^{*'} = a^*$
when
$a \in W$
; -
(b)
$0^{*'} = 0$
;
-
-
5. For each
$X \in Prop$
, add
$X \in Prop'$
when
$o^\ast \not \in X$
and, when
$o \in X$
,
$X\cup \{0\} \in Prop'$
; -
6. For each
$\varphi \in PropFun$
, add
$\varphi $
and
$\varphi '$
to
$PropFun'$
, where
$\varphi '$
is defined by:Footnote
17
$$\begin{align*}\forall f \in U^\omega,\ o \in \varphi f \text{ implies } \varphi'f = \varphi f \cup \{0\}.\end{align*}$$
We called this normalized frame the normalization of
$\mathfrak {F}$
at
$0$
for
$o \in N$
.
The proof of the following Lemma and Corollary are standard. That is, note that their statement and proof (as in, e.g., Seki [Reference Seki29]) relies only on the propositional machinery of a frame:
$U, Prop$
, and
$PropFun$
are irrelevant.
Lemma 3.11. If
$\mathfrak {F}$
is an QL- or LQ-frame (for conventionally normal L3 L) and
$\mathfrak {F}'$
is a normalization of
$\mathfrak {F}$
at
$0$
for o:
-
1. the relation
$R'$
is well-defined; -
2. the ordering
$\leq '$
is such that, for all
$a, b \in W$
:-
(a)
$a \leq ' b$
iff
$a \leq b$
; -
(b)
$0 \leq ' b$
iff
$o \leq b$
; -
(c)
$a \leq ' 0$
if
$a \leq o^*$
.
-
Corallary 3.12. If
$\mathfrak {F}$
is an QL- or LQ-frame (for conventionally normal L3 L) and
$\mathfrak {F}'$
is a normalization of
$\mathfrak {F}$
at
$0$
for o, then
$o^* \leq 0 \leq o$
.
The next lemma does require extra verification of the first-order machinery. Of course, U is unaffected, but we must show that
$Prop$
and
$PropFun$
are well-defined and closed under the required operations.
Lemma 3.13. Suppose that L is a propositional relevant logic (extending
$\mathbf {G}^{g,d}$
) which admits
$\gamma $
(by the method of normalizing models). Let
$\mathfrak {F}$
be a QL- or LQ-frame and
$$\begin{align*}\mathfrak{F}' = \langle W', N', R', *', U, Prop', PropFun' \rangle,\end{align*}$$
the normalization of
$\mathfrak {F}$
at
$0$
for o. Then
$\mathfrak {F}'$
is also a QL- or LQ-frame, respectively.
Proof. Here we must check every frame postulate. By the supposition that L admits
$\gamma $
by the method of normalization (see the appendix), we can use the arguments of Routley et al. [Reference Routley, Plumwood, Meyer and Brady27, pp. 389–390] Seki [Reference Seki29, pp. 214–216] to cover to show that the frame postulates corresponding to L (including those of
$\mathbf {G}^{g,d}$
) are satisfied (with respect to
$W', N', R'$
and
$*'$
).
What remains to show is that
$Prop'$
and
$PropFun'$
and well defined and that conditions (cq1) and (cq2) hold for QL, and additionally that (cq3) holds for LQ.
$Prop'$
is well-defined: We need to check that each element of
$Prop'$
is an
$\leq $
-upset. For each such X not containing
$0$
, we need to show that
$o^\ast \not \in X$
, but this is so by definition. Suppose that
$0 \in X' \in Prop'$
, and that
$\exists y \in X'(y \leq z \ \& \ z \not \in X')$
. As
$X'$
comes from an element, say X, of
$Prop$
, such a y cannot exist in
$X'$
. So let
$y=0$
. This means that
$0 \leq z$
and
$z \not \in X'$
. However, by Lemma 3.11(2).(b),
$o \leq z$
and thus
$z \in X$
, a contradiction. Hence
$Prop$
is well-defined.
$PropFun'$
is well-defined: It is easy to see that each element
$\varphi \in PropFun'$
is a function that produces a unique element of
$Prop'$
as output, given a particular input.
(cq1): Suppose that
$X', Y' \in Prop'$
(and that
$X'=X\cup \{0\}$
, if
$0 \in X'$
, for some
$X \in Prop$
, a similarly for
$Y/Y'$
). We give the cases as follows:
-
$\cap $
If
$0 \not \in X', Y'$
, then
$0 \not \in X' \cap Y' \in Prop$
, and hence in
$Prop'$
. If
$0 \in X'$
but
$0 \not \in Y'$
, then
$X'\cap Y' = X\cap Y \in Prop'$
. If
$0 \in X', Y'$
, then
$X'\cap Y' = \{0\}\cup (X \cap Y)$
, and
$X \cap Y \in Prop$
. (The remaining sub-cases are symmetrical to the second sub-case.)
-
$\cup $
This case is similar to the previous case. One sub-case is shown. Suppose that
$0 \in X', Y'$
. Then
$X' \cup Y' = \{0\} \cup (X \cup Y)$
, where
$X \cup Y \in Prop$
.
-
$\neg $
Either
$0 = 0^* \in X'$
or not. If it is, then
$o \in X$
. Then
$o^* \not \in \neg X$
, and
$o \not \in \neg X$
. From the latter,
$\neg X' = \neg X \in Prop$
. On the other hand, the assumption that
$0 \not \in X' (= X)$
implies that
$o \not \in X$
. Thus
$o^* \in \neg X$
, and by Lemma 3.12 we have
$o \in \neg X$
, and so
$0 \in \neg X'= \{0\}\cup \neg X$
.
-
$\rightarrow $
The case where
$X'=X$
and
$Y'=Y$
is trivial. Suppose that
$X'=X\cup \{0\}$
and
$Y'=Y$
. We know that
$Ra0c$
iff
$Raoc$
, and
$X'\rightarrow Y = \{a \in W' : \forall b, c ((Rabc \ \& \ b \in X') \Rightarrow c \in Y) \}$
, which means that
$a \in X' \rightarrow Y$
iff
$a \in X \rightarrow Y$
, which means that
$X'\rightarrow Y = X\rightarrow Y \in Prop'$
.
On the other hand, if
$X' = X$
and
$Y'=Y\cup \{0\}$
, then we note that
$R'ab0$
iff
$Rabo^*$
. So
$X' \rightarrow Y' = X\rightarrow Y'$
. If
$a \in X\rightarrow Y'$
and
$R'ab0$
, then
$R'abo^*$
, and so
$a \in X\rightarrow Y$
.Finally, suppose that
$X'=X\cup \{0\}$
and
$Y'=Y\cup \{0\}$
. We combine the reasoning of the previous two cases to show
$X'\rightarrow Y' = X \rightarrow Y$
. (Using
$R'a00$
iff
$R'aoo^*$
where needed.) -
$\circ $
Similar to the
$\rightarrow $
case.
(cq2): Suppose that
$\varphi ', \psi ' \in PropFun$
: The cases are as follows:
-
$\varphi ^{\prime }_{N'}$
It is easy to check that
$(\varphi _N)'$
is our desired
$\varphi ^{\prime }_{N'}$
.
-
$\cap $
For the remaining cases, we show only the subcases where one of
$\varphi '$
or
$\psi '$
is not in
$PropFun$
. It is easy to check that, for each
$f \in U^\omega $
,
$\varphi 'f \cap \psi 'f = (\varphi \cap \psi )'f$
, which shows that
$PropFun'$
is closed under (the lifted operator)
$\cap $
.
-
$\cup $
Similar to the previous case.
-
$\neg $
We show that
$\neg (\varphi 'f) = (\neg \varphi )'f$
, for each
$f \in U^\omega $
. If
$0 \not \in \neg (\varphi 'f)\cup (\neg \varphi )'f$
, then
$\neg (\varphi 'f) = \neg (\varphi f) = (\neg \varphi )f= (\neg \varphi )'f$
. On the other hand,
$0 (0^*) \in \neg (\varphi 'f)$
iff
$0^* (0) \not \in (\varphi 'f)$
iff
$o^* \not \in (\varphi )f$
iff
$o \in \neg (\varphi f) = (\neg \varphi )f$
iff
$0 \in (\neg \varphi )'f$
.
-
$\rightarrow $
Fixing an f, we must show that
$(\varphi '\rightarrow \psi ')f=(\varphi \rightarrow \psi )'f$
. To handle multiple cases in parallel, let the notation
denote a in case
$a\neq 0$
and
$0$
otherwise. Then for left-to-right, we prove the contrapositive. If
then
, meaning that there exist
$b,c\in W$
such that
and
$b\in \varphi {f}$
and
$c\notin \psi {f}$
, i.e., there is a counterexample. Counterexamples will lift to the new model, i.e.,
will hold. Also as
$\varphi {f}\subseteq \varphi '{f}$
,
$b\in \varphi '{f}$
and as
$\psi '{f}\cap W=\psi {f}$
, that
$c\notin \psi {f}$
entails that
$c\notin \psi '{f}$
. Together,
. For right-to-left, if
then
, meaning that in the original model for all
$b,c\in W$
such that
, if
$b\in \varphi {f}$
then
$c\in \psi {f}$
. Suppose for contradiction that
. Then there are
$d,e,\in W'$
for which
while
$d\in \varphi '{f}$
and
$e\notin \psi '{f}$
. But (using the same notation) this means that in the original model
with
and
. But since this takes place in the original model,
would be forced to be a member of
$\psi {f}$
. Consequently,
.
-
$\circ $
Similar to the
$\rightarrow $
case.
-
$\forall _n$
We show that
$(\forall _n \varphi ')f = (\forall _n \varphi )'f$
, for every
$f \in U^\omega $
. Fix an arbitrary
$f \in U^\omega $
. There are two distinct cases to consider
$0 \in (\forall _n \varphi )'f$
and
$0 \not \in (\forall _n \varphi )'f$
.For the latter, that is
$0 \not \in (\forall _n \varphi )'f$
, this entails that
$o \not \in (\forall _n \varphi )f$
. That is, for all
$X \in Prop$
,
$X \subseteq \bigcap _{g \sim _x f} (\varphi g)$
entails
$o \not \in X$
. By definition, it follows that each
$\varphi ' g \in \bigcap _{g \sim _x f} (\varphi 'g)$
does not contain
$0$
. And so, . That
$(\forall _n \varphi ')f = (\forall _n \varphi )'f$
follows from the fact that each set belongs to the original model, where the identity holds.
Now suppose that
$0 \in (\forall _n \varphi )'f$
. Then
$o \in (\forall _n \varphi )f$
and thus
$o \in X \subseteq \bigcap _{g \sim _x f} (\varphi g)$
for some
$X \in Prop$
. Then
$o \in \varphi g$
for every g. Let us denote
$X \cup \{0\}$
by
$X'$
. Then
$X' \subseteq \bigcap _{g \sim _x f} (\varphi 'g)$
, as by definition
$\varphi 'g$
must include
$0$
. But then
$0 \in (\forall _n \varphi ')f$
. Using the fact that
$0 \in (\forall _n \varphi ')f$
iff
$0 \in (\forall _n \varphi )'f$
, we now show the identity
$(\forall _n \varphi ')f = (\forall _n \varphi )'f$
. The
$a=0$
case is covered by what we have already shown. If
$a\neq 0$
, then the corresponding identity of the original model is sufficient. -
$\exists _n$
Similar but dual to the previous case.
. That 
This completes the QL portion of the lemma. The remaining case concerns LQ.
(cq3): We show only the sub-case for (cEC). Assume that
$X', Y' \in Prop'$
,
$\varphi ' \in PropFun'$
,
$n \in \omega $
, and
$f \in U^\omega $
. Further suppose that
$X'-Y' \subseteq \underset {j \in U}{\bigcap }\varphi ' (f[j/n])$
. There are two cases.
-
Case 1:
$0 \in X'-Y'$
, which is
$0 \in X'$
and
$0 \not \in Y'$
. Then
$0 \in \underset {j \in U}{\bigcap }\varphi ' (f[j/n])$
. Thus,
$0 \in \varphi ' (f[j/n])$
for each
$j \in U$
. We want to show that there is an
$X \in Prop'$
such that
$0 \in X \subseteq \varphi ' (f[j/n])$
for each
$j \in U$
. Consider the set
$\forall _n \varphi ' f \cup \{0\}$
. This is indeed an element of
$Prop'$
:
$0 \in \varphi ' (f[j/n])$
entails
$o \in \varphi ' (f[j/n])$
, which forces in turn both
$o \in \forall _n \varphi ' f$
and
$0 \in \forall _n \varphi ' f \cup \{0\} \in Prop'$
. This completes the case with
$X = \forall _n \varphi ' f \cup \{0\}$
. Because the original frame satisfied (cEC), we have shown that every element of
$X'-Y'$
is an element of
$(\forall _n \varphi ')f$
, as required. -
Case 2:
$0 \not \in X'-Y'$
. We assume that
$X'-Y' \subseteq \underset {j \in U}{\bigcap }\varphi ' (f[j/n])$
. As
$0 \not \in X'-Y'$
, the result follows from the original model satisfying (cEC) and the fact that both
$\underset {j \in U}{\bigcap }\varphi ' (f[j/n])$
and
$(\forall _n \varphi ')f$
are either equal to their corresponding sets in the original model, or additionally contain
$0$
.
As each normalized frame is a frame of the right kind, soundness for the corresponding logic is straightforward. We record this fact.
Lemma 3.14 (Normal Soundness).
For any formula
$\mathcal {A}$
, if
$\mathcal {A}$
is a theorem of QL or LQ on L3 L, then
$\mathcal {A}$
is valid in every normal QL-frame or LQ-frame, respectively.
Given a LQ-model’s valuation, we define the standard valuation for the normalization of the model’s frame in the following definition. Note that other valuations are possible, but that this standard normalization valuation plays a key role in what’s to come.
Definition 3.15. If
$\mathfrak {M} = \langle \mathfrak {F}, |{-}|\rangle $
is an QL- or LQ-model (for conventionally normal L3 logic L), we take as the standard normalization of model
$\mathfrak {M}$
at
$0$
(for
$0 \in N$
) to be the tuple
$\mathfrak {M}' = \langle \mathfrak {F}', |{-}|'\rangle $
, where
$\mathfrak {F}'$
is the normalization of
$\mathfrak {F}$
(at o), and
$|{-}|'$
is defined as follows:Footnote
18
-
1.
$|c|' = |c|$
; -
2. for all
$\vec {j}\in \mathcal {U}^{n}$
:
$|P^n|'(\vec {j}) = |P^n|(\vec {j})$
, if
$o \not \in |P^n|(\vec {j})$
, and
$(|P^n|(\vec {j})) \cup \{0\}$
if
$o \in |P^n|(\vec {j})$
; -
3. A propositional function
$|\mathcal {A}|'$
is given to each formula in the usual way, given the previous two clauses.
Lemma 3.16. Let L be a conventionally normal L3 propositional relevant logic. Given a QL- or LQ-model
$\mathfrak {M} = \langle \mathfrak {F}, |{-}|\rangle $
, the standard normalization
$\mathfrak {M}' = \langle \mathfrak {F}', |{-}|'\rangle $
of
$\mathfrak {M}$
is a QL- or LQ-model, respectively.
Proof. The underlying frame is an QL- or LQ-frame, as per Lemma 3.13. It remains to be shown that the valuation assigns an element of
$PropFun'$
to each atomic proposition. That every formula is assigned an element of
$PropFun'$
follows from each atomic formula being assigned an element of
$PropFun'$
together with the fact that
$PropFun'$
is closed under the required operations.
It is straightforward to check that each atomic formula is mapped to an element of
$PropFun'$
. As
$PropFun'$
is closed under the appropriate operators, it follows in the usual way that each formula is mapped to an element of
$PropFun'$
.
Lemma 3.17. Let
$\mathfrak {M}$
be a QL- or LQ-model with set W (for conventionally normal L3 logic L). Further let
$\mathfrak {M}'$
be the standard normalization of
$\mathfrak {M}$
. For all
$a \in W$
, for every formula
$\mathcal {A}$
and
$f \in U^\omega $
,
$a \in |\mathcal {A}|f$
iff
$a \in |\mathcal {A}|'f$
.
Proof. The proof is by induction on the complexity of
$\mathcal {A}$
. If
$\mathcal {A}$
is the atomic
$P\tau _1,\dots , \tau _n$
, then
$|P\tau _1,\dots , \tau _n|'f = |P|' (|\tau _1|'f, \dots , |\tau _n|f)$
. For each
$|\tau _i|'f$
,
$|\tau _i|'f = |\tau _i|f$
. Thus, by definition,
$|P\tau _1,\dots , \tau _n|'f$
restricted to W is
$|P\tau _1,\dots , \tau _n|f$
, as required. The case for 
is straightforward. For the inductive cases, we only show a couple.
Case
$\mathcal {A} = \mathcal {B}\vee \mathcal {C}$
: Suppose that
$a \in W$
and
$f \in U^\omega $
. If
$a \in |\mathcal {B} \vee \mathcal {C}|f$
, then by (a couple suppressed steps) the inductive hypothesis either
$a \in |\mathcal {B}|'f$
or
$a \in |\mathcal {C}|'f$
, which entails that
$a \in |\mathcal {B} \vee \mathcal {C}|'f$
, as required. The other direction is similarly straightforward.
Case
$\mathcal {A} = \mathcal {B}\rightarrow \mathcal {C}$
: Right-to-left is trivial as
$R'$
and R agree on all arguments from W. For left-to-right, suppose that
$a\in |\mathcal {B}\rightarrow \mathcal {C}|f$
. Then for all
$b,c\in W$
such that
$Rabc$
and
$b\in |\mathcal {B}|f$
, also
$c\in |\mathcal {C}|f$
. By induction hypothesis, this entails that for all
$b,c\in W$
such that
$R'abc$
and
$b\in |\mathcal {B}|'f$
, also
$c\in |\mathcal {C}|'f$
. This is nearly sufficient to establish that
$a\in |\mathcal {B}\rightarrow \mathcal {C}|f$
; it could go away only in case
$R'ab'c'$
,
$b'\in |\mathcal {B}|'f$
, and
$c'\in |\mathcal {C}|'f$
when either
$b'=0$
or
$c'=0$
. But in such cases, one could select appropriate
$b"=o$
or
$c"=o^*$
such that
$R'ab"c"$
while
$b"\in |\mathcal {B}|'f$
and
$c"\notin |\mathcal {C}|'f$
. As
$a,b",c"\in W$
, though, this is impossible, as it would entail that
$c"\in |\mathcal {C}|'f$
. Thus
$a\in |\mathcal {B}\rightarrow \mathcal {C}|'f$
, as required.
Case
$\mathcal {A} = \forall x_n\mathcal {B}$
: Suppose that
$a \in W$
,
$f \in U^\omega $
and that
$a \in |\forall x_n \mathcal {B}|f$
. Then
$a \in X \in Prop$
and
$X \subseteq \bigcap _{g \sim _{x_n} f} |\mathcal {B}|g$
. Then
$a \in |\mathcal {B}|g$
, for each
$g \sim _{x_n} f$
. By the induction hypothesis, for all
$b \in W$
,
$b \in |\mathcal {B}|'g$
iff
$b \in |\mathcal {B}|'g$
, for each such g. Thus (i)
$a \in \bigcap _{g \sim _{x_n} f} |\mathcal {B}|'g$
and (ii)
$X \subseteq \bigcap _{g \sim _{x_n} f} |\mathcal {B}|'g$
(because
$X \subseteq W$
). Then
$a \in X \in Prop'$
and
$X \subseteq \bigcap _{g \sim _{x_n} f} |\mathcal {B}|g$
, which is that
$a \in |\forall x_n \mathcal {B}|'f$
, as required.
For the other direction, assume that
$a \in W$
,
$f \in U^\omega $
and that
$a \in |\forall x_n \mathcal {B}|'f$
. Then
$a \in X' \in Prop'$
and
$X' \subseteq \bigcap _{g \sim _{x_n} f} |\mathcal {B}|'g$
. Consider X, which is equal to
$X'$
if
$X'\subseteq W$
, and is
$X' - \{0\}$
otherwise. Clearly
$X \in Prop$
. Moreover, by the transitivity of the subset relation,
$X \subseteq \bigcap _{g \sim _{x_n} f} |\mathcal {B}|'g$
, and also we have
$a \in X$
. Now, by the induction hypothesis, for every
$b \in W$
,
$b \in |\mathcal {B}|'g$
iff
$b \in |\mathcal {B}|'g$
, for each such g. Thus we infer that
$X \subseteq \bigcap _{g \sim _{x_n} f} |\mathcal {B}|g$
, and so
$a \in |\forall x_n \mathcal {B}|f$
.
Theorem 3.18. For any formula
$\mathcal {A}$
and any L3 logic L admitting
$\gamma $
by normal models,
$\mathcal {A}$
is a theorem of LQ (QL) iff
$\mathcal {A}$
is valid in every normal LQ-frame (QL-frame).
Proof. The only if direction is soundness, and is covered by Lemma 3.14. For the if direction, suppose that
$\mathcal {A}$
is not a theorem of LQ (QL). Then there is a canonical LQ-model (QL-model) with frame
$\mathfrak {F} = \langle W, N, R, 0, U, Prop, PropFun\rangle $
, (canonical) valuation
$|{-}|$
, and
$o \in N$
such that
$o \not \in |\mathcal {A}|f$
, for some
$f \in U^\omega $
.
For a new
$0$
, take the standard normalization of
$\mathfrak {M}$
(at
$0$
for o), denoted
$\mathfrak {M}' = \langle \mathfrak {F}', |{-}|' \rangle $
. By Lemma 3.16, this
$\mathfrak {M}'$
is a LQ-model (QL-model). By Lemma 3.17,
$o \not \in |\mathcal {A}|'f$
. But
$0 \leq o$
then entails that
$0 \not \in |\mathcal {A}|'f$
, and since
$0 \in N'$
, we have that
$\mathcal {A}$
is not valid on
$\mathfrak {F}$
.
In particular, this proof shows that, for every invalid formula
$\mathcal {A}$
, there is a normal point
$0=0^{\ast }$
in a normal model at which the invalidity of
$\mathcal {A}$
is witnessed. In the proof we took at arbitrary
$o in N$
at which
$\mathcal {A}$
fails and introduced a new point
$0$
which, because of the excluded middle axiom and out construction, is such that
$o^{\ast } \leq 0 \leq o$
. The latter entails that
$0$
is also a point at which
$\mathcal {A}$
fails.
Corallary 3.19. For the logics LQ and QL, where L3 logic L admits
$\gamma $
by normal models, the rule
$\gamma $
is admissible.
Proof. Suppose that
$\neg \mathcal {A} \vee \mathcal {B}$
and
$\mathcal {A}$
are both theorems of LQ. Then by Theorem 3.18, these formulas are valid on every normal model. Consider an arbitrary normal model
$\mathfrak {M} = \langle W, N, R, *, U, Prop, PropFun, |{-}| \rangle $
with normal point
$0$
(
$0=0^*$
). Since
$0 \in N$
,
$0 \in |\neg \mathcal {A} \vee \mathcal {B}|f \cap |\mathcal {A}|f$
for every
$f \in U^\omega $
. Since
$0 \in |\mathcal {A}|f$
and
$0=0^*$
, we have that
$0 \not \in |\neg \mathcal {A}|f$
. But then given the definition of
$|\neg \mathcal {A} \vee \mathcal {B}|f$
,
$0 \in |\mathcal {B}|f$
, as required.
We reintroduce the
$\circ $
and 
notation in a logic’s name for the next corollary, which gives a sufficient condition for
$\gamma $
-admissibility in logics without
$\circ $
and 
.
Corallary 3.20. For every conventionally normal propositional logic L, if LQ
admits
$\gamma $
and conservatively extends LQ, then LQ admits
$\gamma $
.
Proof. Suppose that
$\vdash _{\textbf {LQ}} \mathcal {A}$
and
$\vdash _{\textbf {LQ}} \neg \mathcal {A}\vee \mathcal {B}$
and that
$\mathcal {A}$
and
$\mathcal {B}$
do not contain fusion or 
. Then we have 
since LQ
admits
$\gamma $
. Moreover, since
$\mathcal {B}$
is in the language of LQ, by the conservative extension assumption we have
$\vdash _{\textbf {LQ}} \mathcal {B}$
.
As a result, whenever we can show the conservative extension by
$\circ $
and 
in the first-order case, we can extend our admissibility results to the weaker logics.
4 Concluding remarks
We have shown
$\gamma $
is admissible in a wide range of first-order relevant logics. A major upshot is that we can conceive of many logics QL and LQ as having a well-behaved semantics. Well behaved, that is, in the sense that the machinery for interpreting quantified formulas is sufficiently independent from the propositional machinery required for
$\gamma $
-admissibility. Thus, we have essentially shown that the QL and LQ extensions of L conserve the property of
$\gamma $
-admissibility (w.r.t. the normal models method).Footnote
19
From this point of view, and from the fact that
$\gamma $
-admissibility ensures the set of theorems of a logic is negation consistent (and that the logic contains the set of theorems of classical first-order logic in
$\neg , \vee , \forall $
), we can take the logics that we have shown to admit
$\gamma $
as well-behaved in yet another sense: that the constant domain extensions QL and LQ preserve normal models
$\gamma $
-admissiblity, negation consistency of the set of theorems, and the containment of (the theorems of) their classical counterparts.
There are, however, many other ways to axiomatize first-order extensions of relevant logics. From this work, we plan to extend these results to first-order modal relevant logics and first-order logics that require neighbourhood semantics. (The neighbourhood semantics given in Tedder & Ferenz [Reference Tedder and Ferenz34] is apt for a normal model approach, as negation is treated in a similar way using a star function. Similarly, the framework of Ferenz & Tedder [Reference Ferenz and Tedder10] may be used for weaker modal relevant logics.) For the modal cases, the work of Seki [Reference Seki29] will again be invaluable. In the neighbourhood cases, we are able to better model axiomatizations of first-order logics that, e.g., drop the axiom forms of universal introduction and existential elimination.
A further avenue for future work is to extend the investigation in the paper Ferenz & Ferguson [Reference Ferenz, Ferguson and Sedlár9] in which
$\gamma $
admissibility holds in the case of the varying-domain version of QR described in Mares [Reference Mares18] to examine varying-domain analogues of the weaker relevant logics considered in this paper. Notably, Mares’ system includes an existence predicate that requires some additional consideration when effecting a normalization. The present paper’s emphasis on considering the consequences of additional connectives—like fusion and 
—for the technique of normal models makes this an especially attractive area to explore.
Finally, as a referee has kindly suggested to us, there appears to be some kinship between Slaney’s work on reduced models for weak relevant logics in Slaney [Reference Slaney32] and the techniques employed in this paper. Slaney’s method does not require that a logic has the principle of excluded middle, and so extending his results to first-order relevant logics is a natural step to expand on the results of this paper. We plan on revisiting the connections between normalization and Slaney’s results, as well as exploring the metavaluation method, for first-order relevant logics in future work.
5 Appendix:
$\gamma $
-Admissibility for propositional logics with fusion and
In this appendix, we prove Theorem 2.4 which states that, for any conventionally normal logic L admitting
$\gamma $
, the logic L
also admits
$\gamma $
. The proof will largely follow Seki’s presentation in Seki [Reference Seki29] (minus modalities but tending to the cases of
$\circ $
and 
).
Lemma 5.21. The normalization of an 
frame is an 
frame.
Proof. Let
$\mathfrak {F}'=\langle W',N',R',*'\rangle $
be the normalization of an 
frame
$\mathfrak {F}=\langle W,N,R,*\rangle $
. That
$*'$
is a well-defined unary function is immediate; that
$R'$
is a well-defined ternary relation follows from a similar argument to that found in Routley et al. [Reference Routley, Plumwood, Meyer and Brady27, p. 387].
In particular, we note the following corollaries follow from Lemma 5.21
Corallary 5.22. In a normalization
$\mathfrak {F}'$
based on
$\mathfrak {F}$
, the following hold for all
$a,b\in W$
$$ \begin{align*} \begin{array}{lll} a\leq'b \text{ iff } a\leq b & \hspace{.3cm} & 0\leq' b \text{ iff } o\leq b. \end{array} \end{align*} $$
Corallary 5.23. Let
$\mathfrak {F}'=\langle W',N',R',*'\rangle $
be the normalization of an 
frame
$\mathfrak {F}=\langle W,N,R,*\rangle $
at
$0$
for
$o\in W$
. Then
$o^{*'}\leq '0\leq 'o$
.
From the soundness of 
, the following follows immediately.
Lemma 5.24. If
$\mathcal {A}$
is provable in 
then
$\mathcal {A}$
is valid in every normal 
frame.
At this point, we lift the notion of normalization of a frame to define the normalization of a model.
Definition 5.25. Let
$\langle \mathfrak {F},\lVert - \rVert \rangle $
be an 
model. Then let its normalization be
$\langle \mathfrak {F}',\lVert - \rVert '\rangle $
where
$\mathfrak {F}'$
is the normalization of
$\mathfrak {F}$
and
$\lVert - \rVert '$
is defined so that for atoms p,:
$\lVert p\rVert '=\begin {cases} \lVert p\rVert & \mbox { if }o\notin \lVert p\rVert \\ \lVert p\rVert \cup \lbrace 0\rbrace & \mbox { if }o\in \lVert p\rVert .\\ \end {cases}$
Now, we introduce two lemmata establishing that the normalization of a model will enjoy appropriate properties.
Lemma 5.26. In a normalized 
model,
$\lVert p\rVert '$
is an upset with respect to
$\leq '$
for every atom p.
Proof. By appeal to the model of which the model is a normalization. If
$o\notin \lVert p\rVert $
, then this follows. Otherwise,
$\lVert p\rVert '=\lVert p\rVert \cup \lbrace 0\rbrace $
. Take an arbitrary
$a\in \lVert p\rVert '$
and b such that
$a\leq ' b$
. We prove that
$b\in \lVert p\rVert '$
.
Note again that both
$o\in \lVert p\rVert $
and
$0\in \lVert p\rVert '$
. If
$b=0$
, the result is immediate, so assume that
$b\in W$
. Now, if
$a=0$
, because
$0\leq 'b$
holds precisely when
$o\leq b$
holds in the original model. If
$a\neq 0$
, then because
$b\neq 0$
,
$a\leq 'b$
holds when
$a\leq b$
holds in the original model. In both cases, as
$\lVert p\rVert $
is an upset,
$b\in \lVert p\rVert $
and a fortiori
$b\in \lVert p\rVert '$
Lemma 5.27. In a normalized 
model,
$\lVert \mathcal {A}\rVert '$
is an upset with respect to
$\leq '$
for every formula
$\mathcal {A}$
.
Proof. As
$\langle \mathfrak {F},\lVert - \rVert '\rangle $
is a model, closure of propositions from the basis of Lemma 5.26 follows through a standard inductive argument.
This brings us to the key fact, namely, that a normalized model will agree with the model from which it was constructed. We ensure especially that the semantic clauses for
$\circ $
and 
do not somehow prove problematic.
Lemma 5.28. In a normalized 
model and point
$a\in W$
,
$a\in \lVert \mathcal {A}\rVert $
iff
$a\in \lVert \mathcal {A}\rVert '$
.
Proof. By induction on complexity of
$\mathcal {A}$
. The basis step is provided by definition of the normalized model and most cases are covered as in Routley et al. [Reference Routley, Plumwood, Meyer and Brady27, p. 391]. Given our interest in 
and
$\circ $
, we provide these steps:
$\bullet $
If 
then 
, so this holds for every
$a\in W$
.
$\bullet $
If
$\mathcal {A}=\mathcal {B}\circ \mathcal {C}$
then to show left-to-right, pick an
$a\in \lVert \mathcal {B}\circ \mathcal {C}\rVert $
; this holds precisely when
$b\in \lVert \mathcal {B}\rVert $
and
$c\in \lVert \mathcal {C}\rVert $
such that
$Rbca$
. By induction hypothesis, this entails that
$b\in \lVert \mathcal {B}\rVert '$
and
$c\in \lVert \mathcal {C}\rVert '$
. Additionally, by construction of the normalized frame,
$R'bca$
holds, whence
$a\in \lVert \mathcal {B}\circ \mathcal {C}\rVert '$
. For right-to-left, on the other hand, pick an
$a\in \lVert \mathcal {B}\circ \mathcal {C}\rVert '$
such that
$a\in W$
. Then there are
$b\in \lVert \mathcal {B}\rVert '$
and
$c\in \lVert \mathcal {C}\rVert '$
such that
$R'bca$
. Now, fix the following:
$b'=\begin {cases}b\mbox { if }b\neq 0\\ o\mbox { if }b=0\end {cases}$
and
$c'=\begin {cases}c\mbox { if }c\neq 0\\ o\mbox { if }c=0.\end {cases}$
Notably,
$b'$
and
$c'$
are elements of W. Then either trivially or by construction of
$R'$
, we have that
$Rb'c'a$
and either trivially or by construction of
$\leq '$
, also
$b\leq b'$
and
$c\leq c'$
, whence by Corollary 5.27,
$b'\in \lVert \mathcal {B}\rVert '$
and
$c'\in \lVert \mathcal {C}\rVert '$
. In other words, there are
$b'\in \lVert \mathcal {B}\rVert $
and
$c'\in \lVert \mathcal {C}\rVert $
such that
$Rb'c'a$
, i.e.,
$a\in \lVert \mathcal {B}\circ \mathcal {C}\rVert $
.
One final lemma will suffice to prove Theorem 2.4
Lemma 5.29.
proves
$\mathcal {A}$
iff
$\mathcal {A}$
is valid in every normal 
frame.
Proof. We prove the right-to-left direction via contraposition. Suppose that
$\mathcal {A}$
is not provable in 
. Then there exists a model
$\langle \mathfrak {F},\lVert - \rVert \rangle $
and a normal point
$o\in N$
such that
$o\notin \lVert \mathcal {A}\rVert $
. By Lemma 5.28, in the normalization
$\langle \mathfrak {F},\lVert - \rVert '\rangle $
,
$o\notin \lVert \mathcal {A}\rVert '$
. By Corollary 5.23,
$0\leq '0$
, entailing that
$0\notin \lVert \mathcal {A}\rVert '$
. Because
$0\in N'$
,
$\mathfrak {F}'$
witnesses that
$\mathcal {A}$
is not valid in every normal 
frame.
This brings us to the main theorem concerning 
.
Theorem 2.4.
$\gamma $
is admissible for 
.
Proof. Suppose for contradiction that
$\gamma $
fails, i.e., that there are 
theorems
$\neg \mathcal {A}\vee \mathcal {B}$
and
$\mathcal {A}$
such that
$\mathcal {B}$
is not provable. By Lemma 5.29, there exists an 
model
$\langle \mathfrak {F}',\lVert - \rVert '\rangle $
with
$\mathfrak {F}'$
normal such that
$0\notin \lVert \mathcal {B}\rVert '$
. As
$0\in N'$
, however,
$0\in \lVert \neg \mathcal {A} \vee \mathcal {B}\rVert '$
and
$0\in \lVert \mathcal {A}\rVert '$
. Consequently, either
$0\in \lVert \neg \mathcal {A}\rVert '$
or
$0\in \lVert \mathcal {B}\rVert '$
. Because
$0=0^{*'}$
, the requirement of the former case that
$0^{*'}\notin \lVert \mathcal {A}\rVert '$
translates to
$0\notin \lVert \mathcal {A}\rVert '$
, contradicting the hypothesis that
$0\in \lVert \mathcal {A}\rVert '$
. The latter case is ruled out insofar as
$0$
was assumed not to be a member of
$\lVert \mathcal {B}\rVert '$
. As both disjuncts lead to contradiction, we conclude that
$\gamma $
holds.
Acknowledgments
We would like to thank many comments from participants of several conferences, including Logica 2023, the Second Third Workshop, and the Seminar for Applied Mathematical Logic at the Institute of Computer Science, Czech Academy of Science. We also thank three anonymous reviewers for their comments, which lead to a much better version of the paper.
Funding
Nicholas Ferenz gratefully acknowledged funding from by RVO 67985807 and that this work is also financed by national funds through FCT — Fundação para a Ciência e a Tecnologia, I.P., under the scope of UIDB/00310/2020 project, identified as DOI 10.54499/UIDB/00310/2020.
. MR1 and MR2 are used to define extensions of Brady’s BBQ, where Brady’s BBQ is strictly weaker than what we here would call BBQ. Notably, (A
