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 -matrix) by the combination of two (possibly partial) non-deterministic logical matrices.  We will show that such a combination may result in  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 .  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 -matrix that is axiomatized by a two-dimensional Hilbert-style system that is both finite and analytic.

§ 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 ` H-systems', do not allow for more than one formula in the succedents of the consecutions that they manipulate.

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 [18, 13].
Such generalized systems, here dubbed ` 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  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  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  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  is also an example of this phenomenon.
This logic results from adding infinitely-many axiom
schemas to the logic ,
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
is the limit of a strictly increasing
chain of LFIs
extending  (comparable to the case of

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

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 ` H-systems',

generalize  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
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  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 -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 .

The paper is organized as follows: Section <ref> introduces basic terminology and definitions regarding algebras and languages. Section <ref> presents the notions of one-dimensional logics and  H-systems. Section <ref> proves that  is not finitely axiomatizable by one-dimensional H-systems. Section <ref> introduces
two-dimensional logics and H-systems, and describes the approach to extending a logical matrix to a -matrix with the goal of finding a finite two-dimensional axiomatization for the logic associated with the former.
Section <ref> presents a two-dimensional finite analytic H-system for . 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.

Detailed proofs of some results may be found

in accompanying appendices.

§ PRELIMINARIES

A propositional signature
is a family
$\SigA \SymbDef \{\SigArity{\Sigma}{k}\}_{\ArityA \in \NatSet}$,
where each $\SigArity{\Sigma}{\ArityA}$ is
a collection of $\ArityA$-ary connectives.
We say that $\SigA$ is finite when its base set $\bigcup_{k\in\NatSet}\SigArity{\SigA}{k}$ is finite.

A non-deterministic algebra over $\SigA$, or simply $\SigA$-nd-algebra, is a structure
$\AlgA \SymbDef \Struct{\ValSetA, \AlgInterp{\FunPlaceholder}{\AlgA}}$,
such that $\ValSetA$ is a non-empty collection of values
called the carrier of $\AlgA$,
and, for each $\ArityA \in \NatSet$ and $\ConA \in \SigArity{\SigA}{\ArityA}$,
the multifunction
$\AlgInterp{\ConA}{\AlgA} : \ValSetA^\ArityA \to \PowerSet{\ValSetA}$
is the interpretation of $\ConA$ in $\AlgA$.
When $\SigA$ and $\ValSetA$ are finite, we say that $\AlgA$ is finite.
When the range of all interpretations of $\AlgA$ contains only
singletons, $\AlgA$ is said to be a deterministic algebra over $\SigA$,
or simply a $\SigA$-algebra, meeting the usual definition
from Universal Algebra [12].
When $\EmptySet$ is not in the range
of each $\AlgInterp{\ConA}{\AlgA}$,
$\AlgA$ is said to be total.

Given a $\SigA$-algebra $\AlgA$ and a $\ConA \in \SigArity{\SigA}{1}$, we
let $\AlgInterp{\ConA}{\AlgA}^0(\ValA) \SymbDef \ValA$
and $\AlgInterp{\ConA}{\AlgA}^{i+1}(\ValA) \SymbDef \AlgInterp{\ConA}{\AlgA}(\AlgInterp{\ConA}{\AlgA}^i(\ValA))$.

A mapping $\ValuationA : \ValSetA \to \ValSetB$
is a homomorphism from $\AlgA$ to $\AlgB$ when,
for all $\ArityA \in \NatSet$, $\ConA \in \SigArity{\SigA}{\ArityA}$
and $\ValA_1,\ldots,\ValA_k \in \ValSetA$, we have
$\ValAssignA[\AlgInterp{\ConA}{\AlgA}(\ValA_1,\ldots,\ValA_k)] \subseteq \AlgInterp{\ConA}{\AlgB}(\ValAssignA(\ValA_1),\ldots,\ValAssignA(\ValA_k))$.

The set of all homomorphisms from $\AlgA$ to $\AlgB$ is
denoted by $\HomSet{\SigA}{\AlgA}{\AlgB}$.
When $\AlgB = \AlgA$, we write $\EndSet{\SigA}{\AlgA}$, rather than $\HomSet{\SigA}{\AlgA}{\AlgA}$, for
the set of endomorphisms on $\AlgA$.

Let $\PropSetA$ be a denumerable collection of
$\DefEmph{propositional variables}$
and $\SigA$ be a propositional signature.
The absolutely free $\SigA$-algebra freely generated by
$\PropSetA$ is denoted by $\LangAlg{\SigA}{\PropSetA}$
and called the $\SigA$-language generated by $\PropSetA$.
The elements of $\LangSet{\SigA}{\PropSetA}$ are called
$\SigA$-formulas, and those among them that are
not propositional variables are called $\SigA$-compounds.
Given $\FmSetA \subseteq \LangSet{\SigA}{\PropSetA}$,
we denote by $\FmSetCompl{\FmSetA}$ the set $\SetDiff{\LangSet{\SigA}{\PropSetA}}{\FmSetA}$.

The homomorphisms from $\LangAlg{\SigA}{\PropSetA}$ to $\AlgA$ are called valuations on $\AlgA$,
and we denote by $\ValSet{\SigA}{\AlgA}$ the collection thereof.

Additionally, endomorphisms on $\LangAlg{\SigA}{\PropSetA}$ are dubbed
$\SigA$-substitutions, and we let $\SubsSet{\SigA}{\PropSetA} \SymbDef \EndSet{\SigA}{\LangAlg{\SigA}{\PropSetA}}$;
when there is no risk of confusion, we may omit the superscript from this notation.

Given $\FmA \in \LangSet{\SigA}{\PropSetA}$,

$\PropVars{\FmA}$ be the set of propositional
variables occurring in $\FmA$.

If $\PropVars{\FmA} = \{\PropA_1,\ldots,\PropA_k\}$,
we say that $\FmA$ is $\ArityA$-ary (unary, for $k=1$; binary, for $k=2$) and
$\AlgInterp{\FmA}{\AlgA} : \ValSetA^\ArityA \to \PowerSet{\ValSetA}$
be the $\ArityA$-ary multifunction on $\AlgA$ induced by $\FmA$,
where, for all $\ValA_1,\ldots,\ValA_k \in \ValSetA$, we have
$\AlgInterp{\FmA}{\AlgA}(\ValA_1,\ldots,\ValA_k) \SymbDef
\{\ValuationA(\FmA) \mid \ValuationA \in \ValSet{\SigA}{\AlgA} \text{ and } \ValuationA(\PropA_i) = \ValA_i, \text{ for } 1 \leq i \leq \ArityA\}$.
Moreover, given $\FmB_1,\ldots,\FmB_k \in \LangSet{\SigA}{\PropSetA}$, we write $\FmA(\FmB_1,\ldots,\FmB_k)$
for the $\SigA$-formula $\AlgInterp{\FmA}{\LangAlg{\SigA}{\PropSetA}}(\FmB_1,\ldots,\FmB_k)$,
and, where $\FmSetA\subseteq\LangSet{\SigA}{\PropSetA}$ is a set of
$\ArityA$-ary $\SigA$-formulas, we let $\FmSetA(\FmB_1,\ldots,\FmB_k) \SymbDef \{\FmA(\FmB_1,\ldots,\FmB_k) \mid \FmA \in \FmSetA\}$.

Given $\FmA \in \LangSet{\SigA}{\PropSetA}$,
by $\Subformulas{\FmA}$ we refer to the set of subformulas of $\FmA$.
Where $\BAnaFormA$ is a unary $\SigA$-formula, we define the set $\GenSubfmlas{\BAnaFormA}{\FmA}$

as $\{\SubstA(\BAnaFormA)\mid \SubstA~:~\PropSetA \to \Subformulas{\FmA}\}$.  Given a set $\BAnaSetA \supseteq \Set{\PropA}$ of unary $\SigA$-formulas, we set $\GenSubfmlas{\BAnaSetA}{\FmA} \SymbDef \bigcup_{\BAnaFormA\in\BAnaSetA}\GenSubfmlas{\BAnaFormA}{\FmA}$.

For example, if $\BAnaSetA = \Set{\PropA,\mciNeg\PropA}$, we will have $\GenSubfmlas{\BAnaSetA}{\mciNeg(\PropB\lor\PropC)} = \Set{\PropB,\PropC,\PropB\lor\PropC,\mciNeg(\PropB\lor\PropC)}\cup\Set{ \mciNeg\PropB,\mciNeg\PropC,\mciNeg(\PropB\lor\PropC),\mciNeg\mciNeg(\PropB\lor\PropC)}$. Such generalized notion of
subformulas will be used in the next section
to provide a more generous proof-theoretical concept of analyticity.

§ ONE-DIMENSIONAL CONSEQUENCE RELATIONS

A  statement (or sequent) is a pair $\Pair{\FmSetA}{\FmSetB} \in \PowerSet{\LangSet{\Sigma}{\PropSetA}} \times \PowerSet{\LangSet{\Sigma}{\PropSetA}}$,
where $\FmSetA$ is dubbed the antecedent and $\FmSetB$ the succedent.  A one-dimensional consequence relation on $\LangSet{\SigA}{\PropSetA}$ is a collection $\SetSetCR{}$ of  statements
satisfying, for all $\FmSetA,\FmSetB,\FmSetA^\prime,\FmSetB^\prime \subseteq \LangSet{\SigA}{\PropSetA}$,

prop:CRSSPropO if $\FmSetA \cap \FmSetB \neq \EmptySet$, then $\FmSetA \SetSetCR{} \FmSetB$

prop:CRSSPropD if $\FmSetA \SetSetCR{} \FmSetB$, then
$\FmSetA\cup\FmSetA^\prime \SetSetCR{}{} \FmSetB\cup\FmSetB^\prime$

prop:CRSSPropC if
$\CutSetSS\cup\FmSetA \SetSetCR{} \FmSetB\cup\FmSetCompl{\CutSetSS}$
for all $\CutSetSS\subseteq\LangSet{\SigA}{\PropSetA}$,
then $\FmSetA \SetSetCR{} \FmSetB$

Properties <ref>, <ref>
and <ref> are called
overlap, dilution
and cut, respectively.

The relation $\SetSetCR{}$ is called substitution-invariant when it satisfies, for every $\SubstA \in \SubsSet{\SigA}{}$,

if $\FmSetA \SetSetCR{} \FmSetB$,
then $\sigma[\FmSetA] \SetSetCR{} \sigma[\FmSetB]$

and it is called finitary when it satisfies

if $\FmSetA \SetSetCR{} \FmSetB$,
$\FinSet{\FmSetA} \SetSetCR{} \FinSet{\FmSetB}$
for some finite
$\FinSet{\FmSetA} \subseteq \FmSetA$ and
$\FinSet{\FmSetB} \subseteq \FmSetB$

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 $\nSetSetRel{}{}$ the complement
of $\SetSetRel{}{}$, called the compatibility relation associated with $\SetSetRel{}{}$ [10].

A  statement is a sequent having a single formula as consequent.
When we restrict standard consequence relations to collections of  statements, we define the so-called (substitution-invariant finitary) Tarskian consequence relations.
Every one-dimensional consequence relation
$\SetSetRel{}{}$ determines a Tarskian consequence relation $\SetFmlaRel{\SetSetRel{}{}}{} \;\subseteq\PowerSet{\LangSet{\SigA}{\PropSetA}} \times \LangSet{\SigA}{\PropSetA}$,
dubbed the  Tarskian companion of $\SetSetRel{}{}$,
such that, for all $\FmSetA \cup \{\FmB\} \subseteq \LangSet{\SigA}{\PropSetA}$,
$\FmSetA \SetFmlaRel{\SetSetRel{}{}}{} \FmB$ if, and only if,
$\FmSetA \SetSetRel{}{} \{\FmB\}$.

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 $\Supremum C$
its supremum in the latter lattice.

We present in what follows two ways of obtaining one-dimensional consequence relations:
one semantical,

non-deterministic logical matrices [6],
and the other proof-theoretical,

via  Hilbert-style systems [23, 18].

A non-deterministic $\SigA$-matrix, or simply $\SigA$-nd-matrix,
is a structure $\MatA \SymbDef \Struct{\AlgA,\DesSetA}$,
where $\AlgA$ is a $\SigA$-nd-algebra,
whose carrier is the set of truth-values,
and $\DesSetA \subseteq \ValSetA$ 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 $\SigA$-nd-matrices with the restriction that $\AlgA$ must be total.

From now on, whenever $\ValSubsetA \subseteq \ValSetA$, we denote
$\SetDiff{\ValSetA}{\ValSubsetA}$ by $\ValueSetComp{\ValSubsetA}$.
In case $\AlgA$ is deterministic, we simply say that $\MatA$
is a $\SigA$-matrix.
Also, $\MatA$ is said to be finite when $\AlgA$ is finite.

Every $\SigA$-nd-matrix $\MatA$ determines a substitution-invariant one-dimensional consequence
relation over $\SigA$, denoted by $\SetSetMCR{\MatA}$,
such that

if, and only if, for all
[] ∩  ≠ or
[] ∩≠.

It is worth noting that
$\SetSetMCR{\MatA}$ is
finitary whenever the carrier of $\AlgA$ is finite (the proof runs very similar to that of the same result for Nmatrices <cit.>).

A strong homomorphism between $\SigA$-matrices
$\MatA_1 \SymbDef \Struct{\AlgA_1,D_1}$
and $\MatA_2 \SymbDef \Struct{\AlgA_2, D_2}$
is a homomorphism $h$ between $\AlgA_1$ and $\AlgA_2$
such that $\ValA \in D_1$ if, and only if, $h(\ValA) \in D_2$.
When there is a surjective strong homomorphism between $\MatA_1$
and $\MatA_2$, we have that $\SetSetCR{\MatA_1} = \SetSetCR{\MatA_2}$.

Now, to the Hilbert-style systems.
A (schematic)  rule of inference $\SSHRuleOfInf_\SSHRuleSchema$
is the collection
of all substitution instances
of the  statement $\SSHRuleSchema$,
called the schema of $\SSHRuleOfInf_\SSHRuleSchema$.

Each $\SSHRuleInst \in  \SSHRuleOfInf_\SSHRuleSchema$
is called a rule instance of $\SSHRuleOfInf_\SSHRuleSchema$.

A (schematic)  H-system $\SSHCalcA$ is a collection of
rules of inference.

When we constrain the rule instances of $\SSHCalcA$
to having only singletons as succedents,
we obtain the conventional notion of Hilbert-style system,
called here  H-system.

An $\SSHCalcA$-derivation
in a  H-system $\SSHCalcA$
is a rooted directed
tree $\SSHTreeA$
such that every node is
labelled with sets of formulas or with
a discontinuation symbol $\StarLabel$, and in which
every non-leaf node (that is, a node with child nodes) $\SSHNodeA$ in $\TreeA$ is an expansion of $\SSHNodeA$
by a rule instance $\SSHRuleInst$ of $\SSHCalcA$. This means that
the antecedent of $\SSHRuleInst$ is contained in the label of $\SSHNodeA$

and that
$\SSHNodeA$ has exactly one child node for
each formula $\FmB$ in the succedent of $\SSHRuleInst$.
These child nodes are, in turn, labelled with the same formulas as those of $\SSHNodeA$
plus the respective formula $\FmB$. In case $\SSHRuleInst$ has an empty
succedent, then $\SSHNodeA$ has a single child node
labelled with $\StarLabel$.
Here we will consider only finitary
H-systems, in which each rule instance has
finite antecedent and succedent.
In such cases, we only need to consider finite
Figure <ref>
illustrates how derivations
using only finitary rules of inference may be graphically represented.
We denote by $\LabelFn{\SSHTreeA}(\SSHNodeA)$
the label of the node $\SSHNodeA$ in the tree
It is worth observing that, for  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

[every tree node/.style=,
level distance=1.2cm,sibling distance=1cm,
edge from parent path=() – (), baseline]
[.[style=draw,circle] ;
[.[style=] $\FmSetA$;
node[auto=right] $\HRule{\FmSetC}{\EmptySet}$;

[every tree node/.style=,
level distance=1cm,sibling distance=.5cm,
edge from parent path=() – (), baseline]
[.[style=draw,circle] ;
[.[style=] $\FmSetA$;
node[auto=right] $\HRule{\FmSetC}{\FmB_1,\FmB_2,\ldots,\FmB_n}$;

Graphical representation of $\SSHCalcA$-derivations, for
$\SSHCalcA$ 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
exhibiting only the ones introduced by the
applied rule of inference.
In both cases,
we must have $\FmSetC \subseteq \FmSetA$
to enable the application of the rule.

A node $\SSHNodeA$ of an $\SSHCalcA$-derivation $\SSHTreeA$ is called
$\FmSetD$-closed in case
it is a leaf node with
$\LabelFn{\SSHTreeA}(\SSHNodeA) = \StarLabel$
$\LabelFn{\SSHTreeA}(\SSHNodeA) \cap \FmSetD \neq \EmptySet$.
A branch of $\SSHTreeA$ is $\FmSetD$-closed
when it ends in a $\FmSetD$-closed node.
When every branch in
$\SSHTreeA$ is $\FmSetD$-closed,
we say that $\SSHCalcA$ is itself

An $\SSHCalcA$-proof of a  statement
$\Statement{\FmSetA}{\FmSetB}$ is
a $\FmSetB$-closed $\SSHCalcA$-derivation $\SSHTreeA$
such that $\LabelFn{\SSHTreeA}(\TreeRoot{\SSHTreeA}) \subseteq \FmSetA$.

Consider the binary relation $\SSHCR{\SSHCalcA}$ on $\PowerSet{\LangSet{\SigA}{\PropSetA}}$
such that
$\FmSetA \SSHCR{\SSHCalcA} \FmSetB$
if, and only if, there is
an $\SSHCalcA$-proof of $\Statement{\FmSetA}{\FmSetB}$.
This relation is the
smallest substitution-invariant one-dimensional consequence relation
containing the rules of inference of $\SSHCalcA$,
and it is finitary when $\SSHCalcA$ is finitary.
Since  (and ) 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
whose nodes are labelled only with
subsets of $\GenSubfmlasFn{\BAnaSetA}[\FmSetA \cup \FmSetB]$, we write $\FmSetA \SetSetRel{\SSHCalcA}{\BAnaSetA} \FmSetB$

In case $\SSHCR{\SSHCalcA} = \SetSetRel{\SSHCalcA}{\BAnaSetA}$,
we say that $\SSHCalcA$ is
Note that the ordinary notion of analyticity obtains when
$\BAnaSetA = \Set{\PropA}$.
From now on, whenever we use
the word “analytic” we will mean
this extended notion of
for some $\BAnaSetA$ implicit in the context. When the
$\BAnaSetA$ 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  H-systems by Shoesmith and Smiley [23], it was proved that
any non-deterministic logical matrix $\MatA$ satisfying a criterion of sufficient expressiveness
is axiomatizable by a $\BAnaSetA$-analytic  Hilbert-style system,
which is finite whenever $\MatA$ is finite,
where $\BAnaSetA$ is the set of separators
for the pairs of truth-values of $\MatA$.
According to such criterion, an nd-matrix is sufficiently expressive when,
for every pair $\Pair{\ValA}{\ValB}$
of distinct truth-values,
there is a unary formula $\SepA$,
called a separator for $\Pair{x}{y}$,
such that $\AlgInterp{\SepA}{\AlgA}(\ValA) \subseteq \DesSetA$
and $\AlgInterp{\SepA}{\AlgA}(\ValB) \subseteq \ValuesSetCompl{\DesSetA}$,
or vice-versa;
in other words, when every pair of
distinct truth-values is separable in $\MatA$.

We emphasize that it is essential for the above result
the adoption of  H-systems, instead
of the more restricted  H-systems.

In fact, while two-valued matrices may always be finitely axiomatized by  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  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  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:

Consider the signature $\SigA\SymbDef \{\SigArity{\Sigma}{k}\}_{\ArityA \in \NatSet}$ such that
$\SigA_1 \SymbDef \Set{g, h}$
and $\SigA_k \SymbDef \EmptySet$ for all
$k \neq 1$.
Let $\MatA \SymbDef \Struct{\AlgA, \Set{\tVal}}$ be a
$\SigA$-nd-matrix, with $\ValSetA \SymbDef \Set{\tVal,\fVal,\BotVal}$ and

\begin{align*}
\AlgInterp{g}{\AlgA}(\ValA)
\begin{cases}
%\ValSetA, & \text{if } \ValA \neq \BotVal\\
%\fVal, & \text{otherwise}\\
\Set{\tVal}, & \text{if } \ValA = \BotVal\\
\ValSetA, & \text{otherwise}\\
\end{cases}
\quad
\AlgInterp{h}{\AlgA}(\ValA)
\begin{cases}
%\ValSetA, & \text{if } \ValA \neq \tVal\\
%\tVal, & \text{otherwise}\\
\Set{\fVal}, & \text{if } \ValA = \fVal\\
\ValSetA, & \text{otherwise}\\
\end{cases}
\end{align*}

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

\begin{gather*}
\HRule{h^i(\PropA)}{\PropA, g(\PropA)},
\text{ for all $i \in \NatSet$}.
\end{gather*}

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

§ THE LOGIC  IS NOT FINITELY AXIOMATIZABLE

A one-dimensional logic $\SSHCR{}$ over $\SigA$ is said to be

we have $\PropA,\mciNeg\PropA \;\nSetSetRel{}{}\; \PropB$,
for $\PropA,\PropB \in \PropSetA$.

Moreover, $\SSHCR{}$
is $\mciNeg$-gently explosive in case there is a collection $\bigcirc(\PropA) \subseteq \LangSet{\SigA}{\PropSetA}$ of unary formulas such that,
for some $\FmA \in \LangSet{\SigA}{\PropSetA}$,
we have
$\bigcirc(\FmA), \FmA \nSetSetRel{}{} \varnothing$;
$\bigcirc(\FmA), \mciNeg\FmA \nSetSetRel{}{} \varnothing$,
and, for all $\FmA \in \LangSet{\Sigma}{\PropSetA}$,
$\bigcirc(\FmA),\FmA,\mciNeg\FmA \; \SSHCR{} \varnothing$.
We say that $\SSHCR{}$ is a
logic of formal inconsistency (LFI) in case it is $\mciNeg$-paraconsistent yet
$\mciNeg$-gently explosive.
In case $\bigcirc(\PropA) = \{\mciCons\PropA\}$,
for $\mciCons$ a (primitive or composite) consistency connective, the logic is said also to be a C-system.
In what follows,
let $\SigMCI$ be the propositional signature such that
$\SigMCI_{1} \SymbDef \{\mciNeg,\mciCons\}$,
$\SigMCI_{2} \SymbDef \{\land,\lor,\mciImp\}$,
and $\SigMCI_{k} \SymbDef \EmptySet$
for all $k \not\in \{1,2\}$.

One of the simplest
is the logic , which was
first presented in terms of
a  H-system over $\SigMCI$
obtained by extending
any  H-system for
positive classical logic ()
with the following pair of axiom schemas: