Deductive Systems with Multiple-Conclusion Rules and the Disjunction Property

Abstract

Using the defined notion of the inference with multiply-conclusion rules, we show that in the logics enjoying the disjunction property, any derivable rule can be inferred from the single-conclusion rules and a single multiple-conclusion rule, which represents the disjunction property. Also, the conversion algorithm of single- and multiple-conclusion deductive systems into each other is studied.

1. Introduction

The question “What is inference rule?” is almost as profound as the question “What is truth?.” Speaking very generally, inference rules are the acceptable means of reasoning. They give us a way to go from a set of accepted statements (propositions, judgments) to an acceptable statement (proposition, judgment). Rules can be given in different forms: Aristotle used rules in a form of moduses like [1] (§1 (6))

$$\begin{array}{ccc}\mathrm{If}\hfill & A\mathrm{is}\mathrm{predicated}\mathrm{of}\mathrm{all}B\hfill & \mathrm{premise}\hfill \\ \mathrm{and}\hfill & B\mathrm{is}\mathrm{predicated}\mathrm{of}\mathrm{all}C,\hfill & \mathrm{premise}\hfill \\ \mathrm{then}\hfill & A\mathrm{is}\mathrm{predicated}\mathrm{of}\mathrm{all}C.\hfill & \mathrm{conclusion}\hfill \end{array}$$

Nowadays, we would write such a rule as

$$\frac{A\mathrm{is}\mathrm{predicated}\mathrm{of}\mathrm{all}B,B\mathrm{is}\mathrm{predicated}\mathrm{of}\mathrm{all}C}{A\mathrm{is}\mathrm{predicated}\mathrm{of}\mathrm{all}C}.$$

In this paper, we consider only propositional logics. Thus, the premises and conclusions are propositions (propositional formulas). But even in this case, one may consider different forms of modus ponens [2]:

$$A,A\to B/B\mathrm{or}A,A\mathrm{entails}B/B.$$

As we see, the former rule is about conditional, while the latter rule is about entailment. Clearly, the second form of modus ponens is a rule of meta-logic rather than a rule of logic. In this paper we confine ourselves to rules of the first form: a finitary structural inference rule or a modus rule is given by an ordered pair $(\mathrm{\Gamma },A)$, where $\mathrm{\Gamma }$ is a finite (maybe empty) set of formulas and A is a formula, and we use $\mathrm{\Gamma }/A$ or $\frac{\mathrm{\Gamma }}{A}$ to denote such a pair. Any pair $\mathrm{\Gamma }/A$ constitutes the modus rule that allows for any substitution $\sigma$, to infer $\sigma \left(A\right)$ from $\sigma \left(\mathrm{\Gamma }\right)$.

Let us note that curiously enough, the rule of substitution “for any substitution, $\sigma$, from A infer $\sigma \left(A\right)$” is not structural: it allows to infer formula q from formula p, where p and q are propositional variables, but the structural rule $p/q$ would allow to infer any formula from any formula.

By logic $\mathsf{L}$ we understand a (finitary structural) consequence relation ${⊢}_{\mathsf{L}}$ defined in the following way; for all sets of formulas $\mathrm{\Gamma },\mathsf{\Delta }$, and every formula A

$$\begin{array}{ccc}\left(R\right):\hfill & \mathrm{if}A\in \mathrm{\Gamma },\mathrm{then}\mathrm{\Gamma }{⊢}_{\mathsf{L}}A\hfill & \mathrm{reflexivity}\hfill \\ \left(M\right):\hfill & \mathrm{if}\mathrm{\Gamma }\subseteq \mathsf{\Delta }\mathrm{and}\mathrm{\Gamma }{⊢}_{\mathsf{L}}A,\mathrm{then}\mathsf{\Delta }{⊢}_{\mathsf{L}}A\hfill & \mathrm{monotonicity}\hfill \\ \left(T\right):\hfill & \mathrm{if}\mathrm{\Gamma }{⊢}_{\mathsf{L}}B\mathrm{and}\mathrm{\Gamma },B{⊢}_{\mathsf{L}}A,\mathrm{then}\mathrm{\Gamma }{⊢}_{\mathsf{L}}A\hfill & \text{transitivity - cut}\hfill \\ \left(F\right):\hfill & \mathrm{if}\mathrm{\Gamma }{⊢}_{\mathsf{L}}A,\mathrm{then}\mathsf{\Delta }{⊢}_{\mathsf{L}}A\mathrm{for}\mathrm{some}\mathrm{finite}\mathsf{\Delta }\subseteq \mathrm{\Gamma }\hfill & \mathrm{finitarity}\hfill \\ \left(S\right):\hfill & \mathrm{if}\mathrm{\Gamma }{⊢}_{\mathsf{L}}A,\mathrm{then}\sigma \left(\mathrm{\Gamma }\right){⊢}_{\mathsf{L}}\sigma \left(A\right),\mathrm{for}\mathrm{every}\sigma \hfill & \mathrm{structurality}\hfill \end{array}$$

(1)

Given a logic $\mathsf{L}$, we define a set of theorems $Th\left(\mathsf{L}\right)$ of $\mathsf{L}$ to be

$$Th\left(\mathsf{L}\right):=\{A:\varnothing {⊢}_{\mathsf{L}}A\}.$$

It is customary to define a logic $\mathsf{L}$ by a deductive system—a set of rules $\mathsf{R}$ and axioms. Because axioms can be viewed as rules without premises, we assume that a deductive system is a set of rules and a procedure for derivation such that $\mathrm{\Gamma }{⊢}_{\mathsf{L}}A$ if and only if A can be derived from $\mathrm{\Gamma }$ by rules $\mathsf{R}$.

We extend the notion of the deductive system by allowing to use multiple-conclusion rules. This requires to extend the notion of derivation, and we discuss this generalization in Section 3. Let us stress out that we do not consider multiple-conclusion logics in the sense of Shoesmith and Smiley [3], Carnap’s logics of junctives [4], or hyperformulas [5]. Instead, we study regular logics defined by the deductive systems that admit multiple-conclusion rules. For instance, one can use the following rules to define the classical logic [3] (2.3) and further discussions in Chapter 18 of this book):

$$\begin{array}{ccccc}\frac{A,A\to B}{B}& & \frac{B}{A\to B}& & \frac{\varnothing }{A,A\to B}\\ \frac{A\wedge B}{A}& & \frac{A\wedge B}{B}& & \frac{A,B}{A\wedge B}\\ \frac{A}{A\vee B}& & \frac{B}{A\vee B}& & \frac{A\vee B}{A,B}\\ \frac{A,\neg A}{\varnothing }& & \frac{\varnothing }{A,\neg A}& & \end{array}$$

The idea of using multiple-conclusion rules can be traced back at least to Carnap [6]. Much earlier, Peirce introduced the dialogisms, which are essentially the multiple-conclusion rules, but he preferred to replace them with the single-conclusion rules [7]. Gentzen’s sequent also can be viewed as a multiple-conclusion construction. The following quotation from the authors of [3] explains why Carnap, and not Gentzen, perhaps, should be regarded as the one who introduced multiple-conclusion rules: “Its germ can be found in Gerhard Gentzen’s celebrated Untersuchungen über das logische Schliessen (1934) if one is prepared to interpret his calculus of ‘sequents’ as a metatheory for a multiple-conclusion logic, but this is contrary to Gentzen’s own interpretation, and it was Rudolf Carnap who first consciously broached the subject in his book Formalization of logic (1943)” [3] (Section 2.1, the historical note).

Carnap’s motivation for introducing multiple-conclusion rules was as follows: if we want to syntactically characterize a two-valued classical semantics, this syntactical system should be valid (up to matrix isomorphisms) only in the two-element Boolean matrix. Let us consider matrices depicted in Figure 1 (the designated elements are marked by a bullet). It is not hard to see that any rule which is valid in matrix ${\mathbf{B}}_1$, is valid in all matrices ${\mathbf{B}}_n$ for all $n\ge 0$.

Carnap’s solution was to employ the rules of a different kind: a (structural) multiple-conclusion rule (or multiple-alternative rule, or m-rule for short) is an ordered pair $\mathrm{\Gamma }/\mathsf{\Delta }$ of finite sets of formulas. m-rule $\mathrm{\Gamma }/\mathsf{\Delta }$ is valid in a logical matrix $(\mathbf{A},D)$ if for any valuation $\nu$ such that $\nu \left(A\right)\in D$ for all $A\in \mathrm{\Gamma }$, there is $B\in \mathsf{\Delta }$ such that $\nu \left(B\right)\in D$, that is,

$$\nu \left(\mathrm{\Gamma }\right)\subseteq D,\mathrm{entails}\nu \left(\mathsf{\Delta }\right)\cap D\ne \varnothing .$$

(2)

Let us consider the m-rules

$$\mathsf{t}:=p,\neg p/\varnothing \mathrm{and}\mathsf{de}:=p\vee q/p,q.$$

Then, if we consider logical matrices $({\mathbf{2}}^0,\left\{1\right\}),(\mathbf{2},\left\{1\right\}),({\mathbf{2}}^n,\left\{1\right\}),n\ge 2$ from Figure 1, we can see that

$$\begin{array}{ccc}({\mathbf{2}}^0,\left\{1\right\})⊭\mathsf{t}\hfill & & \mathrm{because}1\mathsf{\wedge }\neg 1=0=1,\mathrm{while}\mathrm{there}\mathrm{is}\mathrm{no}\hfill \\ & & \mathrm{conclusion}\mathrm{taking}\mathrm{value}1\hfill \\ (\mathbf{2},\{1\left\}\right)\mid =\mathsf{t}\hfill & \mathrm{and}(\mathbf{2},\{1\left\}\right)\mid =\mathsf{de}\hfill & \mathrm{left}\mathrm{for}\mathrm{the}\mathrm{reader}\mathrm{to}\mathrm{verify}\hfill \\ ({\mathbf{2}}^n,\left\{1\right\})⊭\mathsf{de}\hfill & \mathrm{for}\mathrm{all}n>1\hfill & \mathrm{if}\nu \left(p\right)=\alpha \mathrm{and}\nu \left(q\right)=\beta ,\mathrm{then}\alpha \vee \beta =1,\mathrm{while}\alpha \ne 1\mathrm{and}\beta \ne 1,\hfill \\ & & \mathrm{that}\mathrm{is},\mathrm{the}\mathrm{premise}\mathrm{takes}\mathrm{a}\mathrm{designated}\mathrm{value},\hfill \\ & & \mathrm{although}\mathrm{both}\mathrm{conclusions}\mathrm{take}\mathrm{the}\mathrm{not-designated}\mathrm{values}\mathrm{cf}.\left(2\right).\hfill \end{array}$$

Thus, if we employ m-rules $\mathsf{t}$ and $\mathsf{de}$ as inference rules together with modus ponens and axioms of the Classical Logic $\mathsf{Cl}$, there is only one logical matrix in which all these rules and axioms are valid, namely $(\mathbf{2},\{1\left\}\right)$.

In 1932 Gödel stated without proof (the proof is due to Gentzen) that intuitionistic propositional logic enjoys the disjunction property: for any formulas $A,B$, if formula $A\vee B$ is a theorem, then at least one of the formulas $A,B$ must be a theorem. It is not true for the classical propositional logic: formula $p\vee \neg p$ is a theorem, while neither p, nor $\neg p$ are theorems. Let us point out that even though the classical logic does not enjoy the disjunction property, the rule $\mathsf{de}$ can be used as an inference rule without expanding the set of theorems.

In what follows, rule $\mathsf{de}$ plays a special role. In the setting of natural deduction, ∨-elimination rule is as depicted in Figure 2:

That is, if we can derive $A\vee B$ and we can derive C separately from A and from B, then we can derive C.

In the multiple-conclusion setting (with the use of $\mathsf{de}$) ∨-elimination can be expressed in a more natural way as depicted below in Figure 3:

In this paper, we study how admissibility of $\mathsf{de}$ can be used to construct bases of admissible rules.

Let us recall that a rule $\mathrm{\Gamma }/A$ is called admissible for a given logic $\mathsf{L}$ if for every substitution $\sigma$,

$$\sigma \left(\mathrm{\Gamma }\right)\subseteq Th\left(\mathsf{L}\right)\mathrm{entails}\sigma \left(A\right)\in Th\left(\mathsf{L}\right).$$

It is not hard to see that a rule $\mathsf{r}$ is admissible for logic $\mathsf{L}$ defined by rules $\mathsf{R}$ if and only if rules $\mathsf{R}\cup \left\{\mathsf{r}\right\}$ define a logic ${\mathsf{L}}^{\prime }$ such that $Th\left(\mathsf{L}\right)=Th\left({\mathsf{L}}^{\prime }\right)$.

We can extend the notion of admissibility to m-rules as follows; an m-rule $\mathrm{\Gamma }/\mathsf{\Delta }$ is admissible for a given logic $\mathsf{L}$ if every substitution $\sigma$,

$$\sigma \left(\mathrm{\Gamma }\right)\subseteq Th\left(\mathsf{L}\right)\mathrm{entails}\sigma \left(\mathsf{\Delta }\right)\cap Th\left(\mathsf{L}\right)\ne \varnothing .$$

The topic of the paper is the relations between the m-rules $\mathsf{t}$ and $\mathsf{de}$ and admissibility of rules. We divide m-rules into three categories: if $\mathsf{r}:=\mathrm{\Gamma }/\mathsf{\Delta }$ is an m-rule, then

$$\begin{array}{l}\mathsf{r}\mathrm{is}\mathrm{conclusive}\mathrm{if}\mathsf{\Delta }\mathrm{consists}\mathrm{of}\mathrm{a}\sin \mathrm{gle}\mathrm{formula};\\ \mathsf{r}\mathrm{is}\mathrm{inconclusive}\mathrm{if}\mathsf{\Delta }\mathrm{consists}\mathrm{of}\mathrm{more}\mathrm{then}\mathrm{one}\mathrm{formula};\\ \mathsf{r}\mathrm{is}\mathrm{terminating}\mathrm{if}\mathsf{\Delta }=\varnothing .\end{array}$$

A rule that has a nonempty set of alternatives is called proper. For instance,

$$\begin{array}{cc}\mathsf{mp}=p,p\to q/q\hfill & \mathrm{is}\mathrm{a}\mathrm{conclusive}\mathrm{rule};\hfill \\ \mathsf{de}=p\vee q/p,q\hfill & \mathrm{is}\mathrm{an}\mathrm{inconclusive}\mathrm{rule};\hfill \\ \mathsf{t}=p\wedge \neg p/\varnothing \hfill & \mathrm{is}\mathrm{a}\mathrm{terminating}\mathrm{rule},\hfill \end{array}$$

and $\mathsf{mp}$ and $\mathsf{de}$ are proper m-rules.

Successive application of rules leads to a notion of inference: from a given set of formulas $\mathrm{\Gamma }$—assumptions—we infer a formula, A. Inferences from the empty set of assumptions (or from the axioms) are proofs.

In this paper, we focus on logics for which the ∨-elimination m-rule $\mathsf{de}$ is admissible (for instance, it is admissible for the intuitionistic logic and it is not admissible for the classical logic). Additionally, we will show that all m-rules except, perhaps, for $\mathsf{de}$ and $\mathsf{t}$, can be eliminated from any base of admissible m-rules for such a logic.

2. Preliminaries

Let $\mathsf{Fm}$ be a set of all (propositional) formulas built in a usual way from a denumerable set of (propositional) variables $Var$ and a finite set of connectives $\mathcal{C}$. The maps $\sigma :Var⟶\mathsf{Fm}$ are called substitutions. Given a substitution $\sigma$ and a formula A, $\sigma \left(A\right)$ denotes the result of replacing each variable p occurring in A with formula $\sigma \left(p\right)$, and if $\mathrm{\Gamma }$ is a set of formulas, then $\sigma \left(\mathrm{\Gamma }\right):=\left\{\sigma \right(A):A\in \mathrm{\Gamma }\}$.

Let ${\mathcal{R}}_{\mathsf{Fm}}$ be a class of all ordered pairs of finite (possibly empty) subsets of $\mathsf{Fm}$. The members of ${\mathcal{R}}_{\mathsf{Fm}}$ are called multiple-conclusion rules, or multiple-alternative rules (m-rules for short). In the sequel, $\mathrm{\Gamma }⋐\mathsf{Fm}$ means that $\mathrm{\Gamma }$ is a finite subset of $\mathsf{Fm}$, and if $\mathrm{\Gamma },\mathsf{\Delta }⋐\mathsf{Fm}$, the rule $(\mathrm{\Gamma },\mathsf{\Delta })$ is denoted as $\mathrm{\Gamma }/\mathsf{\Delta }$. The members of $\mathrm{\Gamma }$ are called premises, while the members of $\mathsf{\Delta }$ are called alternatives or conclusions. If $\{A_0,\cdots ,A_{n-1}\}/\{B_0,\cdots ,B_{m-1}\}$ is an m-rule, we drop curly brackets and write $A_0,\cdots ,A_{n-1}/B_0,\cdots ,B_{m-1}$. Also, if $\mathrm{\Gamma },{\mathrm{\Gamma }}^{\prime }⋐\mathsf{Fm}$, we write $\mathrm{\Gamma },{\mathrm{\Gamma }}^{\prime }$ to denote $\mathrm{\Gamma }\cup {\mathrm{\Gamma }}^{\prime }$.

If $\mathsf{r}:=\mathrm{\Gamma }/\mathsf{\Delta }$ is an m-rule and $\sigma$ is a substitution, then $\sigma \left(\mathrm{\Gamma }\right)/\sigma \left(\mathsf{\Delta }\right)$ is again an m-rule which is called an instance of $\mathsf{r}$.

Let us note that m-rules allow empty sets of premises and alternatives/conclusions, and ∅ has a different meaning depending on whether it is a set of premises or a set of conclusions. To make it easier, we use ▼ for ∅ as a premise and we use ▲ for ∅ as a conclusion. We also assume that for every substitution $\sigma$, $\sigma (▼)=▼$ and $\sigma (▲)=▲$. Symbols ▼ are ▲ are merely notations and they are not elements of the language or metalanguage.

Formula A is valid in a given logic $\mathsf{L}$ ($\mathsf{L}$-valid for short) or A is a theorem of $\mathsf{L}$ if ${⊢}_{\mathsf{L}}A$ (or $A\in Th\left(\mathsf{L}\right)$), otherwise, A is called refuted in $\mathsf{L}$.

We call logic $\mathsf{L}$ consistent if not every formula from $\mathsf{Fm}$ is a theorem of $\mathsf{L}$. Let us note that because of structurality, i.e., because ${⊢}_{\mathsf{L}}$ obeys (S) from (1), a logic $\mathsf{L}$ is consistent if and only if ${⊬}_{\mathsf{L}}q$, where q is a variable.

Let us observe that a rule $\mathsf{r}:=\mathrm{\Gamma }/A$ is admissible for logic $\mathsf{L}$ (in symbols, $\mathrm{\Gamma }\mid {\sim }_{\mathsf{L}}A$) if any substitution that refutes A, refutes at least one member of $\mathrm{\Gamma }$. If $\mathrm{\Gamma }=\varnothing$, then rule $\mathrm{\Gamma }/A$ is admissible for $\mathsf{L}$ if and only if $A\in Th\left(\mathsf{L}\right)$ [8]. For m-rules, an m-rule $\mathrm{\Gamma }/\mathsf{\Delta }$ is admissible for ${⊢}_{\mathsf{L}}$ (in symbols $\mathrm{\Gamma }\mid {\sim }_{\mathsf{L}}\mathsf{\Delta }$) if every substitution $\sigma$ that refutes all formulas from $\mathsf{\Delta }$, refutes at least one formula from $\mathrm{\Gamma }$ [8]. Thus, the rule ▼/▲ is not admissible in any logic.

If $\mathsf{R}$ is a set of all conclusive rules admissible for logic $\mathsf{L}$, then $\mathsf{R}$ defines a logic $\tilde{\mathsf{L}}$ that has the same set of theorems as $\mathsf{L}$. It is not hard to see that $\tilde{\mathsf{L}}$ is the biggest logic that has the same theorems as $\mathsf{L}$, and we call $\tilde{\mathsf{L}}$ an admissible completion of $\mathsf{L}$. In the book by Rybakov [9] (Definition 1.7.3), the term “admissible closure” is used; in our view, the latter term is a bit ambiguous, because “admissible closure” can refer to a consequence closure operator. Let us note that if $\mathsf{R}$ is a set of all conclusive rules admissible for $\mathsf{L}$ and ${\mathsf{R}}^m$ is a set of all m-rules admissible for $\mathsf{L}$, then ${⊢}_{\mathsf{R}}$ and ${⊢}_{{\mathsf{R}}^m}$ define the same logic, namely, $\tilde{\mathsf{L}}$. Indeed, it is clear that a conclusive rule $\mathsf{r}$ is admissible for $\mathsf{L}$ if and only if $\mathsf{r}$ is admissible for $\mathsf{L}$ as m-rule.

If $\mathsf{L}$ is a logic defined by m-rules and $\mathsf{r}$ is a rule, by $\mathsf{L}+\mathsf{r}$ we denote the smallest logic extending $\mathsf{L}$ and containing $\mathsf{r}$. It is not hard to see that if $\mathsf{r}$ is admissible for $\mathsf{L}$, then $Th(\mathsf{L}+\mathsf{r})=Th\left(\mathsf{L}\right)$.

Admissibility of a rule can be expressed in terms of $\mathsf{L}$-unifiability. A set of formulas $\mathrm{\Gamma }$ is unifiable in $\mathsf{L}$ (or $\mathsf{L}$-unifiable) if ▲, otherwise $\mathrm{\Gamma }$ is nonunifiable in $\mathsf{L}$. In other words, formulas $\mathrm{\Gamma }$ are $\mathsf{L}$-unifiable if and only if there is such a substitution $\sigma$, that $\sigma \left(\mathrm{\Gamma }\right)\subseteq Th\left(\mathsf{L}\right)$, and in this case, $\sigma$ is said to be an $\mathsf{L}$-unifier of $\mathrm{\Gamma }$. Thus, an m-rule $\mathrm{\Gamma }/\mathsf{\Delta }$ is admissible for $\mathsf{L}$ if and only if every $\mathsf{L}$-unifier of $\mathrm{\Gamma }$ unifies at least one formula from $\mathsf{\Delta }$.

Logic $\mathsf{L}$ is strongly consistent if there is a finite set of formulas $\mathrm{\Gamma }$ such that $\mathrm{\Gamma }\mid {\sim }_{\mathsf{L}}▲$, that is, $\mathrm{\Gamma }$ is nonunifiable in $\mathsf{L}$. Note that if $\mathrm{\Gamma }$ is a nonunifiable in $\mathsf{L}$ finite set of formulas, then any rule $\mathrm{\Gamma }/\mathsf{\Delta }$ (including $\mathrm{\Gamma }/▲$) is trivially admissible in $\mathsf{L}$. The m-rules with nonunifiable set of premises are called passive (passive rules were introduced in [10]).

Example 1.

Throughout the paper we will use the examples from the following well-known logics.

$$\begin{array}{cc}\mathsf{Int}\hfill & \mathit{intuitionistic}\mathit{propositional}\mathit{logic};\hfill \\ \mathsf{Pos}\hfill & \mathit{positive}\mathit{fragment}\mathit{of}\mathsf{Int};\hfill \\ \mathsf{KP}\hfill & \mathit{Kreisel-Putnam}’s\mathit{logic};\hfill \\ \mathsf{ML}\hfill & \mathit{Medvedev}’s\mathit{logic};\hfill \\ \mathsf{Jhn}\hfill & \mathit{Johansson}’s(\mathit{or}\mathit{minimal})\mathit{logic};\hfill \end{array}$$

and normal modal logics $\mathsf{S}4,\mathsf{D}4,\mathsf{GL},\mathsf{K}4,\mathsf{K}4.1,\mathsf{S}4,\mathsf{S}4.1,\mathsf{Grz},\mathsf{Int},\mathsf{Dn}$ [11]. All these logics are consistent: formula p, where p is a propositional variable, is not a theorem. And all of them, except for $\mathsf{Pos}$, are strongly consistent: formula $p\wedge \neg p$ is not unifiable, while in $\mathsf{Pos}$ every nonempty set of formulas is unifiable (substitute each variable with $p\to p$).

3. Derivation

An m-inference (or m-derivation) of an m-rule from a given set of m-rules will be a generalization of a regular notion of Hilbert style inference (for instance, like in [12]). Since we allow to use the multiple-conclusion rules, inference cannot be a sequence anymore, and it is a tree: application of any inconclusive rule triggers branching. Each derived alternative shall be considered individually, like a separate case in a proof by cases. The introduced below notion of m-inference with use of m-rules reflects our everyday practice of making derivations from a set of assumptions: at each step we either refer to an assumption, or we apply a rule of inference and derive an (intermediate) conclusion, or we use a proof by cases and we lay down a set of alternatives that will be considered separately. The latter is captured by application of some inconclusive rule, when instead of a single conclusion we arrive at a set of alternatives to be considered (for different flavors of formalization of the proofs by cases can be fond in [13]). Our definition of m-inference slightly differs from the definition in [8,14]. An alternative approach to derivation in the multiple conclusion setting the reader can find in [15].

3.1. Basic Definitions: Derivation Trees

By (finite) tree we understand a partially ordered set $(\mathsf{Nd},\le )$ that has the biggest element (called a root) and for each $\mathfrak{n}\in \mathsf{Nd}$, the segment $\{{\mathfrak{n}}^{\prime }\in \mathsf{Nd}:\mathfrak{n}\le {\mathfrak{n}}^{\prime }\}$ is a chain. Labeling of a tree $(\mathsf{Nd},\le )$ is a map $\lambda :\mathsf{Nd}⟶\{A:A\in \mathsf{Fm}\cup \{▼,▲\left\}\right\}$, where ▼ is allowed only in the root and ▲ is allowed only in a leaf. Moreover, the root is always labeled by ▼. A tree together with labeling (that is the pair tree-labeling) is called a labeled tree. When we draw a labeled tree, to simplify notation, instead of node $\mathfrak{n}$ we will use its label $\lambda \left(\mathfrak{n}\right)$. For instance, instead of left-hand side tree depicted in Figure 4 with labeling $\lambda$

$$\begin{array}{cccccc}\mathrm{node}\hfill & {\mathfrak{n}}_0\hfill & {\mathfrak{n}}_1\hfill & {\mathfrak{n}}_2\hfill & {\mathfrak{n}}_3\hfill & {\mathfrak{n}}_4\hfill \\ \lambda \hfill & A\hfill & B\hfill & C\hfill & A\hfill & ▲\hfill \end{array}$$

we use the right-hand side tree

If $\mathfrak{n}$ is a node of a labeled tree, we let $\mathfrak{n}\uparrow :=\{{\mathfrak{n}}^{\prime }\in \mathsf{Nd}:\mathfrak{n}\le {\mathfrak{n}}^{\prime }\}$ and $\mathfrak{n}\downarrow :=\{n^{\prime }\in \mathsf{Nd}:{\mathfrak{n}}^{\prime }\le \mathfrak{n}\}$. Nodes from $\mathfrak{n}\uparrow$ are predecessors of $\mathfrak{n}$ and nodes from $\mathfrak{n}\downarrow$ are successors of $\mathfrak{n}$. A successor ${\mathfrak{n}}^{\prime }$ of a node $\mathfrak{n}$ is called immediate if there are no nodes strongly between ${\mathfrak{n}}^{\prime }$ and $\mathfrak{n}$;. By $lv\left(\mathsf{Nd}\right)$ we denote the set of all leaves of $\mathsf{Nd}$, that is, $lv\left(\mathsf{Nd}\right)$ is the set of all minimal elements of $(\mathsf{Nd},\le )$.

If ${\mathsf{Nd}}^{\prime }\subseteq \mathsf{Nd}$, then $\lambda \left({\mathsf{Nd}}^{\prime }\right):=\bigcup \{\lambda \left(\mathfrak{n}\right):\mathfrak{n}\in {\mathsf{Nd}}^{\prime }\}$. For instance, $\lambda \left(\mathfrak{n}\uparrow \right)$ is a set of all formulas labeling all predecessors of $\mathfrak{n}$, and $\lambda \left(lv\right(\mathsf{Nd}\left)\right)$ is a set of all formulas labeling all leaves of the tree $(\mathsf{Nd},\le )$.

A leaf labeled by ▲ is a terminal leaf, otherwise, the leaf is called extendable.

3.2. Definition of m-Inference

Now, we can introduce the notion of m-inference in the setting of m-rules. Our definition of m-inference is slightly different from the one introduced in works by the authors of [3,14], but as Theorem 2 shows, the classes of derivable m-rules coincide.

Definition 1.

Let $\mathsf{R}$ be a set of m-rules and $\mathrm{\Gamma }$ be a set of formulas (which may be empty). An m-inference from $\mathrm{\Gamma }$ by $\mathsf{R}$ (or $(\mathrm{\Gamma },\mathsf{R})$-inference for short) is a finite labeled tree, defined by induction:

(a) 

A tree containing only a root labeled by ▼ is a $(\mathrm{\Gamma },\mathsf{R})$-inference;

(b) 

If I is a $(\mathrm{\Gamma },\mathsf{R})$-inference, then a tree obtained from I by adjoining to an extendable leaf an immediate successor labeled by a formula from $\mathrm{\Gamma }$ is a $(\mathrm{\Gamma },\mathsf{R})$-inference;

(c) 

If I is a $(\mathrm{\Gamma },\mathsf{R})$-inference, and $\mathfrak{n}$ is an extendable leaf, then a tree, obtained from I by adjoining to $\mathfrak{n}$ immediate successors ${\mathfrak{n}}_0,\cdots ,{\mathfrak{n}}_{m-1}$ labeled by formulas $B_0,\cdots ,B_{m-1}$, is $(\mathrm{\Gamma },\mathsf{R})$-inference, provided there is an instance $\mathsf{\Delta }/\mathrm{\Pi }$ of a rule from $\mathsf{R}$ such that

$$\mathsf{\Delta }\subseteq \lambda \left(\mathfrak{n}\uparrow \right)\mathit{and}\mathrm{\Pi }=\{B_0,\cdots ,B_{m-1}\}.$$

(d) 

If I is a $(\mathrm{\Gamma },\mathsf{R})$-inference and $\mathfrak{n}$ is an expendable leaf, then a tree, obtained from I by adjoining to $\mathfrak{n}$ immediate successors ${\mathfrak{n}}_0$ labeled by ▲, is $(\mathrm{\Gamma },\mathsf{R})$-inference, provided there is an instance $\mathsf{\Delta }/▲$ of a rule from $\mathsf{R}$ such that

$$\mathsf{\Delta }\subseteq \lambda \left(\mathfrak{n}\uparrow \right).$$

For instance, suppose $\mathrm{\Gamma }=\{C_0,\cdots ,C_{k-1}\}$ and $A_0,\cdots ,A_{n-1}/B_0,\cdots ,B_{m-1}$ is an instance of a rule from $\mathsf{R}$. Then, if a tree depicted in Figure 5 is a $(\mathrm{\Gamma },\mathsf{R})$-inference, then the trees depicted in Figure 6 are $(\mathrm{\Gamma },\mathsf{R})$-inferences, provided for (a) that $0\le j<k$, and for (b), that all premises $A_i,i<n$ can be found on the branch between leaf $D_0$ and the root.

Let us observe the following simple but important property of m-inferences.

Proposition 1.

Suppose that I and $I^{\prime }$ are $(\mathrm{\Gamma },\mathsf{R})$-inferences. Then the following assertions hold:

(a) 

a labeled tree obtained from I by omitting all successors of a given node is a $(\mathrm{\Gamma },\mathsf{R})$-inference;

(b) 

if we remove the root of $I^{\prime }$ and adjoin the remainder of $I^{\prime }$ to a leaf of I, the obtained labeled tree is a $(\mathrm{\Gamma },\mathsf{R})$-inference;

(c) 

for any substitution σ, the tree $\sigma \left(I\right)$ obtained from I by replacing in every node the labeling formula A by $\sigma \left(A\right)$, is a $\sigma \left(\mathrm{\Gamma }\right),\mathsf{R}$-inference.

The proof follows immediately from the definition of m-inference.

3.3. Derivations of m-Rules

Using the notion of m-inference from assumptions, we can define the notion of m-inference of m-rule.

Definition 2.

Let $\mathsf{R}$ be a set of m-rules and $\mathsf{r}:=\mathrm{\Gamma }/\mathsf{\Delta }$ be an m-rule. We say that $\mathsf{r}$ is derivable from rules $\mathsf{R}$ (in symbols $\mathsf{R}⊢\mathsf{r}$) if there is a $(\mathrm{\Gamma },\mathsf{R})$-inference I such that $\lambda \left(lv\right(I\left)\right)\subseteq \mathsf{\Delta }\cup \{▲\}$, i.e., every leaf is labeled by a formula from $\mathsf{\Delta }$ or by$▲$.

The following proposition is an immediate consequence of the definition.

Proposition 2.

Let $\mathrm{\Gamma }$ be a finite set of formulas and $\mathsf{R}$ be a set of m-rules. Then any $(\mathrm{\Gamma },\mathsf{R})$-inference I is a derivation of m-rule $\mathrm{\Gamma }/\mathsf{\Delta }$ where $\mathsf{\Delta }=\lambda \left(lv\right(I\left)\right)$, i.e., $\mathsf{\Delta }$ is a set of all formulas labeling all leaves of I.

Corollary 1.

Suppose that I is an m-inference of an m-rule $\mathrm{\Gamma }/\mathsf{\Delta }$ from a set of m-rules $\mathsf{R}$. Then if a formula $A\in \mathsf{\Delta }$ labels a node n that is not a leaf, the tree $I^{\prime }$ obtained from I by omitting all nodes strongly below $\mathfrak{n}$, is also an m-inference of $\mathrm{\Gamma }/\mathsf{\Delta }$ from $\mathsf{R}$.

In other words, if $\mathsf{R}⊢\mathrm{\Gamma }/\mathsf{\Delta }$, then there is a $(\mathrm{\Gamma },\mathsf{R})$-inference, such that formulas from $\mathsf{\Delta }$ label only leaves.

Theorem 1.

Suppose that $\mathsf{R}$ and ${\mathsf{R}}^{\prime }$ are sets of m-rules, while $\mathsf{r}$ and ${\mathsf{r}}^{\prime }$ are m-rules. Then the following hold;

(i) 

if $\mathsf{r}\in \mathsf{R}$, then $\mathsf{R}⊢\mathsf{r}$;

(ii) 

if $\mathsf{R}⊢\mathsf{r}$, then $\mathsf{R}\cup {\mathsf{R}}^{\prime }⊢\mathsf{r}$;

(iii) 

if $\mathsf{R}⊢\mathsf{r}$ and ${\mathsf{R}}^{\prime },\mathsf{r}⊢{\mathsf{r}}^{\prime }$, then $\mathsf{R},{\mathsf{R}}^{\prime }⊢{\mathsf{r}}^{\prime }$.

Proof. 

The proofs of (i) and (ii) are straightforward. Let us prove (iii).

Suppose that $\mathsf{r}=\mathrm{\Gamma }/\mathsf{\Delta },{\mathsf{r}}^{\prime }={\mathrm{\Gamma }}^{\prime }/{\mathsf{\Delta }}^{\prime }$ and $\mathsf{\Delta }=\{D_0,\cdots ,D_{m-1}\}$. By assumption, there is a $(\mathrm{\Gamma },\mathsf{R})$-inference of $\mathsf{\Delta }$, which we denote by I, and there is a $({\mathrm{\Gamma }}^{\prime },{\mathsf{R}}^{\prime },\mathsf{r})$-inference of ${\mathsf{\Delta }}^{\prime }$, which we denote by $I^{\prime }$. To prove (iii) it suffices to observe that any application of rule $\mathsf{r}$ in $I^{\prime }$ can be replaced by an instance of the proof I (see Figure 7).

Let us observe that the set of leaves of the proof depicted in Figure 7c is a subset of the set of leaves of the proof depicted in Figure 7b. Thus, all the leaves of the proof depicted in Figure 7c contain formulas only from ${\mathsf{\Delta }}^{\prime }$. □

Properties of m-Inference

Theorem 2.

Let $\mathsf{R}$ be a set of m-rules, $\mathrm{\Gamma }/\mathsf{\Delta }$ be an m-rule and A be a formula. Then

$$\begin{array}{cc}\mathsf{R}⊢A/A;\hfill & \hfill \left(R\right)\\ \mathsf{R}⊢\mathrm{\Gamma }/\mathsf{\Delta }entails\mathsf{R}⊢{\mathrm{\Gamma }}^{\prime }/{\mathsf{\Delta }}^{\prime }forany{\mathrm{\Gamma }}^{\prime }\supseteq \mathrm{\Gamma }and{\mathsf{\Delta }}^{\prime }\supset \mathsf{\Delta };\hfill & \hfill \left(M\right)\\ if\mathsf{R}⊢\mathrm{\Gamma }/\mathsf{\Delta },A\mathit{and}\mathsf{R}⊢\mathrm{\Gamma },A/\mathsf{\Delta },\mathit{then}\mathsf{R}⊢\mathrm{\Gamma }/\mathsf{\Delta };\hfill & \hfill \left(T\right)\\ if\mathsf{R}⊢\mathrm{\Gamma }/\mathsf{\Delta },A,\mathit{then}\mathsf{R}⊢\sigma \left(\mathrm{\Gamma }\right)/\sigma \left(\mathsf{\Delta }\right)\mathit{for}\mathit{any}\mathit{substitution}\sigma \hfill & \hfill \left(S\right).\end{array}$$

Proof. 

Indeed, if A is a formula, then the tree that consists of a root, labeled by ▼, and its single immediate successor, labeled by A, is an m-inference of the rule $A/A$ from $\mathsf{R}$. Thus, (R) holds.

It follows immediately from the definition of inference that if I is an inference of a rule $\mathrm{\Gamma }/\mathsf{\Delta }$ from $\mathsf{R}$, then I is at the same time an inference of the rule $\mathrm{\Gamma }\cup {\mathrm{\Gamma }}^{\prime }/\mathsf{\Delta }\cup {\mathsf{\Delta }}^{\prime }$ for any finite sets of formulas ${\mathrm{\Gamma }}^{\prime },{\mathsf{\Delta }}^{\prime }$. That is, (M) holds.

Also straight from the definition it follows that if I is an inference of a rule $\mathrm{\Gamma }/\mathsf{\Delta }$ from $\mathsf{R}$ and $\sigma$ is a substitution, then the tree $\sigma \left(I\right)$, obtained from I by replacing every label A with $\sigma \left(A\right)$, is an inference of $\sigma \left(\mathrm{\Gamma }\right)/\sigma \left(\mathsf{\Delta }\right)$ from $\mathsf{R}$. Thus, (S) holds.

To demonstrate (T) we will show that, given an m-inferences of rules $\mathrm{\Gamma },A/\mathsf{\Delta }$ and $\mathrm{\Gamma }/A,\mathsf{\Delta }$ from $\mathsf{R}$, we can construct an m-inference of the rule $\mathrm{\Gamma }/\mathsf{\Delta }$.

Suppose $\mathsf{\Delta }=\{D_0,\cdots ,D_{m-1}\}$ and we have inferences of $\mathrm{\Gamma },A/\mathsf{\Delta }$ and $\mathrm{\Gamma }/A,\mathsf{\Delta }$ from $\mathsf{R}$ depicted respectively in Figure 8a,b:

By Corollary 1, we can assume that A labels only leaves. Then we can construct an inference of $\mathsf{\Delta }$ from $\mathrm{\Gamma }$ by adjoining inference (b) to every leaf labeled by A as depicted below in Figure 9:

and in such a way to obtain an m-inference of $\mathrm{\Gamma }/\mathsf{\Delta }$. □

Let us also note the following property of passive rules which immediately follows from (M).

Corollary 2.

Let $\mathsf{R}$ be a set of m-rules containing rule $\mathrm{\Gamma }/▲$. Then, for any finite set of formulas $\mathsf{\Delta }$,

$$\mathsf{R}⊢\mathrm{\Gamma }/\mathsf{\Delta }.$$

Corollary 3.

If $\mathsf{R}$ is a set of m-rules admissible for logic $\mathsf{L}$ and $\mathsf{r}$ is an m-rule such that $\mathsf{R}⊢\mathsf{r}$, then $\mathsf{r}$ is also admissible for $\mathsf{L}$.

Proof. 

Suppose that $\mathsf{r}=\mathrm{\Gamma }/\mathsf{\Delta }$ and $\sigma$ is a substitution such that $\sigma \left(\mathrm{\Gamma }\right)\in Th\left(\mathsf{L}\right)$. By virtue of (S), there is an m-inference of $\sigma \left(\mathrm{\Gamma }\right)/\sigma \left(\mathsf{\Delta }\right)$ from $\mathsf{R}$. From the definition of m-inference and admissibility of rules from $\mathsf{R}$, any application of rule from $\mathsf{R}$ has at least one conclusion, which is a theorem of $\mathsf{L}$. Hence, $\sigma \left(\mathsf{\Delta }\right)$ contains a theorem of $\mathsf{L}$, and hence rule $\mathrm{\Gamma }/\mathsf{\Delta }$ is admissible for $\mathsf{L}$. Let us note that if some rule from $\mathsf{R}$ is terminating, its admissibility entails that $\mathsf{L}$ is not consistent and hence, every rule is admissible for it. □

3.4. m-Deductive Systems

Theorem 2 ensures that for any set of m-rules $\mathsf{R}$, the restriction of ${⊢}_{\mathsf{R}}$ to the single-conclusion relation is a consequence relation. Thus, every set of m-rules $\mathsf{R}$ can be regarded as an m-deductive system ${⊢}_{\mathsf{R}}$. Recall that $Th\left(\mathsf{R}\right)$ is the set of theorems: $Th\left(\mathsf{R}\right)=\{A\in \mathsf{Fm}:{⊢}_{\mathsf{R}}A\}$.

Let us point out that m-deductive systems lack some properties of regular deductive systems. For instance, a join of m-deductive systems with the same sets of theorems may be an m-deductive system with a strongly larger set of theorems. That is,

$$Th\left({\mathsf{R}}_0\right)=Th\left({\mathsf{R}}_1\right)\nRightarrow Th\left({\mathsf{R}}_0\right)=Th\left({\mathsf{R}}_1\right)=Th({\mathsf{R}}_0\cup {\mathsf{R}}_1).$$

We assume that the reader is familiar with Heyting algebras as models of intermediate logics.

Let us consider deductive system $\mathsf{R}$ defined by all formulas valid in algebra $\mathbf{C}$ depicted in Figure 10 and the rule $\mathsf{mp}$ (we regard formulas as rules of type $▼/A$); we constructed two m-deductive systems:

$$\begin{array}{c}{\mathsf{R}}_0:=\mathsf{R}+\mathsf{de}+\mathsf{dil}\mathrm{and}{\mathsf{R}}_1:=\mathsf{R}+\mathsf{r}+\mathsf{dir},\mathrm{where}\\ \mathsf{r}:=(\neg \neg p\to p)\to (p\vee \neg p)/\neg p\vee \neg \neg p,\mathsf{dil}:=p/q\vee p\mathrm{and}\mathsf{dir}:=p/p\vee q.\end{array}$$

Our goal is to verify that $Th\left(\left(\mathsf{R}\right)\right)=Th\left(\left({\mathsf{R}}_0\right)\right)=Th\left(\left({\mathsf{R}}_1\right)\right)$ and formula $A:=(\neg p\vee \neg \neg p)\vee (\neg \neg p\to p)$ is not a theorem of ${\mathsf{R}}_0$ and ${\mathsf{R}}_1$, while A is a theorem of ${\mathsf{R}}_0\cup {\mathsf{R}}_1$, that is, $Th\left({\mathsf{R}}_0\right)=Th\left({\mathsf{R}}_1\right)⊈Th({\mathsf{R}}_0\cup {\mathsf{R}}_1)$.

We start with an observation that algebra ${\mathbf{C}}^{\prime }$ (see Figure 10) is (isomorphic to) a Lindenbaum algebra of $\mathsf{R}$ on one variable. Hence, both algebras $\mathbf{C}$ and ${\mathbf{C}}^{\prime }$ are models for $\mathsf{R}$.

Next, we observe (and we left for the reader to perform this routine check) that (a) rules $\mathsf{de}$ and $\mathsf{dil}$ are valid in $\mathbf{C}$, hence, $\mathbf{C}$ is a model of ${\mathsf{R}}_0$; (b) rules $\mathsf{r}$ and $\mathsf{dir}$ are valid in ${\mathbf{C}}^{\prime }$, hence, ${\mathbf{C}}^{\prime }$ is a model of ${\mathsf{R}}_1$; and (c) all three m-logics have the same sets of theorems, that is,

$$Th\left(\mathsf{L}\right)=Th\left({\mathsf{L}}_0\right)=Th\left({\mathsf{L}}_1\right).$$

Also, as we can see in Figure 10, formula A is refuted in $\mathbf{C}$ and hence, $A\notin Th\left({\mathsf{R}}_0\right)$ and $A\notin Th\left({\mathsf{R}}_1\right)$. Thus, we only need to show that $A\in Th({\mathsf{R}}_0\cup {\mathsf{R}}_1)$.

Indeed, because algebra ${\mathbf{C}}^{\prime }$ is a Lindebaum algebra of $\mathsf{R}$ on one variable and any formula in one variable is a theorem of $\mathsf{R}$ precisely when it is valid on the generator of ${\mathbf{C}}^{\prime }$ depicted as ∘. Thus, because formula $\left(\right(\neg \neg p\to p)\to (p\vee \neg p\left)\right)\vee (\neg \neg p\to p)$ is valid on this generator, it is a theorem of $\mathsf{R}$, as well as it is a theorem of ${\mathsf{R}}_0$ and ${\mathsf{R}}_1$. Thus, we can construct an m-inference of A from $\left(\right(\neg \neg p\to p)\to (p\vee \neg p\left)\right)\vee (\neg \neg p\to p)$, which is presented in Figure 11.

Thus, formula A is a theorem of ${\mathsf{L}}^{\prime }$.

3.5. Admissible Bases

Suppose that $\mathsf{L}$ is a logic, $\mathsf{R}$ is a set of m-rules and $\mathsf{r}$ is an m-rule. We say that $\mathsf{r}$ is derivable from m-rules $\mathsf{R}$ relative to m-logic $\mathsf{L}$ (in symbols $\mathsf{R}{⊢}_{\mathsf{L}}\mathsf{r}$) if $\mathsf{R}\cup \mathsf{L}⊢\mathsf{r}$.

Let us observe that, by Corollary 3, if $\mathsf{R}$ is a set of admissible for $\mathsf{L}$ m-rules and $\mathsf{R}⊢{}_{\mathsf{L}}\mathsf{r}$, then $\mathsf{r}$ is admissible for $\mathsf{L}$ m-rule. Thus, we can use m-inferences to axiomatize admissible completion of logics.

Definition 3.

Suppose $\mathsf{L}$ is a logic and $\mathsf{R}$ is a set of admissible for $\mathsf{L}$ conclusive rules. Then $\mathsf{R}$ is an admissible relative to $\mathsf{L}$ base if every admissible for $\mathsf{L}$ conclusive rule $\mathsf{r}$ is derivable from $\mathsf{R}$ relative to $\mathsf{L}$, that is,

$$\mathsf{R}⊢{}_{\mathsf{L}}\mathsf{r}\mathit{for}\mathit{every}\mathit{conclusive}\mathit{admissible}\mathit{for}\mathsf{L}\mathit{rule}\mathsf{r}.$$

Example 2.

For $\mathsf{Int}$ the Visser rules

$${\mathsf{v}}_n:=\frac{A^{\left(n\right)}\to (p_n\vee q_n)}{{\bigvee }_{i=0}^n(A^{\left(n\right)}\to p_i)},$$

where $A^{\left(n\right)}:={\bigwedge }_{i=0}^{n-1}(p_i\to q_i),n\ge 1$, form a relative admissible base (cf. the work by the authors of [16]).

In a natural way, the notion of admissible base can be extended to m-rules.

Definition 4.

Suppose $\mathsf{L}$ is a logic and $\mathsf{R}$ is a set of admissible for $\mathsf{L}$ m-rules. Then $\mathsf{R}$ is an admissible relative to $\mathsf{L}$ m-base if every admissible for $\mathsf{L}$ m-rule $\mathsf{r}$ is derivable from $\mathsf{R}$ relative to $\mathsf{L}$, that is,

$$\mathsf{R}⊢{}_{\mathsf{L}}\mathsf{r}\mathit{for}\mathit{every}\mathit{admissible}\mathit{for}\mathsf{L}\mathit{m-rule}\mathsf{r}.$$

And an admissible m-base $\mathsf{R}$ for $\mathsf{L}$ is independent if neither proper subset of $\mathsf{R}$ is an admissible m-base for $\mathsf{L}$.

Definition 5.

Suppose $\mathsf{L}$ is a logic and $\mathsf{R}$ is a set of admissible for $\mathsf{L}$ m-rules. Then $\mathsf{R}$ is an admissible relative to $\mathsf{L}$ extended base if every admissible for $\mathsf{L}$ conclusive rule $\mathsf{r}$ is derivable from $\mathsf{R}$ relative to $\mathsf{L}$, that is,

$$\mathsf{R}⊢{}_{\mathsf{L}}\mathsf{r}\mathrm{for}\mathrm{every}\mathrm{admissible}\mathrm{for}\mathsf{L}\mathrm{m}-\mathrm{rule}\mathsf{r}.$$

And an admissible extended base $\mathsf{R}$ for $\mathsf{L}$ is independent if neither proper subset of $\mathsf{R}$ is an admissible m-base for $\mathsf{L}$.

