1 Introduction
The relation between (finitary) closure systems, (finitary) closure operators, and (finitary) consequence relations, is well known and so is the notion of basis of a closure system
$\mathcal {C}$
(defined, e.g., as a set
$\mathcal B\subseteq \mathcal C$
such that for any
$X\in \mathcal C$
and
$x\notin X$
, there is
$X'\in \mathcal B$
such that
$x\notin X' \supseteq X$
). The logical relevance of this notion is embodied, e.g., in the Lindenbaum lemma for classical propositional logic: in this setting the corresponding closure system
$\mathcal C$
over the set of formulas
$\mathrm {Fm}$
consists of deductively closed sets of formulas (a.k.a. theories) and the lemma says that the set of maximally consistent theories (i.e., maximal elements of
$\mathcal C \setminus \{\mathrm {Fm}\}$
) is a basis of
$\mathcal C$
.
Maximally consistent theories are not always sufficient to obtain an analogous result (e.g., already for the intuitionistic logic), however it is often enough to use the (in general) bigger class of the completely meet-irreducible theories (i.e., theories which cannot be obtained as intersection of a system of strictly bigger theories). Clearly, the substitution-invariance of the underlying consequence relation (i.e., the assumption that it is closed under substitutions defined on formulas) is irrelevant for such a notion, and so one can formulate the following well-known crucial result of (not only) Algebraic logic:
Theorem 1.1 (Lindenbaum lemma).
The completely meet-irreducible closed sets form a basis of any finitary closure system.
While the finitarity restriction is crucial for its usual proof, it is not necessary: there are works (e.g., [Reference Goldblatt3–Reference Vidal, Bou, Esteva and Godo8]) proving it (or its variant for finitely meet-irreducible theories, i.e., theories which cannot be obtained as intersection of any two strictly bigger theories; more on this distinction later) for closure system arising from certain infinitary substitution-invariant consequence relations (usually modal, dynamic, or fuzzy logics). The paper [Reference Bílková, Cintula, Lávička, Moss, Queiroz and Martinez1] provides a general result for closure systems arising from substitution-invariant consequence relations with a countable axiomatization and a finite strong disjunction. The result was further strengthened in [Reference Cintula and Noguera2, theorem 5.5.14] by assuming the presence of strong p-disjunction instead of finite strong disjunction. It is worth noting that while this general result covers most of the known results, its reliance on substitution-invariance excludes examples with non-traditional syntax, such as variants of dynamic logic with infinitary Omega-Iteration rule [Reference Renardel de Lavalette, Kooi and Verbrugge5]. Our main Theorem 1.2 is its further generalization (actually, of its main ingredient [Reference Cintula and Noguera2, proposition 5.5.8] to be more precise) dropping the substitution-invariance and reformulating the additional conditions in the language of closure systems. While its proof turns out to be quite simple adaptation of the original proof from [Reference Cintula and Noguera2], the fact that it no longer requires familiarity with rather heavy logical apparatus (e.g., generalized infinite connectives with parameters) and can be presented in a fully self-contained manner, makes the result accessible to a much wider audience.
A closure system
$\mathcal C$
over a set A is countably axiomatizable if there is a countable system
$\mathcal {AS} {\kern-1pt}\subseteq{\kern-1pt} \mathcal {P}(A){\kern-1pt}\times{\kern-1pt} A$
such that
${\mathcal C {\kern-1pt}={\kern-1pt} \{ T {\kern-1pt}\mid{\kern-1pt} a{\kern-1pt}\in{\kern-1pt} T \text { for each } \langle {S,a}\rangle {\kern-1pt}\in{\kern-1pt} \mathcal {AS} \text { such that } S\subseteq T\}}$
. Let us note that to make this definition coincide with the usual one used in substitution-invariant case, we need to assume that
$\mathcal {AS}$
is closed under substitutions. Therefore in the substitution-invariant case, the countable axiomatizability clearly entails that each of the elements of
$\mathcal {AS}$
can contain only finitely many variables and that A has to be countable (assuming that there is an element of
$\mathcal {AS}$
with at least one variable).
Fortunately, for our purposes it is not necessary to recall the notion of a strong p-disjunction; it suffices to observe that due to [Reference Cintula and Noguera2, theorem 5.3.8] we know that if
$\vdash $
is a substitution-invariant consequence relation with a strong p-disjunction, then its associated closure system
$\mathcal {C}$
, which is always a complete lattice with meet being the intersection and join
$\vee $
of a family
$ \mathcal Y \subseteq \mathcal {C}$
defined as
$$ \begin{align*}\bigvee \mathcal Y = C(\bigcup \mathcal Y) \end{align*} $$
is actually a frame, i.e., a distributive lattice such that for each
$\{X\} \cup \mathcal Y \subseteq \mathcal {C}$
,
$$ \begin{align*}X \cap \bigvee \mathcal Y = \bigvee\limits_{Y \in \mathcal Y} (X \cap Y). \end{align*} $$
This observation suggests the formulation of main result of this paper:Footnote 1
Theorem 1.2. The finitely meet-irreducible closed sets form a basis of any closure system that is defined over a countable set, is a frame, and has a countable axiomatization.
Before we present a proof of this theorem, it should be stressed that as it is formulated for finitely meet-irreducible theories and so it is a variant rather than a generalization of Lindenbaum lemma. Let us end this introduction by commenting, why it is not a problem, at least for its applications in logic.
First, note that while completely meet-irreducible, finitely meet-irreducible, and even maximally consistent theories coincide in classical logic, already in the intuitionistic logic they form three distinct classes. In weaker logics, the simple syntactic characterization of these theories via connectives (negation, disjunction, and implication) is also lost. Instead, we obtain (potentially different) classes of: 1) complete theories (for any
$\varphi $
,
$\varphi \in T$
or
$\neg \varphi \in T$
); 2) prime theories (for any
$\varphi ,\psi $
,
$\varphi \vee \psi \in T$
implies
$\varphi \in T$
or
$\psi \in T$
); and 3) linear theories (for any
$\varphi ,\psi $
,
$\varphi \to \psi \in T$
or
$\psi \to \varphi \in T$
). Interestingly, these classes of theories are almost always subclasses of finitely meet-irreducible theories. In “well-behaved” logics, they even coincide with them. For example, prime theories coincide with finitely meet-irreducible theories in logics with suitable disjunctions (such as intuitionistic logic), and linear theories do so in logics that are complete with respect to their linearly ordered algebraic models (e.g., various fuzzy logics). Therefore, the fact that finitely meet-irreducible theories form a basis is a crucial result in the study of such logics.
2 The proof of Theorem 1.2
Let A denote the domain of closure system
$\mathcal {C}$
, C/
$\vdash $
be its associated closure operator/consequence relation, and
$\mathcal {AS}$
be some of its countable axiomatic systems. Let us recall the folklore notion of the tree-proof in infinitary consequence relations (see, e.g., [Reference Cintula and Noguera2] where it is heavily used for the substitution-invariant consequence relations):
$X \vdash x$
iff there is a tree-proof of x from X in
$\mathcal {AS}$
, i.e., a tree without infinite branches labeled by elements of A such that:
-
• its root is labeled by x,
-
• if y is a label of some of its leafs, then
$y\in X$
or
$\langle {\emptyset , y}\rangle \in \mathcal {AS}$
, -
• if a non-leaf is labeled by y and Y is the set of labels of its direct predecessors, then
$\langle {Y,y}\rangle \in \mathcal {AS}$
.
We continue by introducing a relation
$\Vdash $
between subsets X of A and finite subsets Y of A defined as
$$ \begin{align*} X\Vdash Y & \quad\text{iff}\quad \bigcap\limits_{y\in Y} C(y) \subseteq C(X) \end{align*} $$
and proving that for all sets
$X, P \subseteq A$
and each finite set
$Y\cup \{a,b\}\subseteq A$
:Footnote
2
$$ \begin{align} \frac{X,a\Vdash Y \qquad\qquad X,b\Vdash Y}{X, C(a)\cap C(b)\Vdash Y}. \end{align} $$
$$ \begin{align} \frac{\{X\Vdash Y, p \mid p\in P\} \qquad\qquad X, P \Vdash Y}{X\Vdash Y}. \end{align} $$
We first prove (PCP) by a simple chain of (in)equations (note that we use the distributivity of
$\mathcal C$
):
$$ \begin{align*} \bigcap_{y\in Y} C(y) & \subseteq C(X\cup\{a\}) \cap C(X\cup\{b\}) = (C(X)\vee C(a))\cap (C(X)\vee C(b)) \\ & = C(X)\vee(C(a)\cap C(b)) = C(X\cup(C(a)\cap C(b))). \end{align*} $$
To prove (CUT), let us set
$W = \bigcap _{y\in Y} C(y)$
and note that
$W = C(W)$
. Then we use the left premise of (CUT), to obtain
$W\cap C(p) \subseteq C(X)$
for each
$p \in P$
and so using the fact that
$\mathcal C$
is a frame we obtain that
$W\cap C(P) \subseteq C(X)$
, indeed:
$$ \begin{align*}W\cap C(P) = W\cap \bigvee\limits_{p\in P} (C(p)) = \bigvee\limits_{p\in P} (W\cap C(p)) \subseteq C(X). \end{align*} $$
Next we use the right premise of (CUT) to obtain
$W \subseteq C(X)\vee C(P)$
. Putting it all together and using the distributivity of
$\mathcal C$
, we obtain
$W \subseteq C(X)$
as required:
$$ \begin{align*}W {\kern-1pt}={\kern-1pt} W\cap(C(X)\vee C(P)) {\kern-1pt}={\kern-1pt} (W\cap C(X))\vee (W\cap C(P)) \subseteq C(X) \vee C(X) {\kern-1pt}={\kern-1pt} C(X). \end{align*} $$
Now we are ready to prove the claim: for a given
$x \notin C(X)$
we construct a finitely meet-irreducible
$X' \in \mathcal C$
such that
$X \subseteq X'$
and
$x \notin X'$
.
We start by enumerating all pairs of elements of A by even natural numbers and all elements of
$\mathcal {AS}$
by odd natural numbers. We construct increasing sequences
$X_i$
and
$Y_i$
of subsets, respectively finite subsets, of A such that
$X_i \not \Vdash Y_i$
. We set
$X_0 = X$
and
$Y_0 = \{x\}$
and in the subsequent recursive construction we distinguish odd and even steps. Roughly speaking, in odd steps we make sure that the union of
$X_i$
s is a closed set and in even steps we make sure it is a finitely meet-irreducible one.
If the ith step is even we process the ith pair
$\langle {a_i, b_i}\rangle $
:
-
1. If
$X_i, a_i \not \Vdash Y_i$
, then we set
$X_{i+1} = X_i\cup \{a_i\}$
and
$Y_{i+1} = Y_i$
. -
2. If
$X_i, a_i \Vdash Y_i$
and
$X_i, b_i \not \Vdash Y_i$
, then we set
$X_{i+1} = X_i\cup \{b_i\}$
and
$Y_{i+1} = Y_i$
. -
3. If
$X_i,a_i \Vdash Y_i$
and
$X_i,b_i \Vdash Y_i$
, then there has to be
$w_i \in C(a_i)\cap C(b_i)$
such that
$X_i \not \Vdash Y_i, w_i$
and so we set
$X_{i+1} = X_i$
and
$Y_{i+1} = Y_i\cup \{w_i\}$
.
Indeed such
$w_i$
has to exist as otherwise we could obtain a contradiction with the induction assumption
$X_i\not \Vdash Y_i$
via the following derivation (note that we use (CUT) together with (PCP)):
$$ \begin{align*}\frac{\{X_i\Vdash Y_i, w \mid w\in C(a_i)\cap C(b_i)\} \qquad \displaystyle \frac{X_i, a_i\Vdash Y_i \qquad\qquad X_i,b_i\Vdash Y_i}{X_i, C(a_i)\cap C(b_i)\Vdash Y_i}}{X_i\Vdash Y_i}. \end{align*} $$
If the ith step is odd we process the ith rule
$\langle {P_i,c_i}\rangle $
:
-
1. If
$X_i, c_i \not \Vdash Y_i$
, then we set
$X_{i+1} = X_i \cup \{c_i\}$
and
$Y_{i+1} = Y_i$
. -
2. If
$X_i, c_i \Vdash Y_i$
, then there has to be
$p_i \in P_i$
such that
$X_i \not \Vdash Y_i,p_i$
and so we set
$X_{i+1} = X_i$
and
$Y_{i+1} = Y_i \cup \{p_i\}$
.
Indeed such
$p_i$
has to exist as otherwise we could obtain a contradiction with the induction assumption
$X_i\not \Vdash Y_i$
via the following derivation (note that we use (CUT) twice together with monotonicity of
$\Vdash $
and the fact that
$C(c_i)\subseteq C(P_i)$
):
$$ \begin{align*}\frac{\frac{\displaystyle\frac{\{X_i\Vdash Y_i,p \mid p\in P_i\}}{\{X_i\Vdash Y_i,c_i,p \mid p\in P_i\}} \qquad \frac{P_i \Vdash c_i}{X_i, P_i \Vdash Y_i, c_i}}{\displaystyle X_i\Vdash Y_i, c_i}\qquad X_i,c_i\Vdash Y_i}{X_i\Vdash Y_i}. \end{align*} $$
Next we define
$X'$
as the union of
$X_i$
s and prove the following fact:
$$ \begin{align} y \in C(X') \qquad\text{iff} \qquad y\in X_i \quad \text{for some } i. \end{align} $$
The right-to-left direction is trivial; to prove the converse one, let us assume that
$X'\vdash y$
, fix a tree-proof of y from
$X'$
, and denote by
$l_{\mathbf {n}}$
the label of the node
$\mathbf {n}$
. We prove that for each node
$\mathbf {n}$
there is i such that
$l_{\mathbf {n}} \in X_i$
. As a tree-proof is a well-founded relation with leaves as minimal elements and the root as a maximum, we can do so by induction. If
$\mathbf {n}$
is a leaf the claim is trivial: indeed then either
$l_{\mathbf {n}} \in X'$
or there is i such that
$l_{\mathbf {n}} = c_i$
and
$\langle {\emptyset , c_i}\rangle \in \mathcal {AS} $
and so
$l_{\mathbf {n}} \in X_{i+1}$
(as in this case we clearly have
$X_i, c_i \not \Vdash Y_i$
). If
$\mathbf {n}$
is not a leaf then there is i such that
$l_{\mathbf {n}} = c_i$
and
$\langle {P_i, c_i}\rangle \in \mathcal {AS}$
. Then either
$l_{\mathbf {n}} \in X_{i+1}$
, which is what we want, or there is
$p_i \in P_i$
such that
$p_i \in Y_{i+1}$
. We show that the second case cannot happen: As
$p_i$
is a label of a (direct) predecessor of
$\mathbf {n}$
we know by the induction hypothesis that
$p_i \in X_j$
for some j and so
$p_i\in X_j\cap Y_{i+1} \subseteq X_{\max \{i+1,j\}} \cap Y_{\max \{i+1,j\}}$
, a contradiction with
$X_{\max \{i+1,j\}} \not \Vdash Y_{\max \{i+1,j\}}$
.
From the fact we have just proved we obtain that
$X' \in \mathcal {C}$
and, as clearly
$x \notin X' = C(X')$
, to complete the proof it suffices to show that
$X'$
is finitely meet-irreducible. Assume that it is not, i.e., that
$X' = X_1 \cap X_2$
for some
$X_1, X_2 \in \mathcal {C}$
such that there are
$a\in X_1\setminus X'$
and
$b\in X_2\setminus X'$
. Assume that the pair
$\langle {a,b}\rangle $
was processed in the ith step and note that we had to progress by the third option (because otherwise we would have
$a\in X'$
or
$b\in X'$
) and so there is
$w_i$
in
$Y_{i+1}$
such that
$w_i \in C(a)\cap C(b) \subseteq X_1\cap X_2 = X'$
. Thus due to the (Fact) we know that
$w_i \in X_j$
for some j, a contradiction with
$X_{\max \{i+1,j\}} \not \Vdash Y_{\max \{i+1,j\}}$
.
Funding
The author was supported by the project 22-16111S of the Czech Science Foundation.
