Finite Two-Dimensional Proof Systems for Non-finitely Axiomatizable Logics

Abstract

The characterizing properties of a proof-theoretical presentation of a given logic may hang on the choice of proof formalism, on the shape of the logical rules and of the sequents manipulated by a given proof system, on the underlying notion of consequence, and even on the expressiveness of its linguistic resources and on the logical framework into which it is embedded. Standard (one-dimensional) logics determined by (non-deterministic) logical matrices are known to be axiomatizable by analytic and possibly finite proof systems as soon as they turn out to satisfy a certain constraint of sufficient expressiveness. In this paper we introduce a recipe for cooking up a two-dimensional logical matrix (or B-matrix) by the combination of two (possibly partial) non-deterministic logical matrices. We will show that such a combination may result in B-matrices satisfying the property of sufficient expressiveness, even when the input matrices are not sufficiently expressive in isolation, and we will use this result to show that one-dimensional logics that are not finitely axiomatizable may inhabit finitely axiomatizable two-dimensional logics, becoming, thus, finitely axiomatizable by the addition of an extra dimension. We will illustrate the said construction using a well-known logic of formal inconsistency called mCi. We will first prove that this logic is not finitely axiomatizable by a one-dimensional (generalized) Hilbert-style system. Then, taking advantage of a known 5-valued non-deterministic logical matrix for this logic, we will combine it with another one, conveniently chosen so as to give rise to a B-matrix that is axiomatized by a two-dimensional Hilbert-style system that is both finite and analytic.

V. Greati acknowledges support from CAPES—Finance Code 001 and from the FWF project P 33548. J. Marcos acknowledges support from CNPq.

1 Introduction

A logic is commonly defined nowadays as a relation that connects collections of formulas from a formal language and satisfies some closure properties. The established connections are called consecutions and each of them has two parts, an antecedent and a succedent, the latter often being said to ‘follow from’ (or to be a consequence of) the former. A logic may be manufactured in a number of ways, in particular as being induced by the set of derivations justified by the rules of inference of a given proof system. There are different kinds of proof systems, the differences between them residing mainly in the shapes of their rules of inference and on the way derivations are built. We will be interested here in Hilbert-style proof systems (‘H-systems’, for short), whose rules of inference have the same shape of the consecutions of the logic they canonically induce and whose associated derivations consist in expanding a given antecedent by applications of rules of inference until the desired succedent is produced. A remarkable property of an H-system is that the logic induced by it is the least logic containing the rules of inference of the system; in the words of [24], the system constitutes a ‘logical basis’ for the said logic.

Conventional H-systems, which we here dub ‘Set-Fmla H-systems’, do not allow for more than one formula in the succedents of the consecutions that they manipulate. Since [23], however, we have learned that the simple elimination of this restriction on H-systems —that is, allowing for sets of formulas rather than single formulas in the succedents— brings numerous advantages, among which we mention: modularity (correspondence between rules of inference and properties satisfied by a semantical structure), analyticity (control over the resources demanded to produce a derivation), and the automatic generation of analytic proof systems for a wide class of logics specified by sufficiently expressive non-deterministics semantics, with an associated straightforward proof-search procedure [13, 18]. Such generalized systems, here dubbed ‘Set-Set H-systems’, induce logics whose consecutions involve succedents consisting in a collection of formulas, intuitively understood as ‘alternative conclusions’.

An H-system $\mathcal {H}$ is said to be an axiomatization for a given logic $\mathcal {L}$ when the logic induced by $\mathcal {H}$ coincides with $\mathcal {L}$. A desirable property for an axiomatization is finiteness, namely the property of consisting on a finite collection of schematic axioms and rules of inference. A logic having a finite axiomatization is said to be ‘finitely based’. In the literature, one may find examples of logics having a quite simple, finite semantic presentation, being, in contrast, not finitely based in terms of Set-Fmla H-systems [21]. These very logics, however, when seen as companions of logics with multiple formulas in the succedent, turn out to be finitely based in terms of Set-Set H-systems [18]. In other words, by updating the underlying proof-theoretical and the logical formalisms, we are able to obtain a finite axiomatization for logics which in a more restricted setting could not be said to be finitely based. We may compare the above mentioned movement to the common mathematical practice of adding dimensions in order to provide better insight on some phenomenon. A well-known example of that is given by the Fundamental Theorem of Algebra, which provides an elegant solution to the problem of determining the roots of polynomials over a single variable, demanding only that real coefficients should be replaced by complex coefficients. Another example, from Machine Learning, is the ‘kernel trick’ employed in support vector machines: by increasing the dimensionality of the input space, the transformed data points become more easily separable by hyperplanes, making it possible to achieve better results in classification tasks.

It is worth noting that there are logics that fail to be finitely based in terms of Set-Set H-systems. An example of a logic designed with the sole purpose of illustrating this possibility was provided in [18]. One of the goals of the present work is to show that an important logic from the literature of logics of formal inconsistency (LFIs) called mCi is also an example of this phenomenon. This logic results from adding infinitely-many axiom schemas to the logic mbC, a logic that is obtained by extending positive classical logic with two axiom schemas. Incidentally, along the proof of this result, we will show that mCi is the limit of a strictly increasing chain of LFIs extending mbC (comparable to the case of $\mathcal {C}_{\mathrm {Lim}}$ in da Costa’s hierarchy of increasingly weaker paraconsistent calculi [16]). A natural question, then, is whether we can enrich our technology, in the same vein, in order to provide finite axiomatizations for all these logics. We answer that in the affirmative by means of the two-dimensional frameworks developed in [11, 17]. Logics, in this case, connect pairs of collections of formulas. A consecution, in this setting, may be read as involving formulas that are accepted and those that are not, as well as formulas that are rejected and those that are not. ‘Acceptance’ and ‘rejection’ are seen, thus, as two orthogonal dimensions that may interact, making it possible, thus, to express more complex consecutions than those expressible in one-dimensional logics. Two-dimensional H-systems, which we call ‘$\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$ H-systems’, generalize Set-Set H-systems so as to manipulate pairs of collections of formulas, canonically inducing two-dimensional logics and constituting logical bases for them. Another goal of the present work is, therefore, to show how to obtain a two-dimensional logic inhabited by a (possibly not finitely based) one-dimensional logic of interest. More than that, the logic we obtain will be finitely axiomatizable in terms of a $\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$ analytic H-system. The only requirements is that the one-dimensional logic of interest must have an associated semantics in terms of a finite non-deterministic logical matrix and that this matrix can be combined with another one through a novel procedure that we will introduce, resulting in a two-dimensional non-deterministic matrix (a B-matrix [9]) satisfying a certain condition of sufficient expressiveness [17]. An application of this approach will be provided here in order to produce the first finite and analytic axiomatization of mCi.

The paper is organized as follows: Sect. 2 introduces basic terminology and definitions regarding algebras and languages. Section 3 presents the notions of one-dimensional logics and Set-Set H-systems. Section 4 proves that mCi is not finitely axiomatizable by one-dimensional H-systems. Section 5 introduces two-dimensional logics and H-systems, and describes the approach to extending a logical matrix to a B-matrix with the goal of finding a finite two-dimensional axiomatization for the logic associated with the former. Section 6 presents a two-dimensional finite analytic H-system for mCi. In the final remarks, we highlight some byproducts of our present approach and some features of the resulting proof systems, in addition to pointing to some directions for further research.¹

2 Preliminaries

A propositional signature is a family $\varSigma :=\{{\varSigma }_{k}\}_{k\in \omega }$, where each ${\varSigma }_{k}$ is a collection of $k$-ary connectives. We say that $\varSigma$ is finite when its base set $\bigcup _{k\in \omega }{\varSigma }_{k}$ is finite. A non-deterministic algebra over $\varSigma$, or simply $\varSigma$ -nd-algebra, is a structure $\mathbf {A}:=\left\langle A, {\cdot }_{\mathbf {A}} \right\rangle$, such that $A$ is a non-empty collection of values called the carrier of $\mathbf {A}$, and, for each $k\in \omega$ and ${\copyright }\in {\varSigma }_{k}$, the multifunction ${ {\copyright }}_{\mathbf {A}} : A^k\rightarrow \mathcal {P}(A)$ is the interpretation of ${\copyright }$ in $\mathbf {A}$. When $\varSigma$ and $A$ are finite, we say that $\mathbf {A}$ is finite. When the range of all interpretations of $\mathbf {A}$ contains only singletons, $\mathbf {A}$ is said to be a deterministic algebra over $\varSigma$, or simply a $\varSigma$ -algebra, meeting the usual definition from Universal Algebra [12]. When $\varnothing$ is not in the range of each ${ {\copyright }}_{\mathbf {A}}$, $\mathbf {A}$ is said to be total. Given a $\varSigma$-algebra $\mathbf {A}$ and a ${\copyright }\in {\varSigma }_{1}$, we let ${ {\copyright }}_{\mathbf {A}}^0(x) :=x$ and ${ {\copyright }}_{\mathbf {A}}^{i+1}(x) :={ {\copyright }}_{\mathbf {A}}({ {\copyright }}_{\mathbf {A}}^i(x))$. A mapping $v: A\rightarrow B$ is a homomorphism from $\mathbf {A}$ to $\mathbf {B}$ when, for all $k\in \omega$, ${\copyright }\in {\varSigma }_{k}$ and $x_1,\ldots ,x_k \in A$, we have $f[{ {\copyright }}_{\mathbf {A}}(x_1,\ldots ,x_k)] \subseteq { {\copyright }}_{\mathbf {B}}(f(x_1),\ldots ,f(x_k))$. The set of all homomorphisms from $\mathbf {A}$ to $\mathbf {B}$ is denoted by $\mathsf {Hom}_{\varSigma }(\mathbf {A},\mathbf {B})$. When $\mathbf {B}= \mathbf {A}$, we write $\mathsf {End}_{\varSigma }(\mathbf {A})$, rather than $\mathsf {Hom}_{\varSigma }(\mathbf {A},\mathbf {A})$, for the set of endomorphisms on $\mathbf {A}$.

Let $P$ be a denumerable collection of $propositional\ variables$ and $\varSigma$ be a propositional signature. The absolutely free $\varSigma$-algebra freely generated by $P$ is denoted by $\mathbf {L}_{\varSigma }(P)$ and called the $\varSigma$ -language generated by $P$. The elements of $L_{\varSigma }(P)$ are called $\varSigma$ -formulas, and those among them that are not propositional variables are called $\varSigma$-compounds. Given $\varPhi \subseteq L_{\varSigma }(P)$, we denote by $\varPhi ^{\mathsf {c}}$ the set ${L_{\varSigma }(P)}{\setminus }{\varPhi }$. The homomorphisms from $\mathbf {L}_{\varSigma }(P)$ to $\mathbf {A}$ are called valuations on $\mathbf {A}$, and we denote by $\mathsf {Val}_{\varSigma }(\mathbf {A})$ the collection thereof. Additionally, endomorphisms on $\mathbf {L}_{\varSigma }(P)$ are dubbed $\varSigma$-substitutions, and we let $\mathsf {Subs}_{\varSigma }^{P} :=\mathsf {End}_{\varSigma }(\mathbf {L}_{\varSigma }(P))$; when there is no risk of confusion, we may omit the superscript from this notation.

Given $\varphi \in L_{\varSigma }(P)$, let $\mathsf {props}(\varphi )$ be the set of propositional variables occurring in $\varphi$. If $\mathsf {props}(\varphi ) = \{p_1,\ldots ,p_k\}$, we say that $\varphi$ is $k$-ary (unary, for $k=1$; binary, for $k=2$) and let ${\varphi }_{\mathbf {A}} : A^k\rightarrow \mathcal {P}(A)$ be the $k$ -ary multifunction on $\mathbf {A}$ induced by $\varphi$, where, for all $x_1,\ldots ,x_k \in A$, we have ${\varphi }_{\mathbf {A}}(x_1,\ldots ,x_k) :=\{v(\varphi ) \mid v\in \mathsf {Val}_{\varSigma }(\mathbf {A}) \text { and } v(p_i) = x_i, \text { for } 1 \le i \le k\}$. Moreover, given $\psi _1,\ldots ,\psi _k \in L_{\varSigma }(P)$, we write $\varphi (\psi _1,\ldots ,\psi _k)$ for the $\varSigma$-formula ${\varphi }_{\mathbf {L}_{\varSigma }(P)}(\psi _1,\ldots ,\psi _k)$, and, where $\varPhi \subseteq L_{\varSigma }(P)$ is a set of $k$-ary $\varSigma$-formulas, we let $\varPhi (\psi _1,\ldots ,\psi _k) :=\{\varphi (\psi _1,\ldots ,\psi _k) \mid \varphi \in \varPhi \}$. Given $\varphi \in L_{\varSigma }(P)$, by $\mathsf {subf}(\varphi )$ we refer to the set of subformulas of $\varphi$. Where $\theta$ is a unary $\varSigma$-formula, we define the set $\mathsf {subf}^{\theta }(\varphi )$ as $\{\sigma (\theta )\mid \sigma ~:~P\rightarrow \mathsf {subf}(\varphi )\}$. Given a set $\varTheta \supseteq \{p\}$ of unary $\varSigma$-formulas, we set $\mathsf {subf}^{\varTheta }(\varphi ) :=\bigcup _{\theta \in \varTheta }\mathsf {subf}^{\theta }(\varphi )$. For example, if $\varTheta = \{p,{\lnot }p\}$, we will have $\mathsf {subf}^{\varTheta }({\lnot }(q\vee r)) = \{q,r,q\vee r,{\lnot }(q\vee r)\}\cup \{ {\lnot }q,{\lnot }r,{\lnot }(q\vee r),{\lnot }{\lnot }(q\vee r)\}$. Such generalized notion of subformulas will be used in the next section to provide a more generous proof-theoretical concept of analyticity.

3 One-Dimensional Consequence Relations

A Set-Set statement (or sequent) is a pair $(\varPhi ,\varPsi ) \in \mathcal {P}(L_{\varSigma }(P)) \times \mathcal {P}(L_{\varSigma }(P))$, where $\varPhi$ is dubbed the antecedent and $\varPsi$ the succedent. A one-dimensional consequence relation on $L_{\varSigma }(P)$ is a collection  of Set-Set statements satisfying, for all $\varPhi ,\varPsi ,\varPhi ^\prime ,\varPsi ^\prime \subseteq L_{\varSigma }(P)$,

• (O) if $\varPhi \cap \varPsi \ne \varnothing$, then

• (D) if , then

• (C) if for all $\varPi \subseteq L_{\varSigma }(P)$, then