In Section 5 and Section 6 we see that in the logics with the disjunction property, the admissible bases and m-bases are closely related.

Remark 1.

There is a difference in the properties of admissible conclusive and inconclusive rules. Namely, in contrast to conclusive rules, an inconclusive rule can be derivable and not admissible. Indeed, if $\mathsf{Cl}$ is the logic defined by axiom schemes of the classical logic and $\mathsf{mp}$ as a single inference rule and ${\mathsf{Cl}}^{\mathsf{v}}:=\mathsf{Cl}+\mathsf{de}$, then, $Th\left(\mathsf{Cl}\right)=Th\left({\mathsf{Cl}}^{\mathsf{v}}\right)$: it is clear that $Th\left(\mathsf{Cl}\right)\subseteq Th\left({\mathsf{Cl}}^{\mathsf{v}}\right)$, on the other hand, every theorem of ${\mathsf{Cl}}^{\mathsf{v}}$ is valid in the two-element Boolean algebra, because all axioms and rules of ${\mathsf{Cl}}^{\mathsf{v}}$ are valid in it. Thus, rule $\mathsf{de}$ is trivially derivable in ${\mathsf{Cl}}^{\mathsf{v}}$ but it is not admissible: ${⊢}_{{\mathsf{Cl}}^{\mathsf{v}}}p\vee \neg p$, while ${⊬}_{{\mathsf{Cl}}^{\mathsf{v}}}p$ and ${⊬}_{{\mathsf{Cl}}^{\mathsf{v}}}\neg p$.

4. Introducing Meta-Disjunction

If our language contains disjunction with regular properties, m-Rule

$$\mathsf{de}:=\frac{A\vee B}{A,B}$$

plays a very special role in constructing deductive systems. Indeed, if $\mathsf{R}$ is a set of proper m-rules such that $\mathsf{R}⊢\mathsf{de}$, we can replace the set of m-rules $\mathsf{R}$ by $\mathsf{de}$ and the set of conclusive rules

$${\mathsf{R}}^{\left(1\right)}:=\{\mathrm{\Gamma }/\bigvee \mathsf{\Delta }:\mathrm{\Gamma }/\mathsf{\Delta }\in \mathsf{R}\},$$

where $\bigvee \mathsf{\Delta }:={\bigvee }_{A\in \mathsf{\Delta }}A$. Indeed, if in an inference we apply m-rule $\mathrm{\Gamma }/\mathsf{\Delta }$, instead, we can apply rule $\mathrm{\Gamma }/\bigvee \mathsf{\Delta }$, and then apply $n-1$ times m-rule $\mathsf{de}$ (where $n=\left|\mathsf{\Delta }\right|$). In this section, we discuss the sufficient conditions for logics to have an analog of ∨-elimination.

4.1. m-Protodisjunction

Let $\nabla (p,q)$ be a formula (a nonempty finite set of formulas) in two variables (in the sequel we write $p\nabla q$ to make the meaning more transparent). Then we let

$$\begin{array}{cc}\mathsf{de}:=p\nabla q/p,q\hfill & (\mathrm{Disjunction}\mathrm{Elimination})\hfill \\ \mathsf{dir}:=p/p\nabla q\hfill & (\mathrm{Disjunction}\mathrm{Introduction-Right})\hfill \\ \mathsf{dil}:=q/p\nabla q\hfill & (\mathrm{Disjunction}\mathrm{Introduction-Left})\hfill \end{array}$$

In the case when ∇ contains more then one formula,

$$\begin{array}{cc}\mathsf{de}:=p\nabla q/p,q\hfill & (\mathrm{Disjunction}\mathrm{Elimination})\hfill \\ \mathsf{dir}:=p/D(p,q)\mathrm{for}\mathrm{each}D\in \nabla \hfill & (\mathrm{Disjunction}\mathrm{Introduction-Right})\hfill \\ \mathsf{dil}:=q//D(p,q)\mathrm{for}\mathrm{each}D\in \nabla \hfill & (\mathrm{Disjunction}\mathrm{Introduction-Left})\hfill \end{array}$$

We will use the following rules capturing the properties of ∇.

$$\begin{array}{cc}\mathsf{dc}:=(p\nabla q)/(q\nabla p)\hfill & \left(\mathrm{Commutativity}\right)\hfill \\ \mathsf{dra}:=\left(\right(p\nabla q)\nabla r)/(p\nabla (q\nabla r\left)\right)\hfill & (\mathrm{Right}\mathrm{associativity})\hfill \\ \mathsf{dla}:=\left(\right(p\nabla q)\nabla r)/(p\nabla (q\nabla r\left)\right)\hfill & (\mathrm{Left}\mathrm{associativity})\hfill \\ \mathsf{dd}:=\left(\right(p\nabla r)\nabla (q\nabla r\left)\right)/(p\nabla (q\nabla r\left)\right)\hfill & \left(\mathrm{Self-distributivity}\right)\hfill \\ \mathsf{di}:=(p\nabla p)/p\hfill & \left(\mathrm{Idempotency}\right)\hfill \end{array}$$

Let

$$\mathsf{D}:=\{\mathsf{dc},\mathsf{dra},\mathsf{dla},\mathsf{dd},\mathsf{di}\}$$

(3)

be the set of rules representing the properties of ∇.

Proposition 3.

The following hold;

$$\begin{array}{cc}\hfill DC:& \mathsf{de},\mathsf{dir},\mathsf{dil}⊢\mathsf{dc}\hfill \\ \hfill DRA:& \mathsf{de},\mathsf{dir},\mathsf{dil}⊢\mathsf{dra}\hfill \\ \hfill DLA:& \mathsf{de},\mathsf{dir},\mathsf{dil}⊢\mathsf{dla}\hfill \\ \hfill DD:& \mathsf{de},\mathsf{dir},\mathsf{dil}⊢\mathsf{dd}\hfill \\ \hfill DI:& \mathsf{de},\mathsf{dir},\mathsf{dil}⊢\mathsf{di}\hfill \end{array}$$

Proof. 

The proofs of (DC), (DRA), and (DD) are depicted in Figure 12. Proof of (DLA) is similar to the proof of (DRA), and (DI) is an immediate consequence of $\mathsf{de}$ and the definition of m-inference. □

Definition 6.

A set of m-rules $\mathsf{R}$ is m-disjunctive if for some formula $\nabla (p,q)$ (some nonempty finite set of formulas) in two variables, rules $\mathsf{dir},\mathsf{dil}$, and $\mathsf{de}$ are derivable from $\mathsf{R}$, and we call formula(s) $\nabla$ an m-protodisjunction for $\mathsf{R}$ (comp. with the notion of protodisjunction in works by the authors of [13,17]).

Definition 7.

An m-logic $\mathsf{L}$ has the disjunction property ($\mathsf{DP}$ for short) if rules $\mathsf{dir}$, $\mathsf{dil}$, and $\mathsf{de}$ are admissible in $\mathsf{L}$, that is, if $\tilde{\mathsf{L}}$ is m-disjunctive.

For instance, modal logic $\mathsf{S}4$ has the Disjunction property relative to m-protodisjunction $\nabla :=(\square p\vee \square q)$.

Let us observe that if $\mathsf{R}$ is an m-disjunctive set (or $\mathsf{L}$ enjoys the $\mathsf{DP}$), then rules $\mathsf{dc},\mathsf{dra},\mathsf{dla},\mathsf{dd},\mathsf{di}$ are derivable from $\mathsf{R}$ (or respectively, these rules are admissible for $\mathsf{L}$).

It is important that m-protodisjunction is defined uniquely up to $\mathsf{R}$-equivalence in the following sense.

Let $\mathsf{R}$ be a set of m-rules. Sets of formulas $\mathrm{\Gamma }$ and $\mathsf{\Delta }$ are said to be $\mathsf{R}$-equivalent if

$$\mathrm{\Gamma }⊢{}_{\mathsf{R}}D,\mathrm{for}\mathrm{each}D\in \mathsf{\Delta }\mathrm{and}\mathsf{\Delta }⊢{}_{\mathsf{R}}A,\mathrm{for}\mathrm{each}A\in \mathrm{\Gamma }.$$

Proposition 4.

Let $\mathsf{R}$ be an m-disjunctive set of rules, and ${\nabla }_0$ and ${\nabla }_1$ be m-protodisjunctions for $\mathsf{R}$. Then ${\nabla }_0$ and ${\nabla }_1$ are $\mathsf{R}$-equivalent.

Proof. 

Suppose that $D\in {\nabla }_1$ and ${\nabla }_0=\{D_i,i<n\}$. An m-inference of D from ${\nabla }_0$ is depicted in Figure 13. □

Let us note, that if a logic has conjunction with regular properties, $\nabla$ can be reduced to a single formula.

Note 1.

In order not to add an extra layer of complexity, in this paper we consider only the case when $\nabla$ consists of a single formula, even though the main results hold in a general case.

If $\mathsf{R}$ is an m-disjunctive set of m-rules or if ${⊢}_{\mathsf{L}}$ is an m-logic with the $\mathsf{DP}$, we always assume that meta-disjunction is expressible by a formula $\nabla$.

Example 3.

Let us consider intuitionistic propositional logic $\mathsf{Int}$ and normal modal logic $\mathsf{S}4$. For $\mathsf{Int}$ we can take $p\nabla q=p\vee q$. For $\mathsf{S}4$ we can take $p\nabla q=\square p\vee \square q$. It is clear that rules $\mathsf{dir}$ and $\mathsf{dil}$ are derivable in these logics, that is, $p{⊢}_{\mathsf{L}}p\nabla q$ and $q{⊢}_{\mathsf{L}}p\nabla q$, where $\mathsf{L}\in \{\mathsf{Int},\mathsf{S}4\}$, and all three rules ($\mathsf{dir}$, $\mathsf{dil}$, and $\mathsf{de}$) are admissible for $\mathsf{Int}$ and $\mathsf{S}4$ [11]. For logic $\mathsf{BCK}$ one can take $p\nabla q=(p\to q)\to q$. Let us point out that rule $\mathsf{dc}:=p\nabla q/q\nabla p$ is admissible for $\mathsf{BCK}$, but it is not derivable [18] (Theorem 4.2).

4.2. Properties of m-Protodisjunction

In this section, we prove that with respect to $\mid \sim$, m-protodisjunction has the properties which disjunction is expected to have.

Proposition 5.

Suppose $\nabla$ is an m-protodisjunction for a set of m-rules $\mathsf{R}$. Then for any formulas $A,B\in \mathsf{Fm}$, and any $\mathrm{\Gamma },\mathsf{\Delta }⋐\mathsf{Fm}$,

$$\mathrm{\Gamma },A{⊢}_{\mathsf{R}}\mathsf{\Delta }\mathit{and}\mathrm{\Gamma },B{⊢}_{\mathsf{R}}\mathsf{\Delta }\mathit{entails}\mathrm{\Gamma },A\nabla B{⊢}_{\mathsf{R}}\mathsf{\Delta }.$$

(4)

Proof. 

One can apply $\mathsf{de}$ to $\mathrm{\Gamma },A\nabla B$ and obtain two cases to consider: $\mathrm{\Gamma },A$ and $\mathrm{\Gamma },B$. In each of these cases one can derive $\mathsf{\Delta }$. □

Immediately from Proposition 5 it follows that if ${⊢}_{\mathsf{L}}$ is an m-logic enjoying the $\mathsf{DP}$, then for any formulas $A,B\in \mathsf{Fm}$ and any $\mathrm{\Gamma },\mathsf{\Delta }⋐\mathsf{Fm}$,

$$\mathrm{\Gamma },A\mid {\sim }_{\mathsf{L}}\mathsf{\Delta }\mathrm{and}\mathrm{\Gamma },B\mid {\sim }_{\mathsf{L}}\mathsf{\Delta }\mathrm{entails}\mathrm{\Gamma },A\nabla B\mid {\sim }_{\mathsf{L}}\mathsf{\Delta }$$

(5)

and consequently,

$$\mathrm{\Gamma },A\mid {\sim }_{\mathsf{L}}C\mathrm{and}\mathrm{\Gamma },B\mid {\sim }_{\mathsf{L}}C\mathrm{entails}\mathrm{\Gamma },A\nabla B\mid {\sim }_{\mathsf{L}}C,,$$

(6)

and

$$A\mid {\sim }_{\mathsf{L}}C\mathrm{and}B\mid {\sim }_{\mathsf{L}}C\mathrm{entails}A\nabla B\mid {\sim }_{\mathsf{L}}C.$$

(7)

If $\mathsf{\Delta }:=\{B_0,\cdots ,B_{m-1}\}$ is a finite set of formulas, we let

$$\begin{array}{cc}\nabla (\varnothing ):=\varnothing \hfill & ,\mathrm{when}m=0\hfill \\ \nabla \left(\left\{B_0\right\}\right):=B_0\hfill & ,\mathrm{when}m=1\hfill \\ \nabla \left(\mathsf{\Delta }\right):=B_0\nabla \cdots \nabla B_{m-1}\hfill & ,\mathrm{when}m>1.\hfill \end{array}$$

(8)

Thus, ∇ converts any finite nonempty set of formulas into a single formula.

m-Protodisjunction has the following property.

Corollary 4.

Suppose $\Delta$ is a nonempty finite set of formulas and $\mathsf{R}$ is a set of m-rules with m-protodisjunction $\nabla$ (or ${⊢}_{\mathsf{L}}$ is an m-logic with the $\mathsf{DP}$). Then

$${⊢}_{\mathsf{R}}\nabla \left(\mathsf{\Delta }\right)\mathit{if}\mathit{and}\mathit{only}\mathit{if}{⊢}_{\mathsf{R}}B\mathit{for}\mathit{some}B\in \mathsf{\Delta }$$

(accordingly, $\mid {\sim }_{\mathsf{L}}\nabla \left(\mathsf{\Delta }\right)$ if and only if $\mid {\sim }_{\mathsf{L}}B$ for some $B\in \mathsf{\Delta }$).

Proof. 

The corollary can be proven by a simple induction on cardinality of $\mathsf{\Delta }$. □

Let us introduce the following notations: suppose that A is a formula, $\mathrm{\Gamma },\mathsf{\Delta }$ are sets of formulas, $\mathsf{r}:=\mathrm{\Gamma }/\mathsf{\Delta }$, and q is a variable not occurring in A and formulas from $\mathrm{\Gamma }$ and $\mathsf{\Delta }$. Then

$$\begin{array}{cc}\left(a\right)\hfill & A^q:=A\nabla q;\hfill \\ \left(b\right)\hfill & \mathrm{if}\mathrm{\Gamma }\ne ⌀,\mathrm{then}{\mathrm{\Gamma }}^q:=\{A^q:A\in \mathrm{\Gamma }\};\hfill \\ \left(c\right)\hfill & {▼}^q:=▼\nabla q=▼(\mathrm{because}▼\mathrm{represents}\mathrm{meta-truth});\hfill \\ \left(d\right)\hfill & {▲}^q:=▲\nabla q=q(\mathrm{because}▲\mathrm{represents}\mathrm{meta-falshood});\hfill \\ \left(e\right)\hfill & {\mathsf{r}}^q:={\mathrm{\Gamma }}^q/{\mathsf{\Delta }}^q;\hfill \\ \left(f\right)\hfill & \nabla \left(\mathsf{r}\right):=\mathrm{\Gamma }/\nabla \left(\mathsf{\Delta }\right);\hfill \\ \left(g\right)\hfill & \check{\mathsf{r}}:={\mathrm{\Gamma }}^q/\nabla \left({\mathsf{\Delta }}^q\right),\mathrm{i}.\mathrm{e}.,\check{\mathsf{r}}=\nabla \left({\mathsf{r}}^q\right).\hfill \end{array}$$

(9)

If $\mathsf{R}$ is a set of m-rules and q is a variable not occurring in any m-rule from $\mathsf{R}$,

$${\mathsf{R}}^q:=\{{\mathsf{r}}^q:\mathsf{r}\in \mathsf{R}\}\mathrm{and}\check{\mathsf{R}}:=\{\check{\mathsf{r}}:\mathsf{r}\in \mathsf{R}\}$$

Remark 2.

Note that if $\mathsf{r}:=\mathrm{\Gamma }/▲$ is a terminating rule and $q\notin Var\left(\mathsf{r}\right)$, then, ${\mathsf{r}}^q={\mathrm{\Gamma }}^q/q$ and the latter is a conclusive rule. Thus, for any m-rule $\mathsf{r}:=\mathrm{\Gamma }/\mathsf{\Delta }$ and any $q\notin Var\left(\mathsf{r}\right)$, the rule $\check{\mathsf{r}}={\mathrm{\Gamma }}^q/\nabla \left({\mathsf{\Delta }}^q\right)$ is always a conclusive rule: even if $\mathsf{\Delta }=⌀$, we have ${▲}^q=q$ and $\nabla \left(q\right)=q$ (cf. Equation (8)). If $\mathsf{r}$ is a conclusive rule, the rules ${\mathsf{r}}^q$ and $\check{\mathsf{r}}$ coincide. Hence, if $\mathsf{R}$ is a set of conclusive rules, ${\mathsf{R}}^q=\check{\mathsf{R}}$.

Example 4.

If $\mathsf{r}:=(\neg p_0\to (p_1\vee p_2))/((\neg p_0\to p_1)\vee (\neg p_0\to p_2))$, then

$${\mathsf{r}}^q:=\frac{(\neg p_0\to (p_1\vee p_2))\vee q}{((\neg p_0\to p_1)\vee (\neg p_0\to p_2))\vee q}.$$

Rule $\mathsf{r}$ is admissible for any extension of $\mathsf{Int}$ [19], while rule ${\mathsf{r}}^q$ is admissible for any extension of $\mathsf{Int}$ enjoying the disjunction property.

If $\mathsf{r}:=\diamond p\wedge \diamond \neg p/▲$, then

$${\mathsf{r}}^q:=\frac{(\diamond p\wedge \diamond \neg p)\nabla q}{q},\mathit{where}\nabla \mathit{is}\mathit{the}\mathit{strong}\mathit{disjunction}:A\nabla B:=\square A\vee \square B.$$

Rule $\mathsf{r}$ is admissible for any normal modal logic extending $\mathsf{D}4$ [10], while rule ${\mathsf{r}}^q$ is admissible for any normal modal logic extending $\mathsf{D}4$ enjoying the disjunction property.

Proposition 6.

Let $\mathsf{R}$ be a set of conclusive rules, Γ be a finite set of formulas and $A,B,C$ be formulas. Then,

$$\mathsf{R}⊢\frac{\mathrm{\Gamma },A}{C}\mathit{entails}\mathsf{D},{\mathsf{R}}^q⊢\frac{\mathrm{\Gamma },A\nabla B}{C\nabla B}.$$

Proof. 

Let I be a single-conclusion inference of C from $\mathrm{\Gamma },A$. Then C is the last formula in I. There are three cases to consider: (a) $C=A$; (b) $C\in \mathrm{\Gamma }$; (c) C is obtained from some preceding formulas by a conclusive rule from $\mathsf{R}$.

Case (a). Is trivial.

Case (b). If $C\in \mathrm{\Gamma }$, then by the definition of m-inference, $\mathsf{R}⊢\mathrm{\Gamma }/C$. Thus, $\mathsf{R}⊢\mathrm{\Gamma },A\nabla B/C$ and, by $\mathsf{dir}$, we get $⊢\mathrm{\Gamma },A\nabla B/C\nabla B$.

Case (c). Suppose C is obtained by an instance $C_0,\cdots ,C_{m-1}/C$ of some rule $\mathsf{r}\in \mathsf{R}$. Then,

$$C_0\nabla B,\cdots ,C_{m-1}\nabla B/C\nabla B$$

is an instance of ${\mathsf{r}}^q$ and we can easily convert inference I into the inference of $C\nabla B$ (see Figure 14). □

Corollary 5.

Let $\mathsf{R}$ be a set of conclusive rules, Γ be a finite set of formulas and $A_0,\cdots ,A_{m-1},C$ be formulas. Then, for any $i<m$,

$$\mathsf{R}⊢\frac{\mathrm{\Gamma },A_i}{C}entails\mathsf{D},{\mathsf{R}}^q⊢\frac{\mathrm{\Gamma },A_0\nabla \cdots \nabla A_{m-1}}{A_0\nabla \cdots \nabla A_{i-1}\nabla C\nabla A_{i+1}\nabla \cdots \nabla A_{m-1}}.$$

Proof. 

Indeed, for $i=0$ we can take $B=A_1\nabla \cdots \nabla A_{m-1}$ and use Proposition 6. In the case when $i>0$, we can use commutativity and associativity of $\nabla$ and reduce this case to the case $i=0$. □

5. From Admissible m-Base to Admissible Base

Our goal is to demonstrate that for any consistent m-logic with the $\mathsf{DP}$, the problem of admissibility of any given proper m-rule can be reduced to the problem of admissibility of some conclusive rule.

Theorem 3.

Suppose ${⊢}_{\mathsf{L}}$ is a consistent m-logic with the $\mathsf{DP}$. Let $\mathsf{r}:=\mathrm{\Gamma }/\mathsf{\Delta }$ be a proper m-rule and q be a variable not occurring in $\mathsf{r}$. Then the following are equivalent.

(a) 

m-Rule $\mathsf{r}$ is admissible for ${⊢}_{\mathsf{L}}$;

(b) 

m-Rule ${\mathsf{r}}^q$ is admissible for ${⊢}_{\mathsf{L}}$;

(c) 

Rule $\check{\mathsf{r}}={\mathrm{\Gamma }}^q/\nabla \left({\mathsf{\Delta }}^q\right)$ is admissible for ${⊢}_{\mathsf{L}}$;

(d) 

Rule $\nabla \left(\mathsf{r}\right)=\mathrm{\Gamma }/\nabla \left(\mathsf{\Delta }\right)$ is admissible for ${⊢}_{\mathsf{L}}$.

Proof. 

(a) ⇒ (b). Assume that proper m-rule $\mathsf{r}:=\mathrm{\Gamma }/\mathsf{\Delta }$ is admissible for ${⊢}_{\mathsf{L}}$. Because $\mathsf{r}$ is proper, $\mathsf{\Delta }\ne ⌀$. Let us consider the three following cases:

• $\mathrm{\Gamma }=⌀$, that is, $\mathsf{r}=▼/\mathsf{\Delta }$ and ${\mathsf{r}}^q=▼/{\mathsf{\Delta }}^q$;
• $\mathrm{\Gamma }\ne ⌀$, that is ${\mathsf{r}}^q={\mathrm{\Gamma }}^q/{\mathsf{\Delta }}^q$.

Case$\mathrm{\Gamma }=⌀$. Admissibility of $▼/\mathsf{\Delta }$ entails that there is $B\in \mathsf{\Delta }$ such that ${⊢}_{\mathsf{L}}B$ and consequently, for every substitution $\sigma$, ${⊢}_{\mathsf{L}}\sigma \left(B\right)$. Hence, because $\mathsf{dir}$ is admissible for ${⊢}_{\mathsf{L}}$, for every substitution $\sigma$, we have ${⊢}_{\mathsf{L}}\sigma \left(B\right)\nabla \sigma \left(q\right)$ and therefore, rule $▼/{\mathsf{\Delta }}^q$ is admissible for ${⊢}_{\mathsf{L}}$.

Case$\mathrm{\Gamma }\ne ⌀$. We need to prove that for any substitution $\sigma$,

$$\mathrm{if}{⊢}_{\mathsf{L}}\sigma \left(A\right)\nabla \sigma \left(q\right)\mathrm{for}\mathrm{all}A\in \mathrm{\Gamma },\mathrm{then}\mathrm{there}\mathrm{is}B\in \mathsf{\Delta }\mathrm{such}\mathrm{that}{⊢}_{\mathsf{L}}\sigma \left(B\right)\nabla \sigma \left(q\right).$$

Let $\sigma$ be a unifier of ${\mathrm{\Gamma }}^q$, that is ${⊢}_{\mathsf{L}}\sigma \left(A\right)\nabla \sigma \left(q\right)$ for all $A\in \mathrm{\Gamma }$. Let us consider two subcases:

(i)

$\sigma$ unifies $\mathrm{\Gamma }$;

(ii)

$\sigma$ does not unify $\mathrm{\Gamma }$.

Proof of (i).

Recall that $\mathsf{r}$ is admissible for ${⊢}_{\mathsf{L}}$. Therefore, if $\sigma$ unifies $\mathrm{\Gamma }$, that is, ${⊢}_{\mathsf{L}}\sigma \left(A\right)$ holds for all $A\in \mathrm{\Gamma }$, by admissibility, there is $B\in \mathsf{\Delta }$ such that ${⊢}_{\mathsf{L}}\sigma \left(B\right)$. Hence, because rule $\mathsf{dir}$ is admissible for ${⊢}_{\mathsf{L}}$, we can apply it and obtain ${⊢}_{\mathsf{L}}\sigma \left(B\right)\nabla \sigma \left(q\right)$. □

Proof of (ii).

