1 Introduction
An important theme in the studies of universal algebra and non-classical logics involves determining the cardinality of classes of equational theories (equivalently, varieties) and logics. A variety is an equationally definable class of algebras [Reference Burris and Sankappanavar4]. Finite monoids that generate varieties with
$2^{\aleph _0}$
many subvarieties were constructed in [Reference Jackson and McKenzie13], and later a finite monoid that generates a variety with exactly
$\aleph _0$
subvarieties was found in [Reference Jackson and Lee12]. In [Reference Jackson and Lee12], Jackson and Lee raised the question of whether the subvariety lattice of every variety has cardinality either
$\leq \aleph _0$
or
$2^{\aleph _0}$
[Reference Jackson and Lee12, Question 6.4(ii)].
In the logical context, Jankov [Reference Jankov14] showed that there are
$2^{\aleph _0}$
many distinct superintuitionistic logics, and consequently
$2^{\aleph _0}$
many modal logics in extensions of
$\mathsf {K}$
,
$\mathsf {K4}$
,
$\mathsf {S4}$
, etc. This laid a foundation for the study of cardinalities of classes of modal and superintuitionistic logics. Fine [Reference Fine10] showed that every normal extension of the modal logic
$\mathsf {S4.3}$
is finitely axiomatizable. As a consequence, he obtained that
$\mathsf {S4.3}$
has countably many normal extensions. For more information on cardinalities of intervals of modal and superintuitionistic logics, we refer to [Reference Chagrov and Zakharyaschev5].
For a superintuitionistic or modal logic L, the degree of fmp of L refers to the cardinality of the fmp span of L, that is, the set of logics that define the same class of finite Kripke frames as L. Bezhanishvili et al. [Reference Bezhanishvili, Bezhanishvili and Moraschini2] proved that every cardinal
$\kappa \leq \aleph _0$
and
$\kappa = 2^{\aleph _0}$
is realized as the degree of finite model property (fmp) for some superintuitionistic and transitive modal logic. They also asked the question whether it is provable without the continuum hypothesis (CH) that the degree of fmp can (only) be either
$\leq \aleph _0$
or
$2^{\aleph _0}$
[Reference Bezhanishvili, Bezhanishvili and Moraschini2, Sec. 8(1)]. This question is closely connected to the one posed by Jackson and Lee. A logic is tabular if it is characterized by a single finite Kripke frame, and is pretabular if it is not tabular while all its proper consistent extensions are tabular. Recently, Chen [Reference Chen7] showed that for every cardinal
$\kappa \leq \aleph _0$
and
$\kappa = 2^{\aleph _0}$
, there is a tense logic that has exactly
$\kappa $
pretabular extensions. Even though not explicitly asked in the paper, the question of the cardinals
$\aleph _0 < \kappa < 2^{\aleph _0}$
naturally arises in the same spirit as the above two open questions.
The common theme of these questions is the cardinality of classes of equational theories and logics between countable and continuum, hence they are inherently set-theoretic. It is not to be expected that standard tool kits in the field of universal algebra or modal and superintuitionistic logics could be useful for answering these kinds of questions, as they fall in the scope of ZFC, of which CH is independent. An explicit construction of uncountably many equational theories or logics typically results in constructing
$2^{\aleph _0}$
-many of such equational theories or logics.
In this paper, we apply descriptive set theory via coding to address the aforementioned three questions. The coding method aligns with the standard technique of Gödel numbers in computability theory. The idea behind the proofs is to effectively code equations (resp. formulas) by natural numbers, so that varieties (resp. logics) correspond to subsets of
$\omega $
, which in turn are identified with elements of the Cantor space
$2^\omega $
, namely, real numbers. Thus, instead of varieties or logics, we can count the corresponding sets of reals. That descriptive set theory applies in this context is no surprise, as it is exactly the theory of sets of reals. In descriptive set theory, sets of reals are classified in several hierarchies in terms of their “complexity” (see §2), and their properties are studied with respect to their complexity. The main result that we rely on in this paper is that Borel sets have cardinality either
$\leq \aleph _0$
or
$2^{\aleph _0}$
.
Therefore, all we have to do is verify that the sets of reals corresponding to the sets of equational theories and logics in question are Borel. Specifically, we show that an interval of equational theories in a countable language corresponds to a
$\boldsymbol {\Pi }^0_1$
set, and the fmp span of a modal logic to a
$\boldsymbol {\Pi }^0_2$
set. This implies that their cardinality is either
$\leq \aleph _0$
or
$2^{\aleph _0}$
, provably in ZFC, answering the open questions by Jackson and Lee [Reference Jackson and Lee12, Question 6.4(ii)] and by Bezhanishvili et al. [Reference Bezhanishvili, Bezhanishvili and Moraschini2, Sec. 8(1)] in the positive. On the other hand, we also point out that it follows from [Reference Ježek, Pudlák and Tůma16] that there is an equational theory such that its extensions form a continuum chain, which thus admits no independent system. This example provides a negative solution to [Reference Jackson and Lee12, Question 6.4(i)] in its stated generality, although it does not settle the question for monoids. Moreover, it implies that the cardinality result of intervals of equational theories cannot be shown by constructing independent systems, which explains why we need to employ the toolkit of descriptive set theory. We also observe that even though the definition of pretabularity is more involved and contains a universal quantification over logics, a more sophisticated characterization shows that the corresponding sets of reals are
$\boldsymbol {\Pi }^0_2$
. This yields a similar cardinality result and completes the cardinality characterization of pretabular tense logics in [Reference Chen7].
The paper is organized as follows. §2 recalls preliminaries on descriptive set theory, universal algebra, and modal logic. The main results are proved in §3. §4 concludes the paper with open questions.
2 Preliminaries
We work in ZFC throughout the paper.
2.1 Descriptive set theory
We assume familiarity with basic definitions of descriptive set theory. We use [Reference Jech15, Chaps. 11 and 25] and [Reference Kanamori17, Sec. 12] as our main references for descriptive set theory.
We will work with subsets of the Cantor space
$2^\omega $
, elements of which are called reals. Reals are naturally identified with subsets of
$\omega $
. For
$a \in 2^\omega $
and
$m \in \omega $
, the descriptions
$m \in a$
and
$m \notin a$
mean
$a(m) = 1$
and
$a(m) = 0$
, respectively. The Borel hierarchy (
$\boldsymbol {\Sigma }^0_\alpha $
,
$\boldsymbol {\Pi }^0_\alpha $
for
$0 < \alpha < \omega _1$
) and the arithmetical hierarchy (
$\Sigma ^0_n$
,
$\Pi ^0_n$
for
$n> 0$
) are defined as usual. For a real
$a \in 2^\omega $
, a subset
$A \subseteq 2^\omega $
is
$\Sigma ^0_n(a)$
if there is a
$\Sigma ^0_n$
formula
$\varphi (x)$
of the form
$\exists m_1 \forall m_2 \dots Q m_n R$
where all quantifiers range over
$\omega $
and R is a recursive predicate with the parameter a, such that
$b \in A$
iff
$\varphi (b)$
holds for any
$b \in 2^\omega $
. In such a case, we say that
$\varphi $
defines A. Similarly, a subset
$A \subseteq 2^\omega $
is
$\Pi ^0_n(a)$
if A is defined by a
$\Pi ^0_n$
formula with the parameter a. For example, the singleton set
$\{a\}$
for a real
$a \in 2^\omega $
is
$\Pi ^0_1(a)$
because it is defined by the formula
$\varphi (x) = \forall m (m \in x \leftrightarrow m \in a)$
. We omit the precise definition of
$\boldsymbol {\Sigma }^0_\alpha $
and
$\boldsymbol {\Pi }^0_\alpha $
, but note the following useful fact: for
$n> 0$
, a set
$A \subseteq 2^\omega $
is
$\boldsymbol {\Sigma }^0_n$
iff A is
$\Sigma ^0_n(a)$
for some
$a \in 2^\omega $
, and similarly for
$\boldsymbol {\Pi }^0_n$
.
It is well-known, provably in ZFC, that Borel (even
$\boldsymbol {\Sigma }^1_1$
) sets have the perfect set property—thus the cardinality of a Borel set is either
$\leq \aleph _0$
or
$2^{\aleph _0}$
. We will exploit this fact to obtain the main results on the cardinality of classes of varieties, equational theories, and logics.
Fact 2.1. Every Borel set has cardinality either
$\leq \aleph _0$
or
$2^{\aleph _0}$
.
2.2 Equational theories and logics
We refer to [Reference Bergman1, Reference Burris and Sankappanavar4] for basic facts of universal algebra. A language, or signature, is a set of function symbols with each arity specified. Throughout the paper, we assume that the language is countable. Given a language and a set X of variables, we define terms over X in the language in the standard way. An equation, or identity, over X is an expression of the form
$s \approx t$
, where s and t are terms over X. Following the convention, we assume X to be a countably infinite set and omit it if no confusion arises. A set
$\Phi $
of equations is an equational theory if
$\Phi $
is the set of equations valid in a variety
$\mathcal {V}$
, where a variety is a class of algebras closed under homomorphic images, subalgebras, and products. We can take the following syntactic characterization of equational theories as our working definition of equational theories in this paper (see, e.g., [Reference Burris and Sankappanavar4, Chap. 2, Definition 14.16 and Theorem 14.17]).
Definition 2.2.
-
1. For a term t and an equation $s \approx s'$
, an equation
$t \approx t'$
is a replacement instance of t and
$s \approx s'$
if
$t'$
is the result of replacing an occurrence of s in t by
$s'$
. -
2. For an equation $s \approx s'$
and a tuple of terms
$(t_1, \dots , t_n)$
, the substitution instance of
$s \approx s'$
and
$(t_1, \dots , t_n)$
is the resulting equation by simultaneously replacing every occurrence of each variable
$x_i$
in
$s \approx s'$
by
$t_i$
.
Theorem 2.3. Let
$\Phi $
be a set of equations. Then
$\mathsf {Th}(\Phi )$
, the least equational theory containing
$\Phi $
, is the least set of equations containing
$\Phi $
such that:
-
1. $s \approx s \in \mathsf {Th}(\Phi ) \text { for } s \in \mathsf {T}; $
-
2. $s \approx t \in \mathsf {Th}(\Phi )$
implies
$t \approx s \in \mathsf {Th}(\Phi );$
-
3. $s \approx t,~ t \approx u \in \mathsf {Th}(\Phi )$
implies
$s \approx u \in \mathsf {Th}(\Phi );$
-
4. $\mathsf {Th}(\Phi )$
is closed under replacement; -
5. $ \mathsf {Th}(\Phi )$
is closed under substitution.
We also recall the basics of modal logic. We refer to [Reference Blackburn, de Rijke and Venema3, Reference Chagrov and Zakharyaschev5] for a comprehensive introduction to this subject. Modal formulas are defined by the following syntax, where
$\mathsf {Prop}$
is a countable set of propositional variables:
A normal modal logic L is a set of formulas that contains all the propositional tautologies and the K axiom
$\Box (p \to q) \to \Box p \to \Box q$
, and is closed under modus ponens, necessitation, and uniform substitution. A logic L is a normal extension, or simply an extension, of another logic
$L_0$
if
$L_0 \subseteq L$
. For any logic
$L_0$
, the extensions of
$L_0$
form a complete lattice, denoted
$\mathop {\mathsf {NExt}}{L_0}$
, where the order is the subset relation
$\subseteq $
. Tense logics are defined similarly with two boxes
$\Box _0$
and
$\Box _1$
. Tense logics also contain two extra axioms
$p \to \Box _0 \lnot \Box _1 \lnot p$
and
$p \to \Box _1 \lnot \Box _0 \lnot p$
. We call normal modal logics and tense logics logics if no confusion arises.
A Kripke frame
$\mathcal {F}$
is a pair
$(F, R)$
of a nonempty set F and a binary relation
$R \subseteq F \times F$
. A valuation on
$\mathcal {F}$
is a function
$V: \mathsf {Prop} \to \mathcal {P} (F)$
. This generalizes to all formulas as follows: Boolean connectives are interpreted by Boolean operations on
$\mathcal {P} (F)$
, and
$V(\Box \varphi ) = \{x \in F: \forall y (Rxy \to y \in V(\varphi ))\}$
. We say that
$\mathcal {F}$
validates
$\varphi $
, written
$\mathcal {F} \models \varphi $
, if
$V(\varphi ) = F$
for any valuation V on
$\mathcal {F}$
. Kripke semantics for tense logics is defined analogously, where the converse relation of R is used to interpret the second modality.
3 Main results
The core idea behind the proofs in this section is coding. If the language
$\mathcal {L}$
is countable, then there are only countably many equations. These equations can be effectively coded by natural numbers relative to an oracle for
$\mathcal {L}$
, corresponding to the arity map of the function symbols in
$\mathcal {L}$
. For instance, one may employ a standard Gödel numbering based on prime factorization or a pairing function. Then, the set
$\mathsf {Eq} = \{i \in \omega : i \text { is a code of an equation in } \mathcal {L}\}$
is recursive in
$\mathcal {L}$
. Let
$\varphi _i$
denote the equation with code i. Equational theories
$\Phi $
then correspond to particular kinds of elements
$A \in 2^\omega $
, i.e., infinite
$0$
–
$1$
sequences, in such a way that
$A(i) = 1$
iff
$\varphi _i \in \Phi $
. These will be the reals coding set of sentences satisfying some basic properties, such as the inclusion of all identities
$s \approx s$
and closure under substitutions. In that case, we also call A the code of
$\Phi $
. We will be loose on the distinction between an equational theory and its code if there is no confusion. As every equational theory has a unique code, instead of counting equational theories, we can count elements of
$2^\omega $
, i.e., reals, where descriptive set theory applies. If we can show that the set of reals corresponding to a class of equational theories is in a specific complexity class, such as Borel, we can draw from descriptive set theory consequences on the cardinality of that class of equational theories. Since in modal logic the language is finite, it falls under a special case of the above observation.
We start with intervals of equational theories. Let
$\mathsf {T}$
and
$\mathsf {Eq}$
, respectively, be the sets of codes of all terms and equations. Let
$\Phi _0$
and
$\Phi _1$
be equational theories. Recall that the interval between
$\Phi _0$
and
$\Phi _1$
is the set
An interval in this sense may not be linearly ordered. Since each equational theory corresponds to a real, we can view an interval of equational theories as a set of reals. So, it is meaningful to talk about the complexity hierarchy of an interval of equational theories. Recall that for
$A, B \subseteq \omega $
, the join
$A \oplus B \subseteq \omega $
is the set
Intuitively, using the parameter
$A \oplus B$
amounts to using the parameters A and B.
Lemma 3.1. The set
$[\Phi _0, \Phi _1]$
is
$\Pi ^0_1(\Phi _0 \oplus \Phi _1)$
.
Proof. A set
$\Phi \subseteq \omega $
is in
$[\Phi _0, \Phi _1]$
iff each element in
$\Phi $
indeed codes an equation,
$\Phi $
is an equational theory, and
$\Phi _1\subseteq \Phi \subseteq \Phi _2$
. A set of equations is an equational theory iff it satisfies the five conditions in Theorem 2.3. Thus,
$\Phi \in [\Phi _0, \Phi _1]$
iff it satisfies all the following conditions:
-
1. $\Phi \subseteq \mathsf {Eq}$
; -
2. $s \approx s \in \Phi \text { for } s \in \mathsf {T}; $
-
3. $s \approx t \in \Phi \Rightarrow t \approx s \in \Phi ;$
-
4. $s \approx t,~ t \approx u \in \Phi \Rightarrow s \approx u \in \Phi ;$
-
5. $\Phi \text { is closed under replacement};$
-
6. $\Phi \text { is closed under substitution};$
-
7. $\Phi _0 \subseteq \Phi \subseteq \Phi _1$
.
We show that all these conditions can be expressed by
$\Pi ^0_1$
formulas, with the parameters
$\Phi _0$
and
$\Phi _1$
. We only address items (5) and (7). The others can be verified in a similar manner. First, observe that
$\mathsf {T}$
and
$\mathsf {Eq}$
are recursive in
$\Phi _0$
, since
$\Phi _0$
serves as an oracle that takes any natural number as input (the same applies to
$\Phi _1$
). For instance, t is a well-founded term iff
$t \approx t \in \Phi _0$
. Also, it follows from Definition 2.2 that the ternary relation “
$\varphi '$
is a replacement instance of t and
$\varphi $
” is recursive. So, using a recursive predicate
$\mathsf {Rep}$
, item (5) can be expressed by the
$\Pi ^0_1$
formula with the parameter
$\Phi _0$
(hidden in
$\mathsf {T}$
):
Item (7) can be expressed by the
$\Pi ^0_1$
formula with parameters
$\Phi _0$
and
$\Phi _1$
:
Thus, the set
$[\Phi _0, \Phi _1]$
can be defined by a
$\Pi ^0_1$
formula with parameters
$\Phi _0$
and
$\Phi _1$
, hence it is
$\Pi ^0_1(\Phi _0 \oplus \Phi _1)$
.
Lemma 3.2. For any equational theories
$\Phi _0$
and
$\Phi _1$
, the interval
$[\Phi _0, \Phi _1]$
has cardinality
$\leq \aleph _0$
or
$2^{\aleph _0}$
.
Proof. The interval
$[\Phi _0, \Phi _1]$
is
$\Pi ^0_1(\Phi _0 \oplus \Phi _1)$
by Lemma 3.1, so it is
$\boldsymbol {\Pi }^0_1$
, and hence Borel. Thus, it has cardinality
$\leq \aleph _0$
or
$2^{\aleph _0}$
by Fact 2.1.
Lemma 3.3. Every equational theory has
$\leq \aleph _0$
or
$2^{\aleph _0}$
many extensions.
Proof. This follows from Lemma 3.2 by taking
$\Phi _1$
to be the set of all equations.
Theorem 3.4. Every variety in a countable language has
$\leq \aleph _0$
or
$2^{\aleph _0}$
many subvarieties.
Proof. By Birkhoff’s theorem (see, e.g., [Reference Bergman1, Theorem 4.11] and [Reference Burris and Sankappanavar4, Theorem 11.9]) that a class of algebras is a variety iff it is equationally definable, there is a one-to-one correspondence between varieties and equational theories. Thus, we can reformulate Lemmas 3.2 and 3.3 in terms of varieties: if the language is countable, then for any varieties
$\mathcal {V}_0$
and
$\mathcal {V}_1$
, the interval
$[\mathcal {V}_0, \mathcal {V}_1]$
has cardinality
$\leq \aleph _0$
or
$2^{\aleph _0}$
; in particular, every variety has
$\leq \aleph _0$
or
$2^{\aleph _0}$
many subvarieties.
This answers the open question [Reference Jackson and Lee12, Question 6.4(ii)] in the affirmative.
Remark 3.5. Jackson and Lee also raised a second problem: Does every variety with uncountably many subvarieties have an independent system extending its equational theory [Reference Jackson and Lee12, Question 6.4(i)]? An independent system extending an equational theory
$\Phi $
is an infinite set
$\Psi $
of equations such that every subset
$\Psi ' \subseteq \Psi $
induces a distinct equational theory
$\mathsf {Th}(\Phi \cup \Psi ')$
. Note that a positive answer to this question would also yield the conclusion of Theorem 3.4, as we can construct
$2^{\aleph _0}$
many equational theories from
$2^{\aleph _0}$
many subsets of
$\Psi $
. However, we provide a negative answer to this question as follows.
We refer to [Reference Bergman1, Reference Burris and Sankappanavar4] for the necessary background on universal algebra. It follows from [Reference Ježek, Pudlák and Tůma16, Theorem 3.1] that every completely distributive algebraic lattice with compact top is isomorphic to the lattice of extensions of an equational theory. Let
$S = \mathbb {Q} \cap [0, 1]$
and L be the set of all downsets in S ordered by inclusion. Then L is a complete chain with size
$2^{\aleph _0}$
, in particular, a completely distributive lattice, where
$\bigvee = \bigcup $
and
$\bigwedge = \bigcap $
. If, for a rational
$q \in \mathbb {Q}$
, the principal downset
${\downarrow } q \subseteq \bigcup _{i \in I} D_i$
for some
$\{D_i\}_{i \in I} \subseteq L$
, then
$q \in D_i$
for some
$i \in I$
, and thus
${\downarrow } q \subseteq D_i$
. So, each principal downset
${\downarrow } q$
for
$q \in \mathbb {Q}$
is a compact element in L. In particular, the top element
${\downarrow } 1$
is compact. Moreover, every downset
$D \in L$
is the union
$\bigcup _{q \in D} {\downarrow } q$
of compact elements below D, so L is an algebraic lattice. Thus, by [Reference Ježek, Pudlák and Tůma16, Theorem 3.1], there is an equational theory T such that
$\mathop {\mathsf {Ext}}{T}$
is isomorphic to L. Then,
$|\mathop {\mathsf {Ext}}{T}| = |L| = 2^{\aleph _0}$
, while there are no equations
$\varphi , \psi $
such that
$\mathsf {Th}(T + \varphi )$
and
$\mathsf {Th}(T + \psi )$
are incomparable, so there are no equations
$\varphi , \psi $
such that
$\mathsf {Th}(T + \varphi )$
,
$\mathsf {Th}(T + \psi )$
, and
$\mathsf {Th}(T + \{\varphi , \psi \})$
are pairwise distinct, hence there is no independent system extending T. This yields a negative answer to [Reference Jackson and Lee12, Question 6.4(i)]. However, it follows from the proofs in [Reference Ježek, Pudlák and Tůma16] that T is in a countably infinite language, so the question remains open in the intended setting of Jackson and Lee (i.e., monoids).
Note that this example also shows that the cardinality result of Theorem 3.4 cannot be proved by constructing independent systems, thus ruling out the standard methods of Jankov formulas and their variants. Such approaches would fail to show that the variety corresponding to T has
$2^{\aleph _0}$
many subvarieties. This further explains why we had to employ the toolkit of descriptive set theory.
Next, we present an application of our method to logics and study the degrees of the finite model property (degrees of fmp for short). The degrees of fmp were introduced in [Reference Bezhanishvili, Bezhanishvili and Moraschini2] as a modified version of the degrees of Kripke incompleteness [Reference Fine11] using finite Kripke frames. We first recall the definition for modal logics; the case of superintuitionistic logics is analogous. Let
$L_0$
be a logic.
Definition 3.6. Let
$\mathsf {FFr}$
be the class of all finite Kripke frames. For
$L \in \mathop {\mathsf {NExt}}{L_0}$
, let
and the fmp span of L (in
$\mathop {\mathsf {NExt}}{L_0}$
) be the set
The degree of fmp of L (in
$\mathop {\mathsf {NExt}}{L_0}$
) is the cardinality of the set
$\mathrm {fmp}_{L_0}(L)$
.
The condition
$\mathsf {FFr}(L) = \mathsf {FFr}(L')$
induces an equivalence relation on the lattice
$\mathop {\mathsf {NExt}}{L_0}$
, and the fmp span of L refers to the equivalence class that L belongs to. Thus, intuitively, the degree of fmp of L measures the extent to which L cannot be distinguished from other logics by the means of finite Kripke frames. It was proved in [Reference Bezhanishvili, Bezhanishvili and Moraschini2] that every cardinal
$0 < \kappa \leq \aleph _0$
or
$\kappa = 2^{\aleph _0}$
is realized as the degree of fmp for superintuitionistic logics and transitive modal logics. So, the question naturally arises whether any cardinal between
$\aleph _0$
and
$2^{\aleph _0}$
is also realized as the degree of fmp for some logic. We show that this cannot be the case.
Lemma 3.7. For any logic
$L \in \mathop {\mathsf {NExt}}{L_0}$
, the set
$\mathrm {fmp}_{L_0}(L)$
is
$\Pi ^0_2 (L_0 \oplus L)$
.
Proof. By Lemma 3.1, there is a
$\Pi ^0_1$
formula
$\alpha $
with the parameter
$L_0$
that defines
$\mathop {\mathsf {NExt}}{L_0}$
.
A finite Kripke frame is a finite set with a binary relation. Given a finite Kripke frame
$\mathcal {F}$
and a formula
$\varphi $
, it is decidable whether
$\mathcal {F} \models \varphi $
by considering all possible valuations on
$\mathcal {F}$
of propositional variables occurring in
$\varphi $
. So, finite Kripke frames (up to isomorphism) can be recursively coded by natural numbers such that: the validity relation
is recursive.
For any
$L \in \mathop {\mathsf {NExt}}{L_0}$
and
$L' \subseteq \omega $
, we have
$L' \in \mathrm {fmp}_{L_0}(L)$
iff
$L'$
satisfies
$\alpha $
and the formula
which is readily verified to be a
$\Pi ^0_2$
formula with the parameter L. Thus, the set
$\mathrm {fmp}_{L_0}(L)$
is defined by
$\alpha \land \beta $
, which is a
$\Pi ^0_2$
formula with the parameters
$L_0$
and L. Hence, the set
$\mathrm {fmp}_{L_0}(L)$
is
$\Pi ^0_2(L_0 \oplus L)$
.
Theorem 3.8. For any normal modal logic
$L_0$
and
$L \in \mathop {\mathsf {NExt}}{L_0}$
, the degree of fmp of L in
$\mathop {\mathsf {NExt}}{L_0}$
is either
$\leq \aleph _0$
or
$2^{\aleph _0}$
.
Remark 3.9. It is straightforward to modify the proofs of Lemma 3.7 and Theorem 3.8 and prove similar results for superintuitionistic logics.
Theorem 3.8 shows that we can obtain complete antidichotomy results for the degrees of fmp without using the CH, answering the question posed in [Reference Bezhanishvili, Bezhanishvili and Moraschini2, Sec. 8(1)].
Remark 3.10. It was observed in [Reference Bezhanishvili, Bezhanishvili and Moraschini2] that for transitive modal and superintuitionistic logics, the fmp span is always an interval. So, in fact, Lemma 3.2, applied to transitive modal and superintuitionistic logics, already answers question [Reference Bezhanishvili, Bezhanishvili and Moraschini2, Sec. 8(1)]. We still provided a direct proof, since we believe it is more informative. Moreover, our result applies to all modal logics, whereas the fact that the fmp span is an interval was shown in [Reference Bezhanishvili, Bezhanishvili and Moraschini2] only for transitive modal and superintuitionistic logics.
Finally, we apply our method to study classes of tense logics that are not intervals. A tense logic L is tabular if it is characterized by a single finite Kripke frame, that is, there is a finite Kripke frame
$\mathcal {F}$
such that for any formula
$\varphi $
,
$\varphi \in L$
iff
$\mathcal {F} \models \varphi $
. A tense logic is pretabular if it is not tabular while all its proper consistent extensions are tabular. See [Reference Chagrov and Zakharyaschev5, Chap. 12] for details on tabular and pretabular logics. For a tense logic L, let
$\mathsf {PTAB}(L)$
be the set of pretabular extensions of L.
Recently, Chen [Reference Chen7] showed that for each cardinal
$\kappa \leq \aleph _0$
and
$\kappa = 2^{\aleph _0}$
, there is a tense logic L extending
$\mathsf {S4}_t$
such that L has
$\kappa $
many pretabular extensions. Given this kind of antidichotomy theorem, similar to the case of the degree of fmp, it is natural to ask if there is a tense logic that has
$\kappa $
many pretabular extensions for
$\aleph _0 < \kappa < 2^{\aleph _0}$
. Contrary to intervals and fmp spans, by naively interpreting the definition of pretabularity, we would obtain a rather high upper bound for the complexity of
$\mathsf {PTAB}(L)$
, namely
$\boldsymbol {\Pi }^1_1$
, as the definition contains a universal quantification over logics. It is consistent with Zermelo–Frankel set theory that there exists a
$\boldsymbol {\Pi }^1_1$
set A whose cardinality satisfies
$\aleph _0 < |A| < 2^{\aleph _0}$
. For instance, this will hold in Cohen’s [Reference Cohen9] original model for the negation of the CH, obtained by forcing over Gödel’s constructible universe L. Let A be the set of all real numbers
$x\in \mathbb {R}$
such that
$x \in L_\alpha $
for some x-computable ordinal
$\alpha $
, where
$L_\alpha $
denotes the
$\alpha $
th stage of Gödel’s constructible hierarchy. In this model, A satisfies
$|A| = \aleph _1 < \aleph _2 = 2^{\aleph _0}$
.
However, a more sophisticated characterization can bring the complexity down to
$\boldsymbol {\Pi }^0_2$
, where Fact 2.1 applies. The following fact was proved in [Reference Chagrov, Shehtman, Goos, Hartmanis, Van Leeuwen, Pacholski and Tiuryn6, Lemma 11] and [Reference Chen and Ma8, Theorem 3.7].
Fact 3.11. There is a set of formulas
$\{\mathsf {tab}_n: n \in \omega \}$
such that for any consistent tense logic
$L'$
, we have that
$L'$
is tabular iff
$\mathsf {tab}_n \in L'$
for some
$n \in \omega $
. Moreover, the codes of
$\mathsf {tab}_n$
’s are computable from n.
Lemma 3.12. For any tense logic L, we have that L is pretabular iff it is not tabular while all its proper consistent finitely axiomatizable extensions are tabular.
Proof. It suffices to prove the right-to-left direction, as the other direction is clear by the definition. Assume for a contradiction that L is not pretabular, L is not tabular, and all its consistent finitely axiomatizable extensions are tabular. Then, L has some proper consistent non-tabular extension
$L'$
, which is not finitely axiomatizable. So, there is some
$\varphi \in L'$
such that
$\varphi \notin L$
. Since the logic
$L + \varphi $
is a proper consistent extension of L, it is tabular, and thus contains
$\mathsf {tab}_n$
for some
$n \in \omega $
by Fact 3.11. It follows that
$\mathsf {tab}_n \in L'$
, which contradicts the assumption that
$L'$
is not tabular. Therefore, we conclude the right-to-left direction of the statement.
Lemma 3.13. For any tense logic L, the set
$\mathsf {PTAB}(L)$
is
$\Pi ^0_2(L)$
.
Proof. Similar to the proof of Lemma 3.7, we can code formulas in tense logic and finite Kripke frames so that the validity relation is recursive. We use the same notation
$\mathsf {Fml}$
for the set of formulas. Also, by the proof of Lemma 3.1, there is a
$\Pi ^0_1$
formula
$\alpha (X)$
with the parameter L that defines
$\mathop {\mathsf {NExt}}{L}$
. Let f be the recursive function computing the code of
$\mathsf {tab}_n$
in Fact 3.11 from n.
Tense logics have the same Hilbert-style proof system as bimodal logics, naturally extending that of unimodal logics (see, e.g., [Reference Blackburn, de Rijke and Venema3, Sec. 1.6] and [Reference Chagrov and Zakharyaschev5, Sec. 3.6]). Thus, proofs in tense logics can be coded in a standard way, yielding a recursive predicate
$\mathsf {Proof}$
such that
$\mathsf {Proof}(A, i, p, j)$
iff p is the code of a proof of the formula
$\varphi _j$
in the logic
$L_A + \varphi _i$
.
By Lemma 3.12, for any tense logic
$L'$
, we have that
$L' \in \mathsf {PTAB(L)}$
iff
$L' \in \mathop {\mathsf {NExt}}{L}$
,
$L'$
is not tabular, and for any formula
$\varphi $
, either
$L' + \varphi = L'$
,
$L' + \varphi $
is tabular, or
$L' + \varphi $
is the inconsistent logic, translating into the following formula:
where b is the code of
$\bot $
. Since this formula is
$\Pi ^0_2$
with the parameter L, the set
$\mathsf {PTAB}(L)$
is
$\Pi ^0_2(L)$
.
Theorem 3.14. For any tense logic L, the cardinality of the set of pretabular extensions of L is either
$\leq \aleph _0$
or
$2^{\aleph _0}$
.
4 Conclusion and future research
In this paper, we applied descriptive set theory to study the cardinality of classes of equational theories and logics via coding. The cardinality results were formulated for equational theories, varieties, modal logics, and tense logics to match each specific setting. However, the idea of coding applies to any formal system with a reasonable syntax such as Theorem 2.3. For instance, the cardinality result of intervals (Lemma 3.2) also holds for quasivarieties and universal classes. Moreover, Theorem 3.14 holds for modal logics as well because of a characterization of tabular modal logics similar to Fact 3.11 (see, e.g., [Reference Chagrov and Zakharyaschev5, Corollary 12.2]). In practice, such results are of interest only if there is some sort of antidichotomy result for cardinals
$\leq \aleph _0$
and
$2^{\aleph _0}$
.
A concrete open question is discussed in Remark 3.5, namely [Reference Jackson and Lee12, Question 6.4(i)] in the setting of finite languages, and specifically in the setting of monoids. We also mention two limitations of our method. An obvious one is that it heavily relies on coding. Therefore, the method works only if everything involved (e.g., equations, formulas, and finite Kripke frames) can be effectively and uniquely coded. For example, this is not the case for Kripke frames, which form a proper class. We leave it for future research to apply this method to count Kripke complete logics or the degree of Kripke incompleteness [Reference Fine11].
Another point is that the perfect set property is just one of the regular properties that Borel sets enjoy. Other regular properties include Lebesgue measurability and the Baire property. But these do not have immediate consequences for equational theories or logics. We leave it for future research to obtain results for classes of equational theories or logics, other than determining their cardinalities, by using the complexity of their corresponding sets of reals.
Acknowledgments
We are very grateful to George Metcalfe, Simon Santschi, and Niels Vooijs for pointing us to the open questions in [Reference Jackson and Lee12]. We would also like to thank Yurii Khomskii for valuable comments on an early draft of the paper. We are also grateful to the two anonymous reviewers for their careful reading and helpful suggestions.
Funding
The first author would like to acknowledge the support of the Austrian Science Foundation (FWF) through grants 10.55776/STA139 and 10.55776/ESP3. The third author would like to acknowledge the support of the Student Exchange Support Program of the Japan Student Services Organization and the Student Award Scholarship of the Foundation for Dietary Scientific Research. Open access funding provided by University of Amsterdam.
Open access