Properties (O), (D) and (C) are called overlap, dilution and cut, respectively. The relation is called substitution-invariant when it satisfies, for every $\sigma \in \mathsf {Subs}_{\varSigma }^{}$,

• (S) if , then

and it is called finitary when it satisfies

• (F) if , then for some finite ${\varPhi }^{\mathrm f} \subseteq \varPhi$ and ${\varPsi }^{\mathrm f} \subseteq \varPsi$

One-dimensional consequence relations will also be referred to as one-dimensional logics. Substitution-invariant finitary one-dimensional logics will be called standard. We will denote by $\blacktriangleright _{}^{}$ the complement of $\rhd _{}^{}$, called the compatibility relation associated with $\rhd _{}^{}$ [10].

A Set-Fmla statement is a sequent having a single formula as consequent. When we restrict standard consequence relations to collections of Set-Fmla statements, we define the so-called (substitution-invariant finitary) Tarskian consequence relations. Every one-dimensional consequence relation $\rhd _{}^{}$ determines a Tarskian consequence relation , dubbed the Set-Fmla Tarskian companion of $\rhd _{}^{}$, such that, for all $\varPhi \cup \{\psi \} \subseteq L_{\varSigma }(P)$, if, and only if, $\varPhi \rhd _{}^{} \{\psi \}$. It is well-known that the collection of all Tarskian consequence relations over a fixed language constitutes a complete lattice under set-theoretical inclusion [25]. Given a set C of such relations, we will denote by $\bigsqcup C$ its supremum in the latter lattice.

We present in what follows two ways of obtaining one-dimensional consequence relations: one semantical, via non-deterministic logical matrices [6], and the other proof-theoretical, via Set-Set Hilbert-style systems [18, 23].

A non-deterministic $\varSigma$-matrix, or simply $\varSigma$-nd-matrix, is a structure $\mathbb {M}:=\left\langle \mathbf {A},D \right\rangle$, where $\mathbf {A}$ is a $\varSigma$-nd-algebra, whose carrier is the set of truth-values, and $D\subseteq A$ is the set of designated truth-values. Such structures are also known in the literature as ‘PNmatrices’ [7]; they generalize the so-called ‘Nmatrices’ [5], which are $\varSigma$-nd-matrices with the restriction that $\mathbf {A}$ must be total. From now on, whenever $X\subseteq A$, we denote ${A}{\setminus }{X}$ by $\overline{X}$. In case $\mathbf {A}$ is deterministic, we simply say that $\mathbb {M}$ is a $\varSigma$ -matrix. Also, $\mathbb {M}$ is said to be finite when $\mathbf {A}$ is finite. Every $\varSigma$-nd-matrix $\mathbb {M}$ determines a substitution-invariant one-dimensional consequence relation over $\varSigma$, denoted by $\rhd _{\mathbb {M}}^{}{}$, such that $\varPhi \rhd _{\mathbb {M}}^{}{} \varPsi \text { if, and only if, for all } v\in \mathsf {Val}_{\varSigma }(\mathbf {A}), v[\varPhi ]~\cap ~\overline{D} \ne \varnothing \text { or } v[\varPsi ] \cap D\ne \varnothing .$

It is worth noting that $\rhd _{\mathbb {M}}^{}{}$ is finitary whenever the carrier of $\mathbf {A}$ is finite (the proof runs very similar to that of the same result for Nmatrices [5, Theorem 3.15]).

A strong homomorphism between $\varSigma$-matrices $\mathbb {M}_1 :=\left\langle \mathbf {A}_1,D_1 \right\rangle$ and $\mathbb {M}_2 :=\left\langle \mathbf {A}_2, D_2 \right\rangle$ is a homomorphism h between $\mathbf {A}_1$ and $\mathbf {A}_2$ such that $x\in D_1$ if, and only if, $h(x) \in D_2$. When there is a surjective strong homomorphism between $\mathbb {M}_1$ and $\mathbb {M}_2$, we have that .

Now, to the Hilbert-style systems. A (schematic) Set-Set rule of inference $R_\mathsf s$ is the collection of all substitution instances of the Set-Set statement $\mathsf s$, called the schema of $R_\mathsf s$. Each $r\in R_\mathsf s$ is called a rule instance of $R_\mathsf s$. A (schematic) Set-Set H-system $\mathsf {R}$ is a collection of Set-Set rules of inference. When we constrain the rule instances of $\mathsf {R}$ to having only singletons as succedents, we obtain the conventional notion of Hilbert-style system, called here Set-Fmla H-system.

An $\mathsf {R}$-derivation in a Set-Set H-system $\mathsf {R}$ is a rooted directed tree $\mathsf t$ such that every node is labelled with sets of formulas or with a discontinuation symbol $*$, and in which every non-leaf node (that is, a node with child nodes) $\mathsf n$ in $t$ is an expansion of $\mathsf n$ by a rule instance $r$ of $\mathsf {R}$. This means that the antecedent of $r$ is contained in the label of $\mathsf n$ and that $\mathsf n$ has exactly one child node for each formula $\psi$ in the succedent of $r$. These child nodes are, in turn, labelled with the same formulas as those of $\mathsf n$ plus the respective formula $\psi$. In case $r$ has an empty succedent, then $\mathsf n$ has a single child node labelled with $*$. Here we will consider only finitary Set-Set H-systems, in which each rule instance has finite antecedent and succedent. In such cases, we only need to consider finite derivations. Figure 1 illustrates how derivations using only finitary rules of inference may be graphically represented. We denote by $\ell ^{\,\mathsf t}(\mathsf n)$ the label of the node $\mathsf n$ in the tree $\mathsf t$. It is worth observing that, for Set-Fmla H-systems, derivations are linear trees (as rule instances have a single formula in their succedents), or, in other words, just sequences of formulas built by applications of the rule instances, matching thus the conventional definition of Hilbert-style systems.

Fig. 1.

Graphical representation of $\mathsf {R}$-derivations, for $\mathsf {R}$ finitary. The dashed edges and blank circles represent other branches that may exist in the derivation. We usually omit the formulas inherited from the parent node, exhibiting only the ones introduced by the applied rule of inference. In both cases, we must have $\varGamma \subseteq \varPhi$ to enable the application of the rule.

A node $\mathsf n$ of an $\mathsf {R}$-derivation $\mathsf t$ is called $\varDelta$ -closed in case it is a leaf node with $\ell ^{\,\mathsf t}(\mathsf n) = *$ or $\ell ^{\,\mathsf t}(\mathsf n) \cap \varDelta \ne \varnothing$. A branch of $\mathsf t$ is $\varDelta$-closed when it ends in a $\varDelta$-closed node. When every branch in $\mathsf t$ is $\varDelta$-closed, we say that $\mathsf {R}$ is itself $\varDelta$ -closed. An $\mathsf {R}$ -proof of a Set-Set statement $(\varPhi ,\varPsi )$ is a $\varPsi$-closed $\mathsf {R}$-derivation $\mathsf t$ such that $\ell ^{\,\mathsf t}(\mathsf {rt}(\mathsf t)) \subseteq \varPhi$.

Consider the binary relation $\rhd _{\mathsf {R}}^{}$ on $\mathcal {P}(L_{\varSigma }(P))$ such that $\varPhi \rhd _{\mathsf {R}}^{} \varPsi$ if, and only if, there is an $\mathsf {R}$-proof of $(\varPhi ,\varPsi )$. This relation is the smallest substitution-invariant one-dimensional consequence relation containing the rules of inference of $\mathsf {R}$, and it is finitary when $\mathsf {R}$ is finitary. Since Set-Set (and Set-Fmla) H-systems canonically induce one-dimensional consequence relations, we may refer to them as one-dimensional H-systems or one-dimensional axiomatizations. In case there is a proof of $(\varPhi ,\varPsi )$ whose nodes are labelled only with subsets of $\mathsf {subf}^{\varTheta }[\varPhi \cup \varPsi ]$, we write $\varPhi \rhd _{\mathsf {R}}^{\varTheta } \varPsi$ . In case $\rhd _{\mathsf {R}}^{} = \rhd _{\mathsf {R}}^{\varTheta }$, we say that $\mathsf {R}$ is $\varTheta$-analytic. Note that the ordinary notion of analyticity obtains when $\varTheta = \{p\}$. From now on, whenever we use the word “analytic” we will mean this extended notion of $\varTheta$-analyticity, for some $\varTheta$ implicit in the context. When the $\varTheta$ happens to be important for us or we identify any risk of confusion, we will mention it explicitly.

In [13], based on the seminal results on axiomatizability via Set-Set H-systems by Shoesmith and Smiley [23], it was proved that any non-deterministic logical matrix $\mathbb {M}$ satisfying a criterion of sufficient expressiveness is axiomatizable by a $\varTheta$-analytic Set-Set Hilbert-style system, which is finite whenever $\mathbb {M}$ is finite, where $\varTheta$ is the set of separators for the pairs of truth-values of $\mathbb {M}$. According to such criterion, an nd-matrix is sufficiently expressive when, for every pair $(x,y)$ of distinct truth-values, there is a unary formula $\mathrm S$, called a separator for $(x,y)$, such that ${\mathrm S}_{\mathbf {A}}(x) \subseteq D$ and ${\mathrm S}_{\mathbf {A}}(y) \subseteq \overline{D}$, or vice-versa; in other words, when every pair of distinct truth-values is separable in $\mathbb {M}$.

We emphasize that it is essential for the above result the adoption of Set-Set H-systems, instead of the more restricted Set-Fmla H-systems. In fact, while two-valued matrices may always be finitely axiomatized by Set-Fmla H-systems [22], there are sufficiently expressive three-valued deterministic matrices [21] and even quite simple two-valued non-deterministic matrices [19] that fail to be finitely axiomatized by Set-Fmla H-systems. When the nd-matrix at hand is not sufficiently expressive, we may observe the same phenomenon of not having a finite axiomatization also in terms of Set-Set H-systems, even if the said nd-matrix is finite. The first example (and, to the best of our knowledge, the only one in the current literature) of this fact appeared in [13], which we reproduce here for later reference:

Example 1

Consider the signature $\varSigma :=\{{\varSigma }_{k}\}_{k\in \omega }$ such that $\varSigma _1 :=\{g, h\}$ and $\varSigma _k :=\varnothing$ for all $k \ne 1$. Let $\mathbb {M}:=\left\langle \mathbf {A}, \{\mathbf {a}\} \right\rangle$ be a $\varSigma$-nd-matrix, with $A:=\{\mathbf {a},\mathbf {b},\mathbf {c}\}$ and

$$\begin{aligned} {g}_{\mathbf {A}}(x) = {\left\{ \begin{array}{ll} \{\mathbf {a}\}, &{} \text {if } x= \mathbf {c}\\ A, &{} \text {otherwise}\\ \end{array}\right. } \quad {h}_{\mathbf {A}}(x) = {\left\{ \begin{array}{ll} \{\mathbf {b}\}, &{} \text {if } x= \mathbf {b}\\ A, &{} \text {otherwise}\\ \end{array}\right. } \end{aligned}$$

This matrix is not sufficiently expressive because there is no separator for the pair $(\mathbf {b},\mathbf {c})$, and [13] proved that it is not axiomatizable by a finite Set-Set H-system, even though an infinite Set-Set system that captures it has a quite simple description in terms of the following infinite collection of schemas:

$$\begin{aligned} \frac{h^i(p)}{p, g(p)}, \text { for all}\, i \in \omega . \end{aligned}$$

In the next section, we reveal another example of this same phenomenon, this time of the known LFI [14] called mCi. In the path of proving that this logic is not axiomatizable by a finite Set-Set H-system, we will show that there are infinitely many LFIs between mbC and mCi, organized in a strictly increasing chain whose limit is mCi itself.

Before continuing, it is worth emphasizing that any given non-sufficiently expressive nd-matrix may be conservatively extended to a sufficiently expressive nd-matrix provided new connectives are added to the language [18]. These new connectives have the sole purpose of separating the pairs of truth-values for which no separator is available in the original language. The Set-Set system produced from this extended nd-matrix can, then, be used to reason over the original logic, since the extension is conservative. However, these new connectives, which a priori have no meaning, are very likely to appear in derivations of consecutions of the original logic. This might not look like an attractive option to inferentialists who believe that purity of the schematic rules governing a given logical constant is essential for the meaning of the latter to be coherently fixed. In the subsequent sections, we will introduce and apply a potentially more expressive notion of logic in order to provide a finite and analytic H-system for logics that are not finitely axiomatizable in one dimension, while preserving their original languages.

4 The Logic mCi is Not Finitely Axiomatizable

A one-dimensional logic $\rhd _{}^{}$ over $\varSigma$ is said to be ${\lnot }$-paraconsistent when we have $p,{\lnot }p\;\blacktriangleright _{}^{}\; q$, for $p,q\in P$. Moreover, $\rhd _{}^{}$ is ${\lnot }$-gently explosive in case there is a collection $\bigcirc (p) \subseteq L_{\varSigma }(P)$ of unary formulas such that, for some $\varphi \in L_{\varSigma }(P)$, we have $\bigcirc (\varphi ), \varphi \blacktriangleright _{}^{} \varnothing$; $\bigcirc (\varphi ), {\lnot }\varphi \blacktriangleright _{}^{} \varnothing$, and, for all $\varphi \in L_{\varSigma }(P)$, $\bigcirc (\varphi ),\varphi ,{\lnot }\varphi \; \rhd _{}^{} \varnothing$. We say that $\rhd _{}^{}$ is a logic of formal inconsistency (LFI) in case it is ${\lnot }$-paraconsistent yet ${\lnot }$-gently explosive. In case $\bigcirc (p) = \{{\circ }p\}$, for ${\circ }$ a (primitive or composite) consistency connective, the logic is said also to be a C-system. In what follows, let $\varSigma ^{{\circ }}$ be the propositional signature such that $\varSigma ^{{\circ }}_{1} :=\{{\lnot },{\circ }\}$, $\varSigma ^{{\circ }}_{2} :=\{\wedge ,\vee ,{\,\supset \,}\}$, and $\varSigma ^{{\circ }}_{k} :=\varnothing$ for all $k \not \in \{1,2\}$.

One of the simplest C-systems is the logic mbC, which was first presented in terms of a Set-Fmla H-system over $\varSigma ^{{\circ }}$ obtained by extending any Set-Fmla H-system for positive classical logic (${\textbf {CPL}}^{+}$) with the following pair of axiom schemas:

• $(\mathsf {em})$ $p\vee {\lnot }p$

• $(\mathsf {bc1})$ ${\circ }p{\,\supset \,}(p{\,\supset \,}({\lnot }p{\,\supset \,}q))$

The logic mCi, in turn, is the C-system resulting from extending the H-system for mbC with the following (infinitely many) axiom schemas [20] (the resulting Set-Fmla H-system is denoted here by $\mathcal {H}_{{\textbf {mCi }}}$):

• $(\mathsf {ci})$ ${\lnot }{\circ }p{\,\supset \,}(p\wedge {\lnot }p)$

• $(\mathsf {ci})$ $_j$ ${\circ }{\lnot }^j{\circ }p$ (for all $0 \le j < \omega$)

A unary connective ${\copyright }$ is said to constitute a classical negation in a one-dimensional logic $\rhd _{}^{}$ extending ${\textbf {CPL}}^{+}{}$ in case, for all $\varphi ,\psi \in L_{\varSigma }(P)$, $\varnothing \rhd _{}^{} \varphi \vee {\copyright }(\varphi )$ and $\varnothing \rhd _{}^{} \varphi {\,\supset \,}( {\copyright }(\varphi ) {\,\supset \,}\psi )$. One of the main differences between mCi and mbC is that an inconsistency connective $\bullet$ may be defined in the former using the paraconsistent negation, instead of a classical negation, by setting $\bullet \varphi :={\lnot }{\circ }\varphi$ [20].

Both logics above were presented in [15] in ways other than H-systems: via tableau systems, via bivaluation semantics and via possible-translations semantics. In addition, while these logics are known not to be characterizable by a single finite deterministic matrix [20], a characteristic nd-matrix is available for mbC [1] and a 5-valued non-deterministic logical matrix is available for mCi [2], witnessing the importance of non-deterministic semantics in the study of non-classical logics. Such characterizations, moreover, allow for the extraction of sequent-style systems for these logics by the methodologies developed in [3, 4]. Since mCi’s 5-valued nd-matrix will be useful for us in future sections, we recall it below for ease of reference.

Definition 1

Let $\mathcal {V}_5:=\{f,F, I, T, t\}$ and ${\mathsf {Y}}_{5}:=\{I, T, t\}$. Define the $\varSigma ^{{\circ }}$-matrix $\mathbb {M}_{{\textbf {mCi }}}:=\left\langle \mathbf {A}_{5}, {\mathsf {Y}}_{5} \right\rangle$ such that $\mathbf {A}_{5}:=\left\langle \mathcal {V}_5, {\cdot }_{\mathbf {A}_{5}} \right\rangle$ interprets the connectives of $\varSigma ^{{\circ }}$ according to the following:

One might be tempted to apply the axiomatization algorithm of [13] to the finite non-deterministic logical matrix defined above to obtain a finite and analytic Set-Set system for mCi. However, it is not obvious, at first, whether this matrix is sufficiently expressive or not (we will, in fact, prove that it is not). In what follows, we will show now mCi is actually axiomatizable neither by a finite Set-Fmla H-system (first part), nor by a finite Set-Set H-system (second part); it so happens, thus, that it was not by chance that $\mathcal {H}_{{\textbf {mCi }}}$ has been originally presented with infinitely many rule schemas. For the first part, we rely on the following general result:

Theorem 1

([25], Theorem 2.2.8, adapted). Let be a standard Tarskian consequence relation. Then is axiomatizable by a finite Set-Fmla H-system if, and only if, there is no strictly increasing sequence of standard Tarskian consequence relations such that .

In order to apply the above theorem, we first present a family of finite Set-Fmla H-systems that, in the sequel, will be used to provide an increasing sequence of standard Tarskian consequence relations whose supremum is precisely mCi. Next, we show that this sequence is stricly increasing, by employing the matrix methodology traditionally used for showing the independence of axioms in a proof system.

Definition 2

For each $k \in \omega$, let $\mathcal {H}_{{\textbf {mCi }}}^k$ be a Set-Fmla H-system for positive classical logic together with the schemas (em), (bc1), (ci) and (ci)$_j$, for all $0 \le j \le k$.

Since $\mathcal {H}_{{\textbf {mCi }}}^k$ may be obtained from $\mathcal {H}_{{\textbf {mCi }}}$ by deleting some (infinitely many) axioms, it is immediate that:

Proposition 1

For every $k \in \omega$, .

The way we define the promised increasing sequence of consequence relations in the next result is by taking the systems $\mathcal {H}_{{\textbf {mCi }}}^{k}$ with odd superscripts, namely, we will be working with the sequence Excluding the cases where k is even will facilitate, in particular, the proof of Lemma 3.

Lemma 1

For each $1 \le k < \omega$, let . Then  , and

Finally, we prove that the sequence outlined in the paragraph before Lemma 1 is strictly increasing. In order to achieve this, we define, for each $1 \le k < \omega$, a $\varSigma ^{{\circ }}$-matrix $\mathbb {M}_k$ and prove that $\mathcal {H}_{{\textbf {mCi }}}^{2k-1}$ is sound with respect to such matrix. Then, in the second part of the proof (the “independence part”), we show that, for each $1 \le k < \omega$, $\mathbb {M}_k$ fails to validate the rule schema (ci)$_j$, for $j = 2k$, which is present in $\mathcal {H}_{{\textbf {mCi }}}^{2(k+1)-1}$. In this way, by the contrapositive of the soundness result proved in the first part, we will have (ci)$_j$ provable in $\mathcal {H}_{{\textbf {mCi }}}^{2(k+1)-1}$ while unprovable in $\mathcal {H}_{{\textbf {mCi }}}^{2k-1}$. In what follows, for any $k \in \omega$, we use ${k}^{*}$ to refer to the successor of k.

Definition 3

Let $1 \le k < \omega$. Define the $2{k}^{*}$-valued $\varSigma ^{{\circ }}$-matrix $\mathbb {M}_{k} :=\left\langle \mathbf {A}_k, D_k \right\rangle$ such that $D_k :=\{{k}^{*} + 1, \ldots , 2{k}^{*}\}$ and $\mathbf {A}_k :=\left\langle \{1,\ldots ,2{k}^{*}\}, {\cdot }_{\mathbf {A}_k} \right\rangle$, the interpretation of $\varSigma ^{{\circ }}$ in $\mathbf {A}_k$ given by the following operations:

Before continuing, we state results concerning this construction, which will be used in the remainder of the current line of argumentation. In what follows, when there is no risk of confusion, we omit the subscript ‘$\mathbf {A}_k$’ from the interpretations to simplify the notation.

Lemma 2

For all $k \ge 1$ and $1 \le m \le 2k$,

$$ {{\lnot }}_{\mathbf {A}_k}^m({k}^{*}+1) = {\left\{ \begin{array}{ll} ({k}^{*}+1)+\frac{m}{2}, &{} \text {if } m \text { is even}\\ 1 +\frac{m+1}{2}, &{} otherwise\\ \end{array}\right. } $$

Lemma 3

For all $1 \le k < \omega$, we have but .

Finally, Theorem 1, Lemma 1 and Lemma 3 give us the main result:

Theorem 2

mCi is not axiomatizable by a finite Set-Fmla H-system.

For the second part —namely, that no finite Set-Set H-system axiomatizes mCi—, we make use of the following result:

Theorem 3

([23], Theorem 5.37, adapted). Let be a one-dimensional consequence relation over a propositional signature containing the binary connective $\vee$. Suppose that the Set-Fmla Tarskian companion of , denoted by , satisfies the following property:

If a Set-Set H-system $\mathsf {R}$ axiomatizes , then $\mathsf {R}$ may be converted into a Set-Fmla H-system for that is finite whenever $\mathsf {R}$ is finite.

It turns out that:

Lemma 4

mCi satisfies (Disj).

Proof

The non-deterministic semantics of mCi gives us that, for all $\varphi ,\psi \in L_{\varSigma ^{{\circ }}}(P)$, ; , and , and such facts easily imply (Disj).

Theorem 4

mCi is not axiomatizable by a finite Set-Set H-system.

Proof

If $\mathsf {R}$ were a finite Set-Set H-system for mCi, then, by Lemma 4 and Theorem 3, it could be turned into a finite Set-Fmla H-system for this very logic. This would contradict Theorem 2.

Finding a finite one-dimensional H-system for mCi (analytic or not) over the same language, then, proved to be impossible. The previous result also tells us that there is no sufficiently expressive non-deterministic matrix that characterizes mCi (for otherwise the recipe in [13] would deliver a finite analytic Set-Set H-system for it), and we may conclude, in particular, that:

Corollary 1

The nd-matrix $\mathbb {M}_{{\textbf {mCi }}}$ is not sufficiently expressive.

The pairs of truth-values of $\mathbb {M}_{{\textbf {mCi }}}$ that seem not to be separable (at least one of these pairs must not be, in view of the above corollary) are $(t,T)$ and $(f,F)$. The insufficiency of expressive power to take these specific pairs of values apart, however, would be circumvented if we had considered instead the matrix defined below, obtained from $\mathbb {M}_{{\textbf {mCi }}}$ by changing its set of designated values:

Definition 4

Let $\mathbb {M}_{{\textbf {mCi }}}^{\mathsf {n}}:=\left\langle \mathbf {A}_{5}, {\mathsf {N}}_{5} \right\rangle$, where ${\mathsf {N}}_{5}:=\{f, I, T\}$.

Note that, in $\mathbb {M}_{{\textbf {mCi }}}^{\mathsf {n}}$, we have $t\not \in {\mathsf {N}}_{5}$, while $T\in {\mathsf {N}}_{5}$, and we have that $f\in {\mathsf {N}}_{5}$, while $F\not \in {\mathsf {N}}_{5}$. Therefore, the single propositional variable $p$ separates in $\mathbb {M}_{{\textbf {mCi }}}^{\mathsf {n}}$ the pairs $(t,T)$ and $(f,F)$. On the other hand, it is not clear now whether the pairs $(t,F)$ and $(f,T)$ are separable in this new matrix. Nonetheless, we will see, in the next section, how we can take advantage of the semantics of non-deterministic B-matrices in order to combine the expressiveness of $\mathbb {M}_{{\textbf {mCi }}}$ and $\mathbb {M}_{{\textbf {mCi }}}^{\mathsf {n}}$ in a very simple and intuitive manner, preserving the language and the algebra shared by these matrices. The notion of logic induced by the resulting structure will not be one-dimensional, as the one presented before, but rather two-dimensional, in a sense we shall detail in a moment. We identify two important aspects of this combination: first, the logics determined by the original matrices can be fully recovered from the combined logic; and, second, since the notions of H-systems and sufficient expressiveness, as well as the axiomatization algorithm of [13], were generalized in [17], the resulting two-dimensional logic may be algorithmically axiomatized by an analytic two-dimensional H-system that is finite if the combining matrices are finite, provided the criterion of sufficient expressiveness is satisfied after the combination. This will be the case, in particular, when we combine $\mathbb {M}_{{\textbf {mCi }}}$ and $\mathbb {M}_{{\textbf {mCi }}}^{\mathsf {n}}$. Consequently, this novel way of combining logics provides a quite general approach for producing finite and analytic axiomatizations for logics determined by non-deterministic logical matrices that fail to be finitely axiomatizable in one dimension; this includes the logics from Example 1, and also mCi.

5 Two-Dimensional Logics

From now on, we will employ the symbols ${\mathsf {Y}}$, , ${\mathsf {N}}$ and to informally refer to, respectively, the cognitive attitudes of acceptance, non-acceptance, rejection and non-rejection, collected in the set . Given a set $\varPhi \subseteq L_{\varSigma }(P)$, we will write $\varPhi _{\alpha }$ to intuitively mean that a given agent entertains the cognitive attitude $\alpha \in \mathsf {Atts}$ with respect to the formulas in $\varPhi$, that is: the formulas in $\varPhi _{\mathsf {Y}}$ will be understood as being accepted by the agent; the ones in , as non-accepted; the ones in $\varPhi _{\mathsf {N}}$, as rejected; and the ones in , as non-rejected. Where $\alpha \in \mathsf {Atts}$, we let $\tilde{\alpha }$ be its flipped version, that is, , , and .

We refer to each as a B -statement, where $(\varPhi _{{\mathsf {Y}}},\varPhi _{\mathsf {N}})$ is the antecedent and is the succedent. The sets in the latter pairs are called components. A B -consequence relation is a collection of B-statements satisfying:

• (O2) if or , then

• (D2) if and ${\varPsi }_{\alpha } \subseteq {\varPhi }_{\alpha }$ for every $\alpha \in \mathsf {Atts}$, then

• (C2) if for all and , then

A B-consequence relation is called substitution-invariant if, in addition, holds whenever, for every $\sigma \in \mathsf {Subs}_{\varSigma }^{}$:

• (S2) and ${\varPhi }_{\alpha } = {\sigma }({\varPsi }_{\alpha })$ for every $\alpha \in \mathsf {Atts}$

Moreover, a B-consequence relation is called finitary when it enjoys the property

• (F2) if , then , for some finite ${\varPhi }_{\alpha }^{\mathtt f} \subseteq {\varPhi }_{\alpha }$, and each $\alpha \in \mathsf {Atts}$

In what follows, B-consequence relations will also be referred to as two-dimensional logics. The complement of , sometimes called the compatibility relation associated with  [10], will be denoted by  . Every B-consequence relation induces one-dimensional consequence relations and $\rhd _{\mathsf {f}}^{\mathsf {C}}$, such that iff , and iff . Given a one-dimensional consequence relation , we say that it inhabits the $\mathsf {t}$-aspect of $\mathsf {C}$ if , and that it inhabits the $\mathsf {f}$-aspect of $\mathsf {C}$ if . B-consequence relations actually induce many other (even non-Tarskian) one-dimensional notions of logics; the reader is referred to [9, 11] for a thorough presentation on this topic.

As we did for one-dimensional consequence relations, we present now realizations of B-consequence relations, first via the semantics of nd-B-matrices, then by means of two-dimensional H-systems.

A non-deterministic B -matrix over $\varSigma$, or simply $\varSigma$ -nd-B -matrix, is a structure $\mathfrak {M}:=\left\langle \mathbf {A}, {\mathsf {Y}}, {\mathsf {N}} \right\rangle$, where $\mathbf {A}$ is a $\varSigma$-nd-algebra, ${\mathsf {Y}} \subseteq A$ is the set of designated values and ${\mathsf {N}} \subseteq A$ is the set of antidesignated values of $\mathfrak {M}$. For convenience, we define to be the set of non-designated values, and to be the set of non-antidesignated values of $\mathfrak {M}$. The elements of $\mathsf {Val}_{\varSigma }(\mathbf {A})$ are dubbed $\mathfrak {M}$ -valuations. The B -entailment relation determined by $\mathfrak {M}$ is a collection of B-statements such that

• (B -ent)

  

for every . Whenever , we say that the B-statement holds in $\mathfrak {M}$ or is valid in $\mathfrak {M}$. An $\mathfrak {M}$-valuation that bears witness to is called a countermodel for in $\mathfrak {M}$. One may easily check that is a substitution-invariant B-consequence relation, that is finitary when $A$ is finite. Taking $\mathsf {C}$ as , we define $\rhd _{\mathsf {t}}^{\mathfrak {M}} :=\rhd _{\mathsf {t}}^{\mathsf {C}}$ and $\rhd _{\mathsf {f}}^{\mathfrak {M}} :=\rhd _{\mathsf {f}}^{\mathsf {C}}$.

We move now to two-dimensional, or $\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$, H-systems, first introduced in [17]. A (schematic) $\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$ rule of inference $R_\mathfrak {s}$ is the collection of all substitution instances of the $\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$ statement $\mathfrak {s}$, called the schema of $R_\mathfrak {s}$. Each $r\in R_\mathfrak {s}$ is said to be a rule instance of $R_\mathfrak {s}$. In a proof-theoretic context, rather than writing the B-statement , we shall denote the corresponding rule by . A (schematic) $\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$ H-system $\mathfrak {R}$ is a collection of $\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$ rules of inference. $\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$ derivations are as in the Set-Set H-systems, but now the nodes are labelled with pairs of sets of formulas, instead of a single set. When applying a rule instance, each formula in the succedent produces a new branch as before, but now the formula goes to the same component in which it was found in the rule instance. See Fig. 2 for a general representation and compare it with Fig. 1.

Fig. 2.

Graphical representation of finite $\mathfrak {R}$-derivations. We emphasize that, in both cases, we must have $\varPsi _{{\mathsf {Y}}}\subseteq \varPhi _{{\mathsf {Y}}}$ and $\varPsi _{\mathsf {N}}\subseteq \varPhi _{\mathsf {N}}$ to enable the application of the rule.

Let $\mathfrak {t}$ be an $\mathfrak {R}$-derivation. A node $\mathfrak {n}$ of $\mathfrak {t}$ is -closed in case it is discontinued (namely, labelled with $*$) or it is a leaf node with $\ell ^{\,\mathfrak {t}}(\mathfrak {n}) = (\varPhi _{{\mathsf {Y}}},\varPhi _{\mathsf {N}})$ and either or . A branch of $\mathfrak {t}$ is -closed when it ends in a -closed node. An $\mathfrak {R}$-derivation $\mathfrak {t}$ is said to be -closed when all of its branches are -closed. An $\mathfrak {R}$ -proof of is a -closed $\mathfrak {R}$-derivation $\mathfrak {t}$ with $\ell ^{\,\mathfrak {t}}(\mathsf {rt}(\mathfrak {t})) \subseteq (\varPhi _{{\mathsf {Y}}},\varPhi _{\mathsf {N}})$. The definitions of the (finitary) substitution-invariant B-consequence relation induced by a (finitary) $\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$ H-system $\mathfrak {R}$ and $\varTheta$-analyticity are obvious generalizations of the corresponding Set-Set definitions.

In [17], the notion of sufficient expressiveness was generalized to nd-B-matrices. We reproduce here the main definitions for self-containment:

Definition 5

Let $\mathfrak {M}:=\left\langle \mathbf {A}, {\mathsf {Y}}, {\mathsf {N}} \right\rangle$ be a $\varSigma$-nd-B-matrix.

• Given $X,Y\subseteq A$ and $\alpha \in \{{\mathsf {Y}},{\mathsf {N}}\}$, we say that $X$ and $Y$ are $\alpha$ -separated, denoted by ${X}\#_{\alpha }{Y}$, if $X\subseteq \alpha$ and $Y\subseteq \tilde{\alpha }$, or vice-versa.

• Given distinct truth-values $x, y\in A$, a unary formula $\mathrm S$ is a separator for $(x,y)$ whenever ${{\mathrm S}_{\mathbf {A}}(x)}\#_{\alpha }{{\mathrm S}_{\mathbf {A}}(y)}$ for some $\alpha \in \{{\mathsf {Y}},{\mathsf {N}}\}$. If there is a separator for each pair of distinct truth-values in $A$, then $\mathfrak {M}$ is said to be sufficiently expressive.

In the same work [17], the axiomatization algorithm of [13] was also generalized, guaranteeing that every sufficiently expressive nd-B-matrix $\mathfrak {M}$ is axiomatizable by a $\varTheta$-analytic $\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$ H-system, which is finite whenever $\mathfrak {M}$ is finite, where $\varTheta$ is a set of separators for the pairs of truth-values of $\mathfrak {M}$. Note that, in the second bullet of the above definition, a unary formula is characterized as a separator whenever it separates a pair of truth-values according to at least one of the distinguished sets of values. This means that having two of such sets may allow us to separate more pairs of truth-values than having a single set, that is, the nd-B-matrices are, in this sense, potentially more expressive than the (one-dimensional) logical matrices.

Example 2

Let $\mathbf {A}$ be the $\varSigma$-nd-algebra from Example 1, and consider the nd-B-matrix $\mathfrak {M}:=\left\langle \mathbf {A},\{\mathbf {a}\},\{\mathbf {b}\} \right\rangle$. As we know, in this matrix the pair $(\mathbf {b},\mathbf {c})$ is not separable if we consider only the set of designated values $\{\mathbf {a}\}$. However, as we have now the set $\{\mathbf {b}\}$ of antidesignated truth-values, the separation becomes evident: the propositional variable $p$ is a separator for this pair now, since $\mathbf {b}\in \{\mathbf {b}\}$ and $\mathbf {c}\not \in \{\mathbf {b}\}$. The recipe from [17] produces the following $\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$ axiomatization for $\mathfrak {M}$, with only three very simple schematic rules of inference:

By construction, the one-dimensional logic determined by the nd-matrix of Example 1 inhabits the $\mathsf {t}$-aspect of , thus it can be seen as being axiomatized by this finite and analytic two-dimensional system (contrast with the infinite Set-Set axiomatization known for this logic provided in that same example).

We constructed above a $\varSigma$-nd-B-matrix from two $\varSigma$-nd-matrices in such a way that the one-dimensional logics determined by latter are fully recoverable from the former. We formalize this construction below:

Definition 6

Let $\mathbb {M}:=\left\langle \mathbf {A},D \right\rangle$ and $\mathbb {M}' :=\left\langle \mathbf {A},D' \right\rangle$ be $\varSigma$-nd-matrices. The B -product between $\mathbb {M}$ and $\mathbb {M}'$ is the $\varSigma$-nd-B-matrix $\mathbb {M}\odot \mathbb {M}' :=\left\langle \mathbf {A},D,D' \right\rangle$.

Note that iff iff $\varPhi \rhd _{\mathsf {t}}^{\mathbb {M}\odot \mathbb {M}'}\varPsi$, and iff iff $\varPhi \rhd _{\mathsf {f}}^{\mathbb {M}\odot \mathbb {M}'}\varPsi$. Therefore, and are easily recoverable from , since they inhabit, respectively, the $\mathsf {t}$-aspect and the $\mathsf {f}$-aspect of the latter. One of the applications of this novel way of putting two distinct logics together was illustrated in that same Example 2 to produce a two-dimensional analytic and finite axiomatization for a one-dimensional logic characterized by a $\varSigma$-nd-matrix. As we have shown, the latter one-dimensional logic does not need to be finitely axiomatizable by a Set-Set H-system. We present this application of B-products with more generality below:

Proposition 2

Let $\mathbb {M}:=\left\langle \mathbf {A},D \right\rangle$ be a $\varSigma$-nd-matrix and suppose that $U \subseteq A\times A$ contains all and only the pairs of distinct truth-values that fail to be separable in $\mathbb {M}$. If, for some $\mathbb {M}' :=\left\langle \mathbf {A},D' \right\rangle$, the pairs in U are separable in $\mathbb {M}'$, then $\mathbb {M}\odot \mathbb {M}'$ is sufficiently expressive (thus, axiomatizable by an analytic $\textsc {Set}^{2}\text {-}\textsc {Set}^{2}$ H-system, that is finite whenever $\mathbf {A}$ is finite).

6 A Finite and Analytic Proof System for mCi

In the spirit of Proposition 2, we define below a nd-B-matrix by combining the matrices $\mathbb {M}_{{\textbf {mCi }}}:=\left\langle \mathbf {A}_{5}, {\mathsf {Y}}_{5} \right\rangle$ and $\mathbb {M}_{{\textbf {mCi }}}^{\mathsf {n}}:=\left\langle \mathbf {A}_{5}, {\mathsf {N}}_{5} \right\rangle$ introduced in Sect. 4 (Definition 1 and Definition 4):

Definition 7

Let $\mathfrak {M}_{{\textbf {mCi }}}:=\mathbb {M}_{{\textbf {mCi }}}\odot \mathbb {M}_{{\textbf {mCi }}}^{\mathsf {n}}= \left\langle \mathbf {A}_{5}, {\mathsf {Y}}_{5}, {\mathsf {N}}_{5} \right\rangle$, with ${\mathsf {Y}}_{5}:=\{I, T, t\}$ and ${\mathsf {N}}_{5}:=\{f,I,T\}$.

When we consider now both sets ${\mathsf {Y}}_{5}$ and ${\mathsf {N}}_{5}$ of designated and antidesignated truth-values, the separation of all truth-values of $\mathbf {A}_{5}$ becomes possible, that is, $\mathfrak {M}_{{\textbf {mCi }}}$ is sufficiently expressive, as guaranteed by Proposition 2. Furthermore, notice that we have two alternatives for separating the pairs $(I,t)$ and $(I,T)$: either using the formula ${\lnot }p$ or the formula ${\circ }p$. With this finite sufficiently expressive nd-B-matrix in hand, producing a finite $\{p,{\circ }p\}$-analytic two-dimensional H-system for it is immediate by [17, Theorem 2]. Since mCi inhabits the $\mathsf {t}$-aspect of , we may then conclude that:

Theorem 5

${\textbf {mCi }}{}$ is axiomatizable by a finite and analytic two-dimensional H-system.

Our axiomatization recipe delivers an H-system with about 300 rule schemas. When we simplify it using the streamlining procedures indicated in that paper, we obtain a much more succinct and insightful presentation, with 28 rule schemas, which we call $\mathfrak {R}_{{\textbf {mCi }}}$. The full presentation of this system is given below:

Note that the set of rules $\{{ {\copyright }}^{\textbf {mCi }}_{i} \mid {\copyright }\in \{\wedge ,\vee ,{\,\supset \,}\}, i \in \{1,2,3\}\}$ makes it clear that the $\mathsf {t}$-aspect of the induced B-consequence relation is inhabited by a logic extending positive classical logic, while the remaining rules for these connectives involve interactions between the two dimensions. Also, rule ${{\lnot }}^{\textbf {mCi }}_{2}$ indicates that ${\circ }$ satisfies one of the main conditions for being taken as a consistency connective in the logic inhabiting the $\mathsf {t}$-aspect. In fact, all these observations are aligned with the fact that the logic inhabiting the $\mathsf {t}$-aspect of is precisely mCi. See, in Fig. 3, $\mathfrak {R}_{{\textbf {mCi }}}{}$-derivations showing that, in mCi, ${\lnot }{\circ }p$ and $p{\wedge }{\lnot }p$ are logically equivalent and that ${\circ }{\lnot }{\circ }p$ is a theorem.

Fig. 3.

$\mathfrak {R}_{{\textbf {mCi }}}$-derivations showing, respectively, that , and . Note that, for a cleaner presentation, we omit the formulas inherited from parent nodes.

7 Concluding Remarks

In this work, we introduced a mechanism for combining two non-deterministic logical matrices into a non-deterministic B-matrix, creating the possibility of producing finite and analytic two-dimensional axiomatizations for one-dimensional logics that may fail to be finitely axiomatizable in terms of one-dimensional Hilbert-style systems. It is worth mentioning that, as proved in [17], one may perform proof search and countermodel search over the resulting two-dimensional systems in time at most exponential on the size of the B-statement of interest through a straightforward proof-search algorithm.

We illustrated the above-mentioned combination mechanism with two examples, one of them corresponding to a well-known logic of formal inconsistency called mCi. We ended up proving not only that this logic is not finitely axiomatizable in one dimension, but also that it is the limit of a strictly increasing chain of LFIs extending the logic mbC. From the perspective of the study of B-consequence relations, these examples allow us to eliminate the suspicion that a two-dimensional H-system $\mathfrak {R}$ may always be converted into Set-Set H-systems for the logics inhabiting the one-dimensional aspects of without losing any desirable property (in this case, finiteness of the presentation).

At first sight, the formalism of two-dimensional H-systems may be confused with the formalism of n-sided sequents [3, 4], in which the objects manipulated by rules of inference (the so-called n-sequents) accommodate more than two sets of formulas in their structures. The reader interested in a comparison between these two different approaches is referred to the concluding remarks of [17].

We close with some observations regarding $\mathfrak {M}_{{\textbf {mCi }}}$ and the two-dimensional H-system $\mathfrak {R}_{{\textbf {mCi }}}$. A one-dimensional logic $\rhd _{}^{}$ is said to be ${\lnot }$-consistent when $\varphi ,{\lnot }\varphi \rhd _{}^{} \varnothing$ and ${\lnot }$-determined when $\varnothing \rhd _{}^{} \varphi ,{\lnot }\varphi$ for all $\varphi \in L_{\varSigma }(P)$. A B-consequence relation is said to allow for gappy reasoning when and to allow for glutty reasoning when , for some $\varphi \in L_{\varSigma }(P)$. Notice that ${\lnot }$-determinedness in the logic inhabiting the $\mathsf {t}$-aspect of a B-consequence relation by no means implies the disallowance of gappy reasoning in the two-dimensional setting: we still have $F\in \overline{{\mathsf {Y}}_{5}} \cap \overline{{\mathsf {N}}_{5}}$, so one may both non-accept and non-reject a formula $\varphi$ in , even though non-accepting both $\varphi$ and its negation in mCi is not possible, in view of rule ${{\lnot }}^{\textbf {mCi }}_{7}$. Similarly, the recovery of ${\lnot }$-consistency achieved via ${\circ }$ in such logic does not coincide with the gentle disallowance of glutty reasoning in , that is, we do not have, in general, or , even though for binary compounds both are derivable in view of rules ${ {\copyright }}^{\textbf {mCi }}_{5}$, for ${\copyright }\in \{\wedge ,\vee ,{\,\supset \,}\}$, and ${\circ }_1^{{\textbf {mCi }}{}}$. With these observations we hope to call attention to the fact that B-consequence relations open the doors for further developments concerning the study of paraconsistency (and, dually, of paracompleteness), as well as the study of recovery operators [8].