Suppose that $\sigma$ does not unify $\mathrm{\Gamma }$. Then, there is $A\in \mathrm{\Gamma }$ such that ${⊬}_{\mathsf{L}}$σ(A). On the other hand, $\sigma$ unifies ${\mathrm{\Gamma }}^q$ and hence, ${⊢}_{\mathsf{L}}\sigma \left(A\right)\nabla \sigma \left(q\right)$. Then, by the Disjunction Property, ${⊢}_{\mathsf{L}}\sigma \left(q\right)$. Rule $\mathsf{dil}$ is admissible for ${⊢}_{\mathsf{L}}$, hence, ${⊢}_{\mathsf{L}}\sigma \left(q\right)$ entails ${⊢}_{\mathsf{L}}\sigma \left(B\right)\nabla \sigma \left(q\right)$ for every $B\in \mathsf{\Delta }$. □

(b) ⇒ (c). Suppose m-rule ${\mathsf{r}}^q:={\mathrm{\Gamma }}^q/{\mathsf{\Delta }}^q$ is admissible for ${⊢}_{\mathsf{L}}$. We need to prove that rule ${\mathrm{\Gamma }}^q/\nabla \left({\mathsf{\Delta }}^q\right)$ is admissible for ${⊢}_{\mathsf{L}}$. Let $\sigma$ be a substitution which unifies ${\mathrm{\Gamma }}^q$, that is, $\sigma$ makes all premises ${\mathrm{\Gamma }}^q$ derivable. Then, our assumption entails that ${⊢}_{\mathsf{L}}\sigma \left(B^q\right)$ holds for some $B\in \mathsf{\Delta }$. Hence, by virtue of Corollary 4, ${⊢}_{\mathsf{L}}\nabla \left(\sigma \left({\mathsf{\Delta }}^q\right)\right)$ which means that ${⊢}_{\mathsf{L}}\sigma (\nabla \left({\mathsf{\Delta }}^q\right))$ holds.

(c) ⇒ (d). Suppose that rule ${\mathrm{\Gamma }}^q/\nabla \left({\mathsf{\Delta }}^q\right)$ is admissible for ${⊢}_{\mathsf{L}}$. We need to prove that rule $\mathrm{\Gamma }/\nabla \left(\mathsf{\Delta }\right)$ is admissible for ${⊢}_{\mathsf{L}}$. Let us consider two cases: $\mathrm{\Gamma }=\varnothing$ and $\mathrm{\Gamma }\ne \varnothing$.

Case$\mathrm{\Gamma }=\varnothing$, that is, rule $▼/\nabla \left({\mathsf{\Delta }}^q\right)$ is admissible for ${⊢}_{\mathsf{L}}$. Hence, if $\mathsf{\Delta }$ consists of a single formula B, we have ${⊢}_{\mathsf{L}}{B}^q$. If $\mathsf{\Delta }$ contains more than one formula, by the disjunction property, there is a formula $B\in \mathsf{\Delta }$ such that ${⊢}_{\mathsf{L}}{B}^q$. If we take into account that ${⊬}_{\mathsf{L}}$q and apply the disjunction property to ${⊢}_{\mathsf{L}}B\nabla q$, we can conclude that ${⊢}_{\mathsf{L}}B$ holds and hence, ${⊢}_{\mathsf{L}}\sigma \left(B\right)$ holds for every substitution $\sigma$. Thus, rule $▼/\nabla \left(\mathsf{\Delta }\right)$ is admissible for ${⊢}_{\mathsf{L}}$.

Case$\mathrm{\Gamma }\ne \varnothing$ and we need to show that rule $\mathrm{\Gamma }/\nabla \left(\mathsf{\Delta }\right)$ is admissible for ${⊢}_{\mathsf{L}}$. Let $\sigma$ be a substitution that unifies $\mathrm{\Gamma }$, that is ${⊢}_{\mathsf{L}}\sigma \left(A\right)$ for all $A\in \mathrm{\Gamma }$.

Recall that ${⊢}_{\mathsf{L}}$ is consistent, therefore there is a formula C such that ${⊬}_{\mathsf{L}}$C. Take the substitution

$${\sigma }^{\prime }\left(p\right)=\left\{\begin{array}{cc}\sigma \left(p\right),\hfill & \mathrm{if}p\ne q\hfill \\ C\hfill & \mathrm{otherwise}.\hfill \end{array}\right.$$

Because q does not occur in formulas from $\mathrm{\Gamma }$, for all $A\in \mathrm{\Gamma }$, ${\sigma }^{\prime }\left(A\right)=\sigma \left(A\right)$, and, consequently, ${\sigma }^{\prime }\left(A^q\right)=\sigma \left(A\right)\nabla C$. By the assumption, ${⊢}_{\mathsf{L}}\sigma \left(A\right)$, and hence by $\mathsf{dir}$, ${⊢}_{\mathsf{L}}\sigma \left(A\right)\nabla C$, that is, ${⊢}_{\mathsf{L}}{\sigma }^{\prime }\left(A^q\right)$. Thus, ${\sigma }^{\prime }$ unifies ${\mathrm{\Gamma }}^q$. Now, we can apply the assumption that rule ${\mathrm{\Gamma }}^q/{\mathsf{\Delta }}^q$ is admissible, and we can conclude that for some formula $B\in \mathsf{\Delta }$, formula ${\sigma }^{\prime }\left(B^q\right)$ is derivable. Thus, because ${\sigma }^{\prime }\left(B^q\right)={\sigma }^{\prime }\left(B\nabla q\right)={\sigma }^{\prime }\left(B\right)\nabla C$, formula ${\sigma }^{\prime }\left(B\right)\nabla C$ is a theorem. Recall that we selected C not to be a theorem, hence, by the Disjunction Property, formula ${\sigma }^{\prime }\left(B\right)$ is a theorem. And because variable q does not occur in B, we have ${\sigma }^{\prime }\left(B\right)=\sigma \left(B\right)$, and it means that $\sigma \left(B\right)$ is a theorem and rule $\mathrm{\Gamma }/\mathsf{\Delta }$ is admissible.

(d) ⇒ (a). Suppose that the rule $\mathrm{\Gamma }/\nabla \left(\mathsf{\Delta }\right)$ is admissible for ${⊢}_{\mathsf{L}}$. Let $\sigma$ be a unifier for $\mathrm{\Gamma }$. Then, by the admissibility of $\mathrm{\Gamma }/\nabla \left(\mathsf{\Delta }\right)$, we have $⊢\sigma (\nabla (\mathsf{\Delta }\left)\right)$. Now, we can apply Corollary 4 and conclude that for some $B\in \mathsf{\Delta }$, ${⊢}_{\mathsf{L}}\sigma \left(B\right)$. Thus, the rule $\mathrm{\Gamma }/\mathsf{\Delta }$ is admissible in ${⊢}_{\mathsf{L}}$.  □

Remark 3.

For any consistent m-logic ${⊢}_{\mathsf{L}}$ with the disjunction property, the rules $\mathsf{r}$ and ${\mathsf{r}}^q$ are either both admissible, or both not admissible. Moreover, $\mathsf{r}$ can be derived from ${\mathsf{r}}^q$, while the converse needs not to be true: the restricted Visser rule $V_n^{-}$ is derivable from the Visser rule $V_n$ [20], while the converse does not hold [21] (Corollary 2). If the m-rules $\mathsf{dir}$, $\mathsf{dil}$, and $\mathsf{de}$ are not just admissible (which is required by the disjunction property), but they are derivable in ${⊢}_{\mathsf{L}}$, then ${\mathsf{r}}^q$ is derivable from $\mathsf{r}$.

Logic $\mathsf{L}$ is a-decidable if the problem of admissibility of conclusive rules in $\mathsf{L}$ is decidable, and logic $\mathsf{L}$ is am-decidable if the problem of admissibility of m-rules in $\mathsf{L}$ is decidable.

Corollary 6.

For every consistent m-logic with the DP, the problems of a- and am-admissibility are equivalent.

Example 5.

It is well known from [11] that logics $\mathsf{Int},\mathsf{S}4,\mathsf{K}4,\mathsf{Grz},\mathsf{GL}$ enjoy the DP. Therefore, because the problem of a-admissibility for them is decidable [22,23,24], the problem of m-admissibility for these logics is decidable too. In algebraic terms, for each of these logics, the universal theory of the Lindenbaum algebra is decidable [24] (Theorem 10).

5.1. A Note on Terminating Rules

The goal of this section is to show that terminating rules can be eliminated from any m-inference of any proper rule.

If $\mathsf{R}$ is a set of m-rules, by $\overline{\mathsf{R}}$ we denote a set of proper m-rules obtained from $\mathsf{R}$ by replacing every terminating rule $\mathsf{t}:=A_1,\cdots ,A_n/▲\in \mathsf{R}$ with conclusive rule $\overline{\mathsf{t}}:=A_1,\cdots ,A_n/q$, where q does not occur in any of formulas $A_i,i=1,\cdots ,n.$

Proposition 7.

Suppose that there is an m-inference I of a proper rule $\mathrm{\Gamma }/\mathsf{\Delta }$ from $\mathsf{R}$. Then, there is an inference $\overline{I}$ of $\mathrm{\Gamma }/\mathsf{\Delta }$ from $\overline{\mathsf{R}}$ that does not contain terminal leaves.

Proof. 

Let I be an m-inference of $\mathrm{\Gamma }/\mathsf{\Delta }$ from $\mathsf{R}$. By assumption, rule $\mathrm{\Gamma }/\mathsf{\Delta }$ is proper, hence, $\mathsf{\Delta }$ is not empty. Suppose that $B\in \mathsf{\Delta }$.

Let us observe that, by the definition of m-inference, application of any terminating rule gives a leaf of this m-inference. Thus, if $\mathsf{t}=A_1,\cdots ,A_n/▲\in \mathsf{R}$ and $\sigma \left(A_1\right),\cdots ,\sigma \left(A_n\right)/▲$ is an instance of $\mathsf{t}$ that we have been used in I, instead, we can use the instance $\sigma \left(A_1\right),\cdots ,\sigma \left(A_n\right)/B$ of a proper rule $\overline{\mathsf{t}}$ that belongs to $\overline{\mathsf{R}}$. And in such a way, we can eliminate all applications of the terminating rules from I. □

From Proposition 7 it immediately follows that for strongly consistent logics any m-base (finite m-base) can be converted into an m-base (finite m-base) containing at most one terminating m-rule.

Proposition 8.

Let $\mathsf{R}$ be an m-base (a relative m-base) of strongly consistent m-logic in which formula A is not unifiable and let ${\mathsf{R}}^{\prime }:=\overline{\mathsf{R}}\cup \{A/▲\}$. Then ${\mathsf{R}}^{\prime }$ is an m-base (relative m-base).

Proof. 

First, from Proposition 7, it follows that every conclusive admissible rule is derivable from $\overline{\mathsf{R}}$. Next, if m-rule $\mathrm{\Gamma }/▲$ is admissible, then rule $\mathrm{\Gamma }/A$ is admissible too, and hence it is derivable from $\overline{\mathsf{R}}$. Thus, m-rule $\mathrm{\Gamma }/▲$ is derivable from $\overline{\mathsf{R}}$. □

5.2. Converting Admissible m-Base into Admissible Base

To convert a given relative admissible m-base $\mathsf{R}$ of a given logic $\mathsf{L}$ with the $\mathsf{DP}$ into a relative base, one can do the following: convert every rule $\mathsf{r}=\mathrm{\Gamma }/\mathsf{\Delta }$ from $\mathsf{R}$ into rule ${\mathrm{\Gamma }}^q/\nabla \left({\mathsf{\Delta }}^q\right)$; the obtained set of rules we denote $\check{\mathsf{R}}$. The set $\check{\mathsf{R}}$ consists of conclusive rules (cf. Remark 2). From Theorem 3 we know that each rule from $\check{\mathsf{R}}$ remains admissible. Below, we show that every admissible for $\mathsf{L}$ conclusive rule can be derived from $\check{\mathsf{R}}$. Let us note that as a result of such a conversion some m-rules become trivial, for instance, $\widehat{\mathsf{de}}$:

$$p_1\nabla p_2/p_1,p_2\mathrm{becomes}{p}_1\nabla p_2\nabla q/p_1\nabla p_2\nabla q.$$

Theorem 4.

Suppose that $\mathsf{L}$ is a logic with the $\mathsf{DP}$ and $\mathsf{R}$ is an admissible m-base (a relative m-base) of $\mathsf{L}$, then, $\check{\mathsf{R}}$ is an admissible base (respectively, a relative base) of $\mathsf{L}$.

To prove Theorem 4, we prove a bit more general Theorem 5, which holds not only for the logics enjoying the $\mathsf{DP}$. Recall from Proposition 3 that all rules from $\mathsf{D}$ (cf. Equation (3)) representing the properties of ∇ are derivable in any logic with the $\mathsf{DP}$. Hence, we can take $\mathsf{\Delta }$ in Theorem 5 to be a singleton, and we will obtain Theorem 4 as a corollary.

Theorem 5.

Suppose $\mathsf{R}$ is a set of proper m-rules, and $\mathsf{r}:=\mathrm{\Gamma }/\mathsf{\Delta }$ is a proper rule. If

$$\mathsf{R}⊢\mathrm{\Gamma }/\mathsf{\Delta },$$

then

$$\mathsf{D},\check{\mathsf{R}}⊢\mathrm{\Gamma }/\nabla \left(\mathsf{\Delta }\right).$$

In other words, any m-inference of $\mathrm{\Gamma }/\mathsf{\Delta }$ from $\mathsf{R}$ can be converted into inference of $\mathrm{\Gamma }/\nabla \left(\mathsf{\Delta }\right)$ from $\check{\mathsf{R}}$ which is a single-conclusion inference, because all rules from $\mathsf{D}$ and $\check{\mathsf{R}}$ are conclusive.

Proof. 

Let I be a $(\mathrm{\Gamma },\mathsf{R})$-inference and $\mathsf{\Delta }$ is a set of formulas which appear in the leaves of I. Without loss of generality we can assume that each formula from $\mathsf{\Delta }$ appears in a leaf of the inference: if $\lambda \left(lv\left(I\right)\right)={\mathsf{\Delta }}^{\prime }⊈\mathsf{\Delta }$, after we have derived $\nabla \left({\mathsf{\Delta }}^{\prime }\right)$, we can apply (multiple times if necessary) rule $\mathsf{dir}$ and derive $\nabla \left(\mathsf{\Delta }\right)$.

Let k be the number of nodes of I having more than one immediate successor (in other words, k represents the number of applications of inconclusive rules). By induction on k we prove that for any $(\mathrm{\Gamma },\mathsf{R})$-inference, such that $\lambda \left(lv\right(I\left)\right)=\mathsf{\Delta }$, there is a $(\mathrm{\Gamma },\mathsf{D}\cup \check{\mathsf{R}})$-inference, $I^{\prime }$, such that $\lambda \left(lv\left(I^{\prime }\right)\right)=\nabla \left(\mathsf{\Delta }\right)$. Let us note that because all members of $\mathsf{D}\cup \check{\mathsf{R}}$ are conclusive rules, $I^{\prime }$ is a linear inference and has a single leaf labeled by $\nabla \left(\mathsf{\Delta }\right)$.

Basis. If $k=0$, then I is a linear inference. By the assumption, $\mathsf{R}$ is a set of proper m-rules and therefore, it does not contain any terminating rules. Hence, the leaf of I contains a formula D from $\mathsf{\Delta }$, and using the rules from $\mathsf{D}$ one can easily extend I to derive $\nabla \left(\mathsf{\Delta }\right)$.

Assumption. Assume that for any $(\mathrm{\Gamma },\mathsf{R})$-inference I having less than k branching nodes, there is an $(\mathsf{D}\cup \check{\mathsf{R}},\mathrm{\Gamma })$- inference $I^{\prime }$ the leaf of which contains $\nabla \left(\mathsf{\Delta }\right)$.

Step. Let I be a $(\mathrm{\Gamma },\mathsf{R})$-inference having k branching nodes. Let $\mathfrak{n}$ be a branching node having no branching successors. Suppose that $B_0,\cdots ,B_{m-1}$ is a list of formulas in the leaves below $\mathfrak{n}$, and $B_m,\cdots ,B_{n-1}$ is a list of all formulas in the leaves that are not successors of $\mathfrak{n}$. Assume also that $\lambda \left(\mathfrak{n}\right)=B$ (see Figure 15) and alternatives $C_0,\cdots ,C_{m-1}$ are obtained by application of inconclusive rule $\mathsf{r}:=A_0,\cdots ,A_{s-1}/C_0,\cdots ,C_{m-1}$ from $\mathsf{R}$.

Let us remove all successors of $\mathfrak{n}$ from I. By Proposition 1(a), the resulting tree is also a $(\mathrm{\Gamma },\mathsf{R})$-inference with $B,B_m,\cdots ,B_{n-1}$ in its leaves (see the left-hand side of Figure 16).

Observe that $\check{\mathsf{r}}=A_0\nabla q,\cdots ,A_{n-1}\nabla q/C_0\nabla \cdots \nabla C_{m-1}\nabla q$, hence

$$A_0\nabla \overline{C},\cdots ,A_{s-1}\nabla \overline{C}/C_0\nabla \cdots \nabla C_{m-1}\nabla \overline{C},$$

(10)

where $\overline{C}:=C_0\nabla \cdots \nabla C_{m-1}$, is an instance of $\check{\mathsf{r}}$. As all formulas $A_0,\cdots ,A_{s-1}$ are in the nodes preceding $\mathfrak{n}$, we can extend the reduced inference (see Figure 16).

By Corollary 5, from $C_0\nabla C_1\nabla \cdots \nabla C_{m-1}$ we can derive

$$B_0\nabla C_1\nabla \cdots \nabla C_{m-1}.$$

Then we can apply Corollary 5 again and get

$$B_0\nabla B_1\nabla \cdots \nabla C_{m-1}.$$

And so on, until we got

$$B_0\nabla B_1\nabla \cdots \nabla B_{m-1}$$

In such a way we obtain the inference depicted in Figure 17.

Let us observe that the obtained inference contains $k-1$ branching nodes, therefore we can apply the induction assumption and convert the obtained inference into an inference of $B_0\nabla \cdots \nabla B_{n-1}$, using, if necessary, rules from $\mathsf{D}$. □

Corollary 7.

Suppose that $\mathsf{L}$ is a logic enjoying the $\mathsf{DP}$. Then, if $\mathsf{L}$ has a finite admissible m-base (relative m-base), then, $\mathsf{L}$ has a finite admissible base (relative base).

Example 6.

It was proven in [22] by Rybakov that logics $\mathsf{Int}$ and $\mathsf{S}4$ have no finite relative admissible bases. Hence, these logics have no finite relative admissible m-bases either.

6. From Admissible Base to Admissible m-Base

In the previous section we saw how to convert a given (relative) admissible m-base $\mathsf{R}$ of a logic with the $\mathsf{DP}$ into a (relative) admissible base $\check{\mathsf{R}}$. In this section, we show how to convert a given (relative) admissible base into a (relative) admissible m-base.

Theorem 6.

Suppose that $\mathsf{L}$ is a logic and $\mathsf{R}$ is an admissible base (relative base). Then, if $\mathsf{L}$ is strongly consistent and there is a nonunifiable in $\mathsf{L}$ finite set of formulas $\Xi$, the set $\mathsf{R}\cup \{\mathsf{DP},\Xi /▲\}$ is an admissible m-base (relative m-base); otherwise, $\mathsf{R}\cup \left\{\mathsf{DP}\right\}$ is an admissible m-base (relative m-base).

Proof. 

First, let us prove that every proper admissible rule is derivable from $\mathsf{R}\cup \left\{\mathsf{DP}\right\}$ for $\mathsf{L}$. Indeed, suppose that $\mathsf{r}:=\mathrm{\Gamma }/\mathsf{\Delta }$ is a proper m-rule admissible in $\mathsf{L}$. If $\mathsf{\Delta }$ consists of a single formula, m-rule $\mathsf{r}$ is a conclusive rule, and hence by the definition of the base, $\mathsf{r}$ is derivable from $\mathsf{R}$. Suppose $\left|\mathsf{\Delta }\right|>1$. Let us consider rule $\mathrm{\Gamma }/\nabla \left(\mathsf{\Delta }\right)$. By Theorem 3(d), $\mathrm{\Gamma }/\nabla \left(\mathsf{\Delta }\right)$ is admissible for $\mathsf{L}$, and hence, $\mathrm{\Gamma }/\nabla \left(\mathsf{\Delta }\right)$ is derivable from $\mathsf{R}$. Now, we can $\left|\mathsf{\Delta }\right|-1$ times apply $\mathsf{de}$ and obtain $\mathrm{\Gamma }/\mathsf{\Delta }$. Thus, $\mathrm{\Gamma }/\mathsf{\Delta }$ is derivable from $\mathsf{R}\cup \left\{\mathsf{DP}\right\}$.

For relative bases one can take a set of conclusive rules $\mathsf{L}\cup \mathsf{R}$ and repeat the preceding argument.

Next, we prove that if $\Xi$ is a finite nonunifiable in $\mathsf{L}$ set of formulas, then every admissible for $\mathsf{L}$ terminating m-rule can be derived from $\mathsf{R}\cup \{\Xi /▲\}$.

Indeed, suppose that m-rule $\mathsf{r}=\mathrm{\Gamma }/▲$ is admissible for $\mathsf{L}$. Then, $\mathrm{\Gamma }$ is a nonunifiable in $\mathsf{L}$ finite set of formulas and hence, conclusive rule $\mathrm{\Gamma }/A$ is admissible in $\mathsf{L}$ for every formula A. In particular, m-rules $\mathrm{\Gamma }/B$ are admissible for each $B\in \Xi$. Therefore, because $\mathsf{R}$ is a base, rule $\mathrm{\Gamma }/B$ is derivable from $\mathsf{R}$ for each $B\in \Xi$. Thus, each premise of rule $\Xi /▲$ is derivable from $\mathrm{\Gamma }$ and by transitivity of consequence relation, $\mathrm{\Gamma }/▲$ is derivable from $\mathsf{R},\Xi /▲$.

For relative bases one can take a set of conclusive rules $\mathsf{L}\cup \mathsf{R}$ and repeat the preceding argument. □

Corollary 8.

Suppose that $\mathsf{L}$ is a logic enjoying the $\mathsf{DP}$. Then, if $\mathsf{L}$ has a finite admissible base (relative base), then $\mathsf{L}$ has a finite admissible m-base (relative m-base).

Combining together Corollaries 7 and 8, we obtain the following.

Corollary 9.

A logic with the $\mathsf{DP}$ has a finite admissible base (relative base) if and only if it has a finite admissible m-base (relative m-base).

7. Some Applications

(1) Logics $\mathsf{K}4,\mathsf{K}4.1,\mathsf{S}4,\mathsf{S}4.1,\mathsf{Grz},\mathsf{Int},\mathrm{Dn},n\ge 1$ are a-decidable [9]. Hence, by Corollary 6, all these logics are am-decidable.

(2) Logics $\mathsf{Pos}$ and $\mathrm{Jhn}$ are a-decidable [25]; hence, by Corollary 6, these logics are am-decidable.

(3) A relative admissible base for conclusive rules for $\mathsf{Int}$ was established in [16]. Adding m-rules $p\vee q/p,q$ and $p,\neg p/▲$ to this relative base (or any relative base for this matter) gives us a relative m-base described in [26].

(4) It is known from [19] that Medvedev’s logic $\mathsf{ML}$ (which enjoys the $\mathsf{DP}$) is structurally complete. Hence, m-rules $p\vee q/p,q$ and $p,\neg p/▲$ form a relative to $\mathsf{ML}$ admissible m-base.

(5) Gabbay-de Jongh logics ${\mathsf{BB}}_{\mathfrak{n}},n>1$ enjoy the DP [27]. The relative m-bases for these logics have been constructed in [28] (Theorem 5.36):

$${\mathsf{r}}_n:=({\vee }_{i=1}^n(p_i\to p)\to {\vee }_{j=1}^n{p}_j)/{\vee }_{j=1}^n(({\vee }_{i=1}^n{p}_i\to p)\to p_j),\mathsf{de},\mathsf{t},$$

where $\mathsf{t}:=p,\neg p/▲$. By Theorem 4, ${\check{\mathsf{r}}}_n$ (or ${\mathsf{r}}_n^q$, because rules ${\mathsf{r}}_n$ are conclusive) gives a relative admissible base for ${\mathsf{BB}}_{\mathfrak{n}}$:

$$\check{\mathsf{r}}:=({\vee }_{i=1}^n(p_i\to p)\to {\vee }_{j=1}^n{p}_j)\vee q/{\vee }_{j=1}^n(({\vee }_{i=1}^n{p}_i\to p)\to p_j)\vee q.$$

Note that we did not include $\check{\mathsf{de}}$ and $\check{\mathsf{t}}$ because these rules are trivial:

$$\check{\mathsf{de}}=p_1\vee p_2\vee q/p_1\vee p_2\vee q\mathrm{and}\check{\mathsf{t}}=p\vee q,\neg p\vee q/q.$$