1. Introduction
Definition 1.1. Take a first-order language
$\mathcal {L}$
, a finite
$\mathcal {L}$
-structure M, and an
$\mathcal {L}$
-formula
$\varphi (x_1,\dots ,x_n)$
in n free variables. We call the quantity
$$ \begin{align*} \frac{ \left \vert \left\{ {(a_1, \dots, a_n) \in M^n}\:\middle \vert \:{\varphi(a_1, \dots,a_n)} \right\} \right \vert }{ \vert M \vert ^n }\end{align*} $$
the degree of satisfiability of the formula
$\varphi $
in the structure M, and denote it
$\operatorname {\mathrm {\mathbf {ds}}}_M(\varphi )$
.
Definition 1.2. Take a theory T over a first-order language
$\mathcal {L}$
, along with an
$\mathcal {L}$
-formula
$\varphi $
. If we can find a constant
$\varepsilon> 0$
such that for every finite model M of the theory T, we have either:
-
1.
$\operatorname {\mathrm {\mathbf {ds}}}_M(\varphi ) = 1$
; or else -
2.
$\operatorname {\mathrm {\mathbf {ds}}}_M(\varphi ) \leq 1 - \varepsilon ,$
then we say that the formula
$\varphi $
has finite satisfiability gap
$\varepsilon $
in T.
A classic result of Gustafson [Reference Gustafson9] states that in a finite non-Abelian group G,
$\operatorname {\mathrm {\mathbf {ds}}}_G(xy=yx)$
cannot exceed
$\frac {5}{8}$
. In particular, “deceptive” groups, which only barely fail to be Abelian, do not exist. The seminal work of Antolín, Martino, and Ventura [Reference Antolín, Martino and Ventura1], generalizing Gustafson’s result to a class of finitely generated groups, boosted collective interest in finite gap properties of other group-theoretic equations and formulae: in the last few years, tight finite gap bounds have been obtained for the nested simple commutator equation [Reference Lescot13], the 2-Engel and metabelian identities [Reference Delizia, Jezernik, Moravec and Nicotera7], the equations
$xy^2=y^2x$
and
$xy^3=y^3x$
[Reference Kocsis11], and others. The existence of an equation in the language of group theory that does not have finite satisfiability gap remains open, even in the case of equations in only one free variable. An elementary argument shows that
$x^2 = 1$
has finite satisfiability gap
$\frac {1}{4}$
, and Laffey [Reference Laffey12] established a finite gap of
$\frac {2}{9}$
for
$x^3 = 1$
. For
$x^p = 1$
with
$p \geq 5$
, only partial results are known.
1.1. Degrees of classicality
Recall that a Heyting algebra
$\langle H, \wedge , \vee , \rightarrow , \bot , \top \rangle $
is a bounded distributive lattice where for every two elements
$a, b \in H$
, the set
$\left \{ {c \in H}\:\middle \vert \:{a \wedge c \leq b} \right \}$
has a distinguished maximum element denoted
$a \rightarrow b$
. We introduce
$\neg x$
as shorthand for
$x \to \bot $
. A Boolean algebra is a Heyting algebra
$\langle H, \wedge , \vee , \bot , \top \rangle $
in which
$x \to y = \neg x \lor y$
for all
$x, y \in H$
. We will assume that
$\bot \neq \top $
throughout this article, since the trivial Heyting algebra satisfies every equation.
The main significance of Heyting algebras is that they provide the natural algebraic semantics for (the propositional fragment of) intuitionistic logic. We leverage this correspondence multiple times throughout this paper, by freely identifying propositional formulae of intuitionistic logic with first-order terms in the language of Heyting algebras. Recall that a propositional formula
$\varphi $
is provable in intuitionistic logic precisely if
$H \models (\varphi = \top )$
for every Heyting algebra H.
Definition 1.3. Consider the language
$\langle \wedge , \vee , \rightarrow , \bot , \top \rangle $
of Heyting algebras. We call an equation
$\varphi $
a classical principle if a Heyting algebra H satisfies
$H \models \varphi $
precisely when H is a Boolean algebra.
Notice that an equation
$f = \top $
constitutes a classical principle precisely if adding f as an axiom to the standard Hilbert calculus for intuitionistic propositional logic yields a Hilbert calculus whose tautologies are those of classical propositional logic.
Example 1.4. The following are well-known classical principles:
-
1.
$x \vee \neg x = \top $
(the law of excluded middle), -
2.
$\neg \neg x = x$
(double-negation elimination), -
3.
$(x \rightarrow y) \rightarrow x = x$
(Peirce’s law), -
4.
$\neg y \rightarrow \neg x = x \rightarrow y$
(contrapositive principle), -
5.
$(\neg x \to y) \to ((x \to y) \to y) = \top $
(LEM - eliminator form), -
6.
$x \rightarrow y = \neg x \vee y$
(material implication).
In what follows, we investigate the degree of satisfiability of formulae in Heyting algebras. We give a complete classification of all equations in one free variable with respect to finite satisfiability gap in Section 2 (as discussed previously, an analogous classification for equations in groups remains elusive). In particular, we obtain that the law of excluded middle,
$x \vee \neg x = \top $
, either holds for all x, or for no more than
$\frac {2}{3}$
of all x. While the poorly understood structure of free Heyting algebras makes a similar classification for two-variable equations unlikely, we provide a thorough treatment of the classical principles enumerated above, along with some results that can be used to establish (the lack of) finite gap in many two-variable cases (Section 3). Finally, we generalize the classification of one variable equations to infinite Heyting algebras (Section 4), and present applications of our results in point-set topology (Corollary 4.8), in black-box algebras (Section 5), and in the philosophy of logic (Section 6).
1.2. Technical preliminaries
Definition 1.5. For a natural number n, the symbol
$[n]$
denotes the subset
$\{1,2,\dots , n\}$
of the naturals.
Definition 1.6. The upset of an element x in a Heyting algebra H (or any poset) is the set
$\left \{ {y \in H}\:\middle \vert \:{y \geq x} \right \}$
, which we denote by
$\uparrow _H x$
(or simply
$\uparrow x$
if H is clear from context).
Definition 1.7. Given a Heyting algebra H with bottom element
$\bot $
and top element
$1$
, the Heyting algebra
$H \oplus \top $
is the Heyting algebra obtained from H by adding a new element
$\top $
to H and the relation
$\top \geq x$
for all
$x \in H$
. The operation of adjoining a k-chain to H is denoted
$H \oplus _{k} \top $
and is defined recursively as
$H \oplus _{k} \top := (H \oplus _{k -1} \top ) \oplus \top $
.
Proposition 1.8. Every finite system of equations in the language of Heyting algebras is equivalent to some equation of the form
$\varphi = \top $
.
Proof Let
$a,b$
denote arbitrary terms in the language of Heyting algebras. Use the fact that
$a = b$
precisely if
$a \rightarrow b = \top $
and
$b \rightarrow a = \top $
, along with the fact that
$a = \top $
and
$b = \top $
hold precisely if
$a \wedge b = \top $
holds, to reduce the system to a single equation in the given form.
In accordance with Proposition 1.8, a complete classification of all equations in a given number of variables with respect to degree of satisfiability immediately induces a corresponding classification for all finite systems of equations as well.
Proposition 1.9. Consider an algebraic theory T over a language
$\mathcal {L}$
. For any two models
$H,J$
of T,
$H \times J$
is also a model of T. Moreover, when H and J are finite, the equality
$$ \begin{align*}\operatorname{\mathrm{\mathbf{ds}}}_{H \times J}{\varphi} = \operatorname{\mathrm{\mathbf{ds}}}_{H}{\varphi} \times \operatorname{\mathrm{\mathbf{ds}}}_{J}{\varphi}\end{align*} $$
holds for any
$\mathcal {L}$
-equation
$\varphi $
.
Proposition 1.9 does not generalize to arbitrary formulae in the language of Heyting algebras. Consider the join-irreducibility formula
$\varphi \leftrightarrow \forall y, z. (x = y \vee z) \rightarrow (x = y) \vee (x = z)$
. In a Boolean algebra, only
$\bot $
and atoms are join-irreducible, so
$\varphi $
has degree of satisfiability
$1$
in the 2-element Boolean algebra, degree of satisfiability
$\frac {3}{4}$
in the 4-element Boolean algebra, but degree
$\frac {1}{2} \neq 1 \cdot \frac {3}{4}$
in the 8-element Boolean algebra.
1.3. Excluded-middle and double-negation-elimination
Definition 1.10. Take a Heyting algebra H. We let
$\operatorname {\mathrm {\mathbf {EM}}}_H$
denote the center of H, i.e., the set
$\left \{ {x \in H}\:\middle \vert \:{x \vee \neg x = \top } \right \}$
of elements that satisfy the law of excluded middle. Similarly, we let
$\operatorname {\mathrm {\mathbf {DN}}}_H$
denote the set
$\left \{ {x \in H}\:\middle \vert \:{\neg \neg x = x} \right \}$
of elements that satisfy double-negation elimination.
Since the sets
$\operatorname {\mathrm {\mathbf {EM}}}_H$
and
$\operatorname {\mathrm {\mathbf {DN}}}_H$
are of particular importance to us, we take a few moments to establish and/or recall some of their simple properties.
Proposition 1.11. For any Heyting algebra H, the set
$\operatorname {\mathrm {\mathbf {EM}}}_H$
is a sub-algebra of
$H;$
in fact it is a Boolean algebra and, for every other Boolean sub-algebra B of H, we have
$B \subseteq \operatorname {\mathrm {\mathbf {EM}}}_H$
.
Theorem 1.12 (Glivenko [Reference Glivenko8]).
The subposet
$\operatorname {\mathrm {\mathbf {DN}}}_H$
of a Heyting algebra H always forms a Boolean algebra
$;$
furthermore, it is a
$\wedge $
-subsemilattice of H.
The containment
$\operatorname {\mathrm {\mathbf {EM}}}_H \subseteq \operatorname {\mathrm {\mathbf {DN}}}_H$
holds in any Heyting algebra H. Moreover, if
$\operatorname {\mathrm {\mathbf {EM}}}_H \neq \operatorname {\mathrm {\mathbf {DN}}}_H$
, then Proposition 1.11 along with Theorem 1.12 gives that
$\operatorname {\mathrm {\mathbf {DN}}}_H$
cannot be a sub-algebra of H.
Proposition 1.13. Let H be a finite Heyting algebra. If
$\operatorname {\mathrm {\mathbf {ds}}}_H(x \lor \neg x = \top ) \geq 1/2$
, then
$\operatorname {\mathrm {\mathbf {EM}}}_H = \operatorname {\mathrm {\mathbf {DN}}}_H$
.
Proof Since
$\operatorname {\mathrm {\mathbf {EM}}}_H$
and
$\operatorname {\mathrm {\mathbf {DN}}}_H$
are both Boolean algebras, we can find numbers
$n,m \in \mathbb {N}$
such that
$ \vert \operatorname {\mathrm {\mathbf {EM}}}_H \vert = 2^n$
and
$ \vert \operatorname {\mathrm {\mathbf {DN}}}_H \vert = 2^m$
. Since
$\operatorname {\mathrm {\mathbf {EM}}}_H \subseteq \operatorname {\mathrm {\mathbf {DN}}}_H$
, we must have either
$n = m$
(as desired) or
$$\begin{align*}\vert \operatorname{\mathrm{\mathbf{DN}}}_H \vert \geq 2 \vert \operatorname{\mathrm{\mathbf{EM}}}_H \vert = 2 \operatorname{\mathrm{\mathbf{ds}}}_H(x \lor \neg x = \top) \vert H \vert \geq \vert H \vert .\end{align*}$$
This means that
$\operatorname {\mathrm {\mathbf {DN}}}_H = H$
and so double-negation elimination holds everywhere. But then H is a Boolean algebra which implies that the law of excluded middle holds everywhere as well; in other words
$\operatorname {\mathrm {\mathbf {DN}}}_H = H = \operatorname {\mathrm {\mathbf {EM}}}_H$
, as desired.
We note that the
$\frac {1}{2}$
bound obtained in Proposition 1.13 is not tight. A tight bound (
$\frac {2}{5}$
) follows immediately from Theorem 6.1 in Section 6, using the fact that the smallest Heyting algebra H with
$\operatorname {\mathrm {\mathbf {DN}}}_H \not \subseteq \operatorname {\mathrm {\mathbf {EM}}}_H$
has five elements.
2. Equations in one free variable
In this section we classify all equations in one free variable into two classes: those equations which have finite satisfiability gap and those which do not. The main result of this section, Theorem 2.11, states that (up to logical equivalence of first-order formulae) only three equations,
$p = \top , p = \bot $
, and
$p \vee \neg p = \top $
belong to the first class.
Proposition 2.1. The equations
$p = \top $
and
$\neg p = \top $
have finite satisfiability gap
$1/2$
.
Proof Since every Heyting algebra H has at least two elements, we have that
$$ \begin{align*}\operatorname{\mathrm{\mathbf{ds}}}_{H}(p = \top) = \frac{ \left \vert \left\{ {y \in H}\:\middle \vert \:{y = \top} \right\}\right \vert }{ \vert H \vert } = \frac{1}{ \vert H \vert } \leq \frac{1}{2}.\end{align*} $$
Similarly, noticing that
$\neg p = \top $
holds only if
$p = \bot $
, we get that
$\operatorname {\mathrm {\mathbf {ds}}}_{H}(\neg p = \top ) \leq \frac {1}{2}$
as well. Both of these gaps are realized in the Heyting algebra with two elements.
To establish an analogous result for the law of excluded middle (Theorem 2.2), we will argue inductively on the multiplicative structure of Heyting algebras by making use of Proposition 1.9 (recall that this relates the degree of satisfiability of an equation in a product of Heyting algebras to its degree of satisfiability in the factors).
Theorem 2.2. The equation
$p \vee \neg p = \top $
has finite satisfiability gap
$1/3$
.
Proof We proceed by simultaneous induction on the number of elements of the finite algebra H and the number of elements of the set
$\operatorname {\mathrm {\mathbf {EM}}}_H$
. In the base case, the algebra H satisfies
$ \vert \operatorname {\mathrm {\mathbf {EM}}}_H \vert = 2$
. Consequently,
$\operatorname {\mathrm {\mathbf {ds}}}_H(p \vee \neg p = \top ) = \frac {2}{ \vert H \vert }$
, which is either
$1$
or at most
$\frac {2}{3}$
, as desired.
In the inductive case, the algebra H has
$ \vert \operatorname {\mathrm {\mathbf {EM}}}_H \vert> 2$
. Since
$ \vert \operatorname {\mathrm {\mathbf {EM}}}_H \vert> 2$
, we can find some
$c \in \operatorname {\mathrm {\mathbf {EM}}}_H$
such that
$c \neq \bot $
and
$c \neq \top $
. Consider the subposet
$H_c = \left \{ {x \in H}\:\middle \vert \:{x \leq c} \right \}$
of H. This clearly forms a Heyting algebra with the order inherited from H.
Define the map
$f:H \to H_c \times H_{\neg c}$
by
$f(x)=(x \wedge c, x \wedge \neg c)$
. Then f is clearly a bounded lattice homomorphism. It is injective because, if
$f(x) = f(y)$
, then
$$\begin{align*}x = x \wedge \top = x \wedge (c \vee \neg c ) = (x \wedge c) \vee (x \wedge \neg c) = (y \wedge c) \vee (y \wedge \neg c) = y. \end{align*}$$
Moreover, f is surjective because if
$(a,b) \in H_c \times H_{\neg c}$
, then
$$ \begin{align*} f(a \vee b) &= ((a \vee b) \wedge c, (a \vee b) \wedge \neg c)\\ &=((a \wedge c) \vee (b \wedge c), (a \wedge \neg c) \vee (b \wedge \neg c)) \\ &=(a \vee (b \wedge c), (a \wedge \neg c) \vee b) \\ &= (a \vee \bot, \bot \vee b) &(\text{since } c \text{ is in the center})\\ &=(a,b). \end{align*} $$
By the finiteness of H, it follows that f preserves implications as well, and is therefore a Heyting algebra isomorphism.
Since
$ \vert H_c \vert < \vert H \vert $
and
$ \vert H_{\neg c} \vert < \vert H \vert $
, the inductive hypothesis applies, and gives us that either
$\operatorname {\mathrm {\mathbf {ds}}}_{H_c}(p \vee \neg p = \top ) = 1$
and
$\operatorname {\mathrm {\mathbf {ds}}}_{H_{\neg c}}(p \vee \neg p = \top ) = 1$
both hold, or at least one of
$\operatorname {\mathrm {\mathbf {ds}}}_{H_c}(p \vee \neg p = \top ) \leq \frac {2}{3}$
or
$\operatorname {\mathrm {\mathbf {ds}}}_{H_{\neg c}}(p \vee \neg p = \top ) \leq \frac {2}{3}$
holds. In either case, applying Proposition 1.9 concludes the proof.
The
$\frac {1}{3}$
bound for the satisfiability gap of the equation
$x \vee \neg x = \top $
is tight and indeed it is realized in the three-element Heyting algebra. Note that Theorem 4.5 gives rise to a substantially different proof of Theorem 2.2.
The formulae in one free variable which are not logically equivalent to those that occur in Proposition 2.1 and Theorem 2.2 do not have finite satisfiability gap. To show this (Lemma 2.10) we need to recall the definition of the Rieger–Nishimura lattice (Figure 1).
Definition 2.3. We define the sequences
$d_n$
and
$i_n$
of disjunctive and implicative Rieger–Nishimura formulae in the free variable p by mutual recursion as follows:
$$ \begin{align*} & d_0 = \bot, & \quad & i_0 = \bot, \\ & d_1 = p, & \quad & i_1 = \neg p, \\ & d_{n+1} = i_n \vee d_n, & \quad & i_{n+1} = i_n \rightarrow d_n. \end{align*} $$
The Rieger–Nishimura lattice consists of the formulae
$\top , d_n, i_n$
for all
$n \in \mathbb {N}$
, equipped with the ordering defined by
$a \leq _{RN} b$
precisely if
$a \rightarrow b$
holds in intuitionistic propositional logic.
Theorem 2.4 (Rieger [Reference Rieger15]).
As a Heyting algebra, the Rieger–Nishimura lattice is isomorphic to the free Heyting algebra on one generator.
Figure 1 (Left) Hasse diagram of the Rieger–Nishmiura lattice. (Right) Recursive definition of the terms of the Rieger–Nishmiura lattice. Theorem 2.11 states that the equations
$i_0 = \top $
,
$i_1 = \top $
,
$d_1 = \top $
,
$d_2 = \top $
, and
$i_\infty = \top $
(corresponding elements marked in bold) are the only ones with finite satisfiability gap.
It follows from Theorem 2.4 that every system of equations in one free variable p is logically equivalent to an equation of the form
$\varphi (p) = \top $
, where
$\varphi $
belongs to the Rieger–Nishmiura lattice. Notice that, in the notation of Definition 2.3, Proposition 2.1, and Theorem 2.2 show that the equations
$i_0 = \top $
,
$i_1 = \top $
,
$d_1 = \top $
, and
$d_2 = \top $
all have finite satisfiability gap.
Proposition 2.5. The equation
$\neg \neg p = \top $
has no finite satisfiability gap. Furthermore, we have
$\operatorname {\mathrm {\mathbf {ds}}}_{H \oplus _k \top }(\neg \neg p = \top ) < 1$
and
$\lim _{k \to \infty }\operatorname {\mathrm {\mathbf {ds}}}_{H \oplus _k \top }(\neg \neg p = \top ) = 1$
for any Heyting algebra H and
$k \in \mathbb {N}$
.
Proof If
$\neg \neg p = \top $
, then
$\bot = \neg p \wedge \neg \neg p = \neg p \wedge \top = \neg p$
. Since every element of the n-element chain, with the exception of
$\bot $
itself, negates to bottom (for any n), the sequence
$(C_n)_{n\in \mathbb {N}}$
of chains witnesses the fact that
$\neg \neg p = \top $
has no finite satisfiability gap. Furthermore, for any Heyting algebra H, every element of
$H \oplus _{k} \top \setminus H$
also negates to bottom (but
$\bot $
itself does not); thus the rest of the claim follows by the same argument as above.
Next consider
$i_3$
which is equivalent to
$\neg \neg p \to p$
and the equation
$i_3 = \top $
(i.e., the double-negation-elimination equation). Since both double-negation elimination and the law of excluded middle are classical principles, it is perhaps surprising to discover that, while
$p \vee \neg p = \top $
has a gap (Theorem 2.2), the equation
$\neg \neg p = p$
does not (Corollary 2.8).
Proposition 2.6. In every Heyting algebra H, the image of the negation map
$x \mapsto \neg x$
coincides with the set
$\operatorname {\mathrm {\mathbf {DN}}}_H$
.
Proof See, e.g., Theorem 1 of Chapter VIII in [Reference Balbes and Dwinger3].
Lemma 2.7. For any Heyting algebra H, let
$\iota : H \hookrightarrow H \oplus \top $
be the obvious lattice inclusion of H into
$H \oplus \top (i.e., such that (H \oplus \top ) \setminus \iota (H) = \{\top \})$
. Then, for any
$x \in H$
which is not
$\bot _H$
, we have
$\neg \iota ( x) = \iota ( \neg x)$
.
Proof If
$\neg \iota (x) = \max \left \{ {c \in H \oplus T}\:\middle \vert \:{\iota (x) \wedge c = \bot } \right \} = \top $
, then
$\iota (x) = \iota (x) \wedge \top = \bot $
and hence
$x = \bot _{H}$
since
$\iota $
is an injection. Thus, for any
$x \in H \setminus \{\bot \}$
, there is a
$y \in H \setminus \{\bot \}$
such that
$\neg \iota (x) = \iota (y)$
and so we must have
$y = \neg x$
, as desired.
Corollary 2.8. The formula
$\neg \neg x = x$
has no finite satisfiability gap.
Proof Consider the lattice inclusion
$\iota : B_n \hookrightarrow B_n \oplus \top $
as in Lemma 2.7 of a Boolean algebra
$B_n$
. It is enough to show that
$\iota (\top _{B_n})$
is the only element of
$B_n \oplus T$
for which double negation elimination does not hold since then one has that
$$\begin{align*}\lim_{n \to \infty}\bigl( \operatorname{\mathrm{\mathbf{ds}}}_{B_n \oplus \top}(\neg \neg x = x) \bigr)= \lim_{n \to \infty}\Bigl( \frac{\vert B_n \vert}{\vert B_n \oplus \top \vert} \Bigr) = 1.\end{align*}$$
To that end, using Lemma 2.7, we have that
$\neg \neg \iota (\top _{B_n}) = \neg \bot = \top \neq \iota (\top _{B_n})$
. Conversely
$\neg \neg \iota (\bot _{B_n}) = \neg \neg \bot = \bot = \iota (\bot _{B_n})$
and, for all
$b \in B_n \setminus \bot _{B_n}$
, we have
$\neg \neg \iota (b) = \iota (\neg \neg b) = \iota (b)$
by Lemma 2.7 and since
$B_n$
is Boolean.
Proposition 2.5 suggests that the sequence
$(H \oplus _k \top )_{k \in \mathbb {N}}$
is a good candidate for showing that the equations
$i_n = \top $
and
$d_m = \top $
for
$n \geq 4$
and
$m \geq 3$
have no gap, since the degree of satisfiability of both of these equations in
$H \oplus _{k} \top $
tends to
$1$
in as k tends to infinity (this follows by the ordering of the Rieger–Nishmiura lattice and from the fact that the degree of satisfiability of
$i_2=\top $
in
$H \oplus _k \top $
tends to
$1$
by the proof of Proposition 2.5). However, in itself this does not suffice to show that the equation
$\varphi = \top $
has no gap for all 
, since we have not yet ruled out the case that
$\operatorname {\mathrm {\mathbf {ds}}}_{H \oplus _{k} \top }(\varphi = \top ) = 1$
for all k. In Lemma 2.9 we show that, starting with some H such that
$\operatorname {\mathrm {\mathbf {ds}}}_{H}(\varphi = \top ) \neq 1$
, the elements of H which do not satisfy the equation
$\varphi = \top $
in H also do not satisfy it in
$H \oplus _{k} \top $
.
Lemma 2.9. Let
$\varphi $
be an element in the Rieger–Nishmiura lattice satisfying “
or 
”, H be a Heyting algebra and
$\iota : H \hookrightarrow H \oplus \top $
be the lattice-inclusion defined so that
$(H \oplus \top ) \setminus \iota (H) = \{\top \}$
. For any
$x \in H$
, if
$\varphi (x) \neq \top $
, then
$\varphi (\iota (x)) = \iota (\varphi (x))$
.
Proof We prove this by induction. For the base case, consider
$d_2$
and
$i_2$
. Notice that
$$\begin{align*}\iota(i_2(\bot)) = \iota(\neg \neg \bot) = \iota(\bot) = \bot_{H \oplus \top} = \neg \neg \bot_{H \oplus \top} = \neg \neg \iota(\bot) = i_2(\iota(\bot)).\end{align*}$$
Furthermore, for any
$x \neq \bot $
such that
$i_2(x) \neq \top $
(which implies that
$\neg \neg x \neq \top $
and hence
$\neg x \neq \bot $
) we have
$$ \begin{align*} \iota(i_2(x)) &= \iota( \neg \neg x)\\ &= \neg \iota( \neg x) &\text{(by Lemma~2.7 and since } \neg x \neq \bot\text{)} \\ &= \neg \neg \iota(x) &\text{(by Lemma~2.7 and since } x \neq \bot\text{)}\\ &= i_2(\iota(x)). \end{align*} $$
Furthermore, for all x such that
$d_2(x) = x \vee \neg x \neq \top $
(which implies
$x \not \in \{\bot , \top \}$
) we have that
$$ \begin{align*} \iota(d_2(x)) &= \iota(x \vee \neg x) \\& = \iota(x) \vee \iota(\neg x) &\text{(since } \iota \text{ is a lattice homomorphism)}\\&= \iota(x) \vee \neg \iota(x) &\text{(by Lemma~2.7 and since } x \neq \bot) \\ &= d_2(\iota(x)). \end{align*} $$
This concludes the proof of the base case.
Now suppose by way of induction that the claim holds if
$\varphi \in \{i_n, d_n\}$
and note throughout that if
$\psi \leq _{RN} \xi $
for two formulae
$\psi $
and
$\xi $
, then, for any x, if
$\xi (x) \neq \top $
then
$\psi (x) \neq \top $
.
If
$\varphi = d_{n+1}$
, then, for any x such that
$d_{n+1}(x) \neq \top $
we have
$d_n(x) \neq \top $
and
$i_n(x) \neq \top $
(since
$i_n \leq _{RN} d_{n+1}$
and
$d_n \leq _{RN} d_{n+1}$
); thus
$$ \begin{align*} \iota(\varphi(x)) &= \iota(d_{n+1}(x)) = \iota(i_n(x) \vee d_n(x)) &\text{(definition of } d_{n+1})\\ &= \iota(i_n(x)) \vee \iota(d_n(x)) &(\text{since } \iota \text{ is a lattice homomorphism)}\\ &= i_n(\iota(x)) \vee d_n(\iota(x)) &\text{(by induction and since } d_{n+1}(x) \neq \top)\\ &= d_{n+1}(\iota(x)) = \varphi(\iota(x)) &\text{(definition of } d_{n+1}). \end{align*} $$
If
$\varphi = i_{n+1}$
, then, for any x such that
$i_{n+1}(x) \neq \top $
, we have
$d_n(x) \neq \top $
(since
$d_n \leq _{RN} i_{n+1}$
) and also
$i_n(x) \neq \top $
(since otherwise
$$\begin{align*}i_{n+1}(x) = i_n(x) \to d_n(x) = \top \to d_n(x) = d_n(x),\end{align*}$$
which is a case we already considered). Thus we have
$$ \begin{align} i_{n+1}(\iota(x)) &= i_n(\iota(x)) \to d_n(\iota(x)) &\text{(definition of } i_{n+1}) \end{align} $$
$$ \begin{align} &= \iota(i_n(x)) \to \iota(d_n(x)) &\text{(induction \& since } i_{n+1}(x) \neq \top). \end{align} $$
By the definition of implication, we have that
$$ \begin{align*} \iota(i_n(x)) \to \iota(d_n(x)) &:= \max \left\{ {c \in H \oplus \top}\:\middle \vert \:{\iota(i_n(x)) \wedge c \leq \iota(d_n(x))} \right\}, \end{align*} $$
and c must either be an element of
$\iota (H)$
or
$c = \top $
. It cannot be that
$c =\top $
since then
$i_n(x) \leq _{H} d_n(x)$
which implies that
$ \varphi (x) = i_{n+1}(x) = i_n(x) \to d_n(x) = \top $
(which contradicts the assumption that
$\varphi (x) \neq _{H} \top $
). Thus c must be an element of
$\iota (H)$
. In this case we have (by the definition of
$i_{n+1}$
) that
$ \iota (i_n(x)) \to \iota (d_n(x)) = \iota (i_n(x) \to d_n(x)) = \iota (i_{n+1}(x)). $
Combining this with Equations (1) and (2) yields
$\varphi (\iota (x)) = i_{n+1}(\iota (x)) = \iota (i_{n+1}(x)) = \iota (\varphi (x))$
, as desired.
Lemma 2.10. Let
$n \geq 2$
and
$\varphi \in \{i_n, d_{n+1}\}$
. We can construct a finite Heyting algebra H such that
$\operatorname {\mathrm {\mathbf {ds}}}_{H \oplus _{k} \top }(\varphi = \top ) < 1$
for all
$k \in \mathbb {N}$
, but for which we have
$\lim _{k \rightarrow \infty } \operatorname {\mathrm {\mathbf {ds}}}_{H \oplus _{k} \top }(\varphi = \top ) = 1$
.
Proof Proposition 2.5 shows that
$i_2 = \top $
has no gap while Corollary 2.8 does the same for the equation
$i_3 = \top $
, so from here on we can assume that 
. Since propositional intuitionistic logic is complete with respect to finite Heyting algebras (Figure 2), and intuitionistic logic does not prove
$\varphi $
, we can find a finite Heyting algebra H for which
$\operatorname {\mathrm {\mathbf {ds}}}_{H}(\varphi = \top ) \neq 1$
. By Lemma 2.9 we know that
$\operatorname {\mathrm {\mathbf {ds}}}_{H \oplus _k \top }(\varphi = \top ) < 1$
for any
$k \in \mathbb {N}$
. But from Proposition 2.5 and the fact that 
we also know that
$\varphi (x) = \top $
is satisfied by at least k elements of
$H \oplus _k \top $
. Thus we have that
$$ \begin{align*} \operatorname{\mathrm{\mathbf{ds}}}_{H \oplus_k \top}(\varphi = \top) \geq \frac{k}{ \vert H \vert + k}\end{align*} $$
which tends to
$1$
since the right-hand side goes to
$1$
as
$k \to \infty $
.
Theorem 2.11. An equation
$\varphi (p)$
in one free variable has finite satisfiability gap precisely if it is equivalent to one of the following
$: p = \top $
,
$\neg p = \top $
or
$p \vee \neg p = \top $
.
Proof Follows immediately from Proposition 2.1, Theorem 2.2 and Lemma 2.10 by considering the Rieger–Nishmiura lattice (Theorem 2.4).
Figure 2 A sequence of Heyting algebras on which
$d_5 = \top $
has no finite gap. The sole element that fails to satisfy
$d_5 = \top $
is highlighted in white. Similar families can be constructed for all
$\varphi \geq _{\mathbf {RN}} i_2$
, while
$i_3$
requires a different technique.
3. Classical principles in two free variables
The structure of free Heyting algebras in more than one generator is poorly understood: in particular, the Rieger–Nishmiura theorem has no known analogue for such algebras. This prevents us from extending the methods of Section 2 towards a complete classification of two-variable equations with respect to satisfiability gap. However, a celebrated proof-theoretic result of Pitts (Theorem 3.3), combined with a result of Yankov (Theorem 3.4) allows us to determine the degrees of satisfiability of many classical principles. In particular, we obtain that none of the two-variable principles listed in Example 1.4 have finite gap.
Proposition 3.1. Take a theory T over a first-order language
$\mathcal {L}$
, and a formula
$\varphi (x_1,\dots ,x_n,y)$
in
$\mathcal {L}$
. If
$\varphi (x_1,\dots ,x_n,y)$
has finite satisfiability gap in T, then so does
$\forall y. \varphi (x_1,\dots ,x_n,y)$
.
Proof Assume that
$\varphi (x_1,\dots ,x_n,y)$
has satisfiability gap
$\varepsilon $
. Assume that
$\operatorname {\mathrm {\mathbf {ds}}}_H(\forall y. \varphi (x_1,\dots ,x_n,y))> 1 - \varepsilon $
in some finite model H of T. We lower bound the probability that elements
$w_1,\dots ,w_n$
and z chosen uniformly randomly from H satisfy
$\varphi (w_1,\dots ,w_n,z)$
. Choose
$w_1,\dots ,w_n$
and z uniformly randomly from H. With probability exceeding
$1 - \varepsilon $
, the chosen
$w_1,\dots ,w_n$
satisfy the formula
$\forall y. \varphi (w_1,\dots ,w_n,y)$
, and thus
$w_1,\dots ,w_n, z$
definitely satisfy
$\varphi (w_1,\dots ,w_n,z)$
. But this means that
$\operatorname {\mathrm {\mathbf {ds}}}_H(\varphi (x_1,\dots ,x_n,y))> 1 - \varepsilon $
, and hence
$\operatorname {\mathrm {\mathbf {ds}}}_H(\varphi (x_1,\dots ,x_n,y)) = 1$
.
Given an equation
$\varphi (x,y)$
in two free variables,
$\forall y. \varphi (x,y)$
has one free variable. One could hope to use the contrapositive of Proposition 3.1 to obtain non-existence of a finite satisfiability gap for a large class of equations in two variables, by reducing them to equations in one variable, which we have fully classified in Section 2. Unfortunately, as we see in Example 3.2, in the general case, the set defined by
$\forall y. \varphi (x,y)$
need not have an equational definition.
Example 3.2. The set defined by the formula
$\forall y. y \vee (y \rightarrow x) = \top $
need not coincide with any set defined by an equation in the language of Heyting algebras.
Proof Consider the 4-chain as a Heyting algebra. The set S defined by the formula
$\forall y. y \vee (y \rightarrow x) = \top $
has two elements, and does not contain
$\bot $
. Since the set defined by
$\neg \neg x = \top $
has 3 elements, and the set defined by
$\neg x = \top $
contains
$\bot $
, we have that S does not contain either of these sets. Using the Rieger–Nishmiura theorem, we get that S would have to coincide with the set defined by
$x = \top $
. But the latter has only one element.
In some cases, a celebrated result of A. M. Pitts allows us to work around the difficulty posed by Example 3.2, essentially by internalizing second-order propositional quantification in the intuitionistic propositional calculus.
Theorem 3.3 (Pitts [Reference Pitts14]).
Take a finite sequence of propositional variables
$\overline {x}$
, and a propositional variable y not contained in
$\overline {x}$
. Let
$\Phi (\overline {x}, y)$
denote a formula of intuitionistic propositional calculus containing only the variables in
$\overline {x}, y$
. Then we can find a propositional formula 
so that the following all hold
$:$
-
1. The formula
contains only the variables in
$\overline {x}$
. -
2. For any propositional formula
$\Psi (\overline {x})$
, intuitionistic logic proves the implication precisely if it proves
$\Psi (\overline {x}) \rightarrow \Phi (\overline {x}, y)$
. -
3. Given any propositional formula
$\Psi $
, intuitionistic logic proves all implications , where
$\Phi (\overline {x}, \Psi )$
denotes the formula obtained by substituting the formula
$\Psi $
for the propositional variable y everywhere in
$\Phi $
.
contains only the variables in 
precisely if it proves 
, where 
Keep in mind that the Pitts quantifier, 
, assigns formulae of intuitionistic logic to formulae of intuitionistic logic, not first-order formulae in the language of Heyting algebras to other such formulae. Before we use them, we require an alternative to Proposition 3.1 which allows us to replace the universally quantified first-order formula with a Pitts quantified equation. For classical principles, Proposition 3.5 constitutes one such result.
Theorem 3.4 (Yankov [Reference Yankov18]).
Take a classical principle
$f(x_1,\dots ,x_n) = \top $
in n free variables, and choose a variable symbol p distinct from each of the variables
$x_1,\dots ,x_n$
. We can find terms
$y_1, \dots , y_n \in \{ \top , p, \bot \}$
so that the universal closure of the inequality
$f(y_1,\dots ,y_n) \leq \neg \neg p \rightarrow p$
holds in every Heyting algebra.
Proposition 3.5. Take a classical principle
$f(x,y) = \top $
in the language of Heyting algebras. If
$f(x,y) = \top $
has finite satisfiability gap, then so does 
.
Proof Substituting 
for
$\Phi (\overline {x})$
in Theorem 3.3 yields that intuitionistic logic proves the implication 
. Passing through the Heyting semantics, we get that the universal closure of the inequality 
holds in every Heyting algebra.
Now assume that the equation
$f(x,y) = \top $
has finite satisfiability gap
$\varepsilon $
in the class of Heyting algebras. Moreover, assume that 
in some Heyting algebra H. Choose elements a and b uniformly randomly from H. With probability exceeding
$1 - \varepsilon $
, the chosen a satisfies 
, and thus, by the previously derived inequality, also satisfies
$f(a,b) = \top $
for all
$b \in H$
. But this means that
$\operatorname {\mathrm {\mathbf {ds}}}_H(f(x,y) = \top )> 1 - \varepsilon $
, and hence, by the finite satisfiability gap assumption,
$\operatorname {\mathrm {\mathbf {ds}}}_H(f(x,y) = \top ) = 1$
. We conclude that H is a Boolean algebra. We know from Theorem 3.4 that 
is equivalent to something in the downset of
$i_3$
, so it is either a classical principle (and thus its universal closure holds in H), or else equivalent to one of
$\{x = \top , \neg x = \top , \bot = \top \}$
, and by Proposition 2.1 holds with probability no larger than
$\frac {1}{2}$
in H.
Notice that while one could extend Proposition 3.5 to multiple variables, the assumption that
$f(x,y) = \top $
is a classical principle cannot be eliminated from the proof in any straightforward way. For example, one can find Heyting algebras where the equation
$x \vee (x \rightarrow y \vee \neg y) = \top $
holds universally, but 
does not.
Corollary 3.6. The following two-variable equations do not have finite satisfiability gap
$:$
-
•
$((x \rightarrow y) \rightarrow x) \rightarrow x = \top $
, -
•
$(\neg x \rightarrow \neg y) \rightarrow (y \rightarrow x) = \top $
, -
•
$(\neg x \rightarrow y) \rightarrow (x \rightarrow y) \rightarrow y = \top $
.
Corollary 3.6, along with Theorem 2.11, settle the finite gap question for most of the commonly considered classical principles enumerated in Example 1.4, with the sole exception of material implication,
$(x \rightarrow y) \rightarrow \neg x \vee y = \top $
. We shall prove that, although taking its universal closures or applying Pitts quantifiers always yields the equation
$x \vee \neg x = \top $
, the principle of material implication nevertheless does not have finite gap (Theorem 3.8). Consequently, the implications in Propositions 3.1 and 3.5 cannot be reversed, not even in the context of classical principles.
Definition 3.7. The materializer of an element x in a Heyting algebra H is the set
$M_H(x) = \left \{ {y \in H}\:\middle \vert \:{x \to y = \neg x \lor y} \right \}$
.
We remark that materializers display interesting algebraic structure which perhaps warrants further investigation in the future. Indeed, it can be shown that they contain
$\bot , \top $
, are closed under
$\wedge $
, and absorb all right implications. Moreover, whenever we have
$M_H(a) = M_H(b)$
, we also have
$(a \rightarrow b) \in \operatorname {\mathrm {\mathbf {EM}}}_H$
. Accordingly, in an algebra with trivial center, all materializers (apart from those of
$\bot , \top $
) are unique. While we found these properties useful in other developments, none of them play any direct role in what follows; thus, to avoid unnecessary tangents, we shall not include their proofs here.
Theorem 3.8. There exists a sequence
$(H_n)_{n \in \mathbb {N}}$
of Heyting algebras such that
$$ \begin{align*}1> \operatorname{\mathrm{\mathbf{ds}}}_{H_n}(a \to b=\neg a \lor b) \geq 1 - \frac{3^{n+1}}{(2^n + 1)^2}.\end{align*} $$
Proof Take the Boolean algebra
$B := (2^{[n]}, \cap , \cup , \to , \emptyset , [n])$
and let
$(H, \land , \lor , \Rightarrow , \emptyset , \top )$
denote the Heyting algebra formed by adjoining a new top element
$\top $
to B. Take any x and y in
$2^{[n]}$
and notice that, since
$x \leq y$
if and only if
$x \Rightarrow y = \top $
, then it must be that, if
$x \Rightarrow y \neq \top $
, then
$$\begin{align*}x \Rightarrow y = \bigvee \left\{ {r \in H}\:\middle \vert \:{x \land r \leq y} \right\} = \bigvee \left\{ {r \in B}\:\middle \vert \:{x \land r \leq y} \right\} = x \rightarrow y.\end{align*}$$
This implies that, for any
$x \in H$
, we can lower-bound the cardinality of the materializer
$M_H(x)$
of x as
$ \vert M_H(x) \vert \geq \vert H \vert - \vert \uparrow x \vert $
. Consequently we have
$$ \begin{align*} \sum_{x \in H} \vert M_H(x) \vert &\geq \vert H \vert ^2 - \sum_{x \in H} \vert \uparrow_H x \vert &\text{(since } \vert M_H(x) \vert \geq \vert H \vert - \vert \uparrow_H x \vert )\\ &= \vert H \vert ^2 - \Bigl (1 + \sum_{x \in B} \vert \uparrow_H x \vert \Bigr) &\text{(since } \vert \uparrow_H \top \vert = 1)\\ &= \vert H \vert ^2 - \Bigl (1 + \sum_{x \in B} (1 + \vert \uparrow_B x \vert ) \Bigr) &\text{(since } \forall x \in H, \{\top\} = \uparrow_H x \setminus \uparrow_B x)\\ &= \vert H \vert ^2 - \Bigl (1 + \vert B \vert + \sum_{i=0}^n \binom{n}{i}2^{n - i} \Bigr) &\text{(since } \uparrow_B x = \left\{ {s \subseteq [n]}\:\middle \vert \:{x \subseteq s} \right\})\\ &= \vert H \vert ^2 - (1 + 2^n + 3^n) &\text{(binomial formula)}\\ &\geq \vert H \vert ^2 - 3^{n+1}, \end{align*} $$
which then implies that
$\lim _{n \to \infty } \operatorname {\mathrm {\mathbf {ds}}}_{H}(a \to b=\neg a \lor b) = 1$
since
$$ \begin{align*} \operatorname{\mathrm{\mathbf{ds}}}_H(a \to b=\neg a \lor b) &= \frac{\sum_{x \in H} \vert M_H(x) \vert }{ \vert H \vert ^2} \geq \frac{\vert H \vert ^2 - 3^{n+1}}{\vert H \vert ^2} \geq 1 - \frac{3^{n+1}}{(2^n + 1)^2}. \end{align*} $$
Corollary 3.9. None of the equations in two variables given in Example 1.4 have a finite satisfiability gap.
4. The infinite case
In group theory, the notion of index provides an elegant way of measuring the “density” of subsets of infinite groups, and allows one to make sense of degree of satisfiability even in infinite groups. In fact, thanks to a relationship between virtual properties and positive degree of satisfiability [Reference Antolín, Martino and Ventura1], the concept manages to provide more information about the algebraic structure of groups in the infinite setting!
Since general Heyting algebras, unlike groups, do not come equipped with standard gadgets for measuring subset density quantitatively, we focus on finding purely qualitative analogues of the finite satisfiability gap results, in terms of set-theoretic cardinality instead of density. We extend the one-variable classification to infinite Heyting algebras by showing that if an equation
$\varphi (x)$
in one free variable has finite gap, then the set
$\left \{ {x \in H}\:\middle \vert \:{\neg \varphi (x)} \right \}$
cannot be non-empty and finite in an infinite Heyting algebra (Corollary 4.6), and has to be at least as large as
$\left \{ {x \in H}\:\middle \vert \:{ \varphi (x)} \right \}$
(Theorem 4.7).
Throughout this section let H denote an arbitrary (not necessarily finite) Heyting algebra, and let
$\mathbf {S} \subseteq H$
denote its set of non-central elements.
Lemma 4.1. Any maximal element
$s \in \mathbf {S}\ (i.e.,\ an\ element\ so\ that\ \textit{for}\ any s' \in \mathbf {S},\ \textit{if}\ s\ \leq s'\ then\ s = s')\ is\ dense\ in\ H\ (i.e.,\ \neg s = \bot )$
.
Proof Set
$\sigma = s \vee \neg s$
. Since s is a non-central element,
$\sigma \neq \top $
, so we have that
$$ \begin{align*}\sigma \vee \neg \sigma = (s \vee \neg s) \vee \neg (s \vee \neg s) = s \vee \neg s \vee \bot = s \vee \neg s \neq \top,\end{align*} $$
and hence
$\sigma \in \mathbf {S}$
too. But
$s \leq \sigma $
, so in fact
$s = \sigma $
. Hence,
$\neg s = \neg \sigma = \neg (s \vee \neg s) = \bot $
as claimed. (See also Figure 3 for a topological interpretation of this argument.)
Figure 3 A (not closed) open set s of a topological space V is either dense (
$\neg s = \bot $
), or the inclusion
$s \subseteq s \cup \mathrm {Int}(V \setminus s)$
is proper. In any case,
$\sigma = s \cup \mathrm {Int}(V \setminus s)$
itself is dense (its complement has empty interior;
$\neg \sigma = \bot $
). If s is a maximal non-closed open set, then
$s = \sigma $
.
Lemma 4.2. If
$a \vee b$
and
$a \wedge b$
both belong to
$\operatorname {\mathrm {\mathbf {EM}}}_H$
, then so do a and b.
Proof We prove that
$(a \vee b) \vee \neg (a \vee b), (a \wedge b) \vee \neg (a \wedge b) \vdash a \vee \neg a$
is a theorem of intuitionistic logic. By completeness it follows that if
$a \vee b$
and
$a \wedge b$
both belong to
$\operatorname {\mathrm {\mathbf {EM}}}_H$
, then so do a and b in any Heyting algebra H. The intuitionistic logic argument goes as follows. From
$(a \vee b) \vee \neg (a \vee b)$
, we have that one of a, b or
$\neg (a \vee b)$
holds. If it is a, then
$a \vee \neg a$
holds, so we’re done. If it is
$\neg (a \vee b)$
, then
$\neg a$
also holds, and so does
$a \vee \neg a$
, so we’re done again. So for the rest of the argument we can assume that b holds. There are two further possibilities: either
$a \wedge b$
holds, or
$\neg (a \wedge b)$
holds. In the former case, a and hence
$a \vee \neg a$
immediately follow. In the latter case, we have that b holds, so if a held,
$a \wedge b$
would follow, contradicting
$\neg (a \wedge b)$
. Thus, we get that
$\neg a$
, and consequently
$a \vee \neg a$
, must hold.
Lemma 4.3. For any
$x \in H$
and any maximal non-central element
$\sigma \in \mathbf {S}$
, either
$x \leq \sigma $
or
$x \lor \sigma = \top $
.
Proof Since
$\sigma $
is maximal non-central, then either
$x \vee \sigma = \sigma $
or else
$x \vee \sigma $
is central. In the first case
$x \leq \sigma $
as desired, and in the second case, we can calculate as follows:
$$ \begin{align*} \top &= (\sigma \lor x) \lor \neg (\sigma \lor x) \\ &= (\sigma \lor x) \lor (\neg \sigma \land \neg x) \\ &= (\sigma \lor x) \lor (\bot \land \neg x) & \text{(by Lemma~4.1)} \\ &= \sigma \lor x.\\[-35pt] \end{align*} $$
Corollary 4.4. For any
$x \in \operatorname {\mathrm {\mathbf {EM}}}_H$
and any maximal non-central element
$\sigma \in \mathbf {S}$
, we have precisely one of
$x \vee \sigma = \top $
or
$\neg x \vee \sigma = \top $
.
Proof It’s clear that both equalities cannot hold. By Lemma 4.3, either
$x \vee \sigma = \top $
or
$x \leq \sigma $
. In the former case we have our claim. In the latter case, since
$\neg x \vee x = \top $
and
$x \leq \sigma $
, we get that
$\neg x \vee \sigma = \top $
as desired.
Theorem 4.5. Take any maximal non-central element
$\sigma \in \mathbf {S}$
. The function
$f: \operatorname {\mathrm {\mathbf {EM}}}_H \rightarrow \mathbf {S}$
given by the equation
$$ \begin{align*}f(x) = \begin{cases} \sigma \wedge x, & \text{if}\ \sigma \vee x = \top, \\ \sigma \wedge \neg x, & \text{otherwise,} \end{cases} \end{align*} $$
is well-defined and two-to-one.
Proof For well-definedness, apply Lemma 4.2 and Corollary 4.4. Now take two central elements
$c,d$
such that
$\sigma \vee c = \top $
and
$\sigma \vee d = \top $
. Assume that
$f(c) = \sigma \wedge c = \sigma \wedge d = f(d)$
. Then we have that
$$\begin{align*}c = c \vee (\sigma \wedge c) = c \vee (\sigma \wedge d) = (c \vee \sigma) \wedge (c \vee d) = \top \wedge (c \vee d) = c \vee d.\end{align*}$$
By a similar argument, we have
$d = c \vee d$
. Thus
$c = c \vee d = d$
and hence (applying Corollary 4.4 once more) the function f is two-to-one as claimed.
Corollary 4.6. Every non-Boolean Heyting algebra that has only finitely many non-central elements is finite.
Proof A non-Boolean Heyting algebra that has finitely many non-central elements always has a maximal non-central element. The result follows immediately from Theorem 4.5.
Notice that Theorem 4.5 immediately yields an alternative proof of Theorem 2.2 (since the map f in Theorem 4.5 is two-to-one). Corollary 4.6 is an infinitary analogue of the latter. We obtain an even stronger infinitary result in Theorem 4.7.
Theorem 4.7. Consider an infinite Heyting algebra H, and define the following subsets
$:$
$$ \begin{align*} C = \left\{ {x \in H}\:\middle \vert \:{x \vee \neg x = \top} \right\}, \\ D = \left\{ {x \in H}\:\middle \vert \:{x \vee \neg x \neq \top} \right\}. \end{align*} $$
We always have either
$ \vert D \vert = 0$
or
$ \vert C \vert \leq \vert D \vert $
.
Proof If
$ \vert C \vert <\infty $
or
$ \vert D \vert <\infty $
, then the result follows from Corollary 4.6. For the rest of the proof, we assume that the sets C and D are both infinite. Choose an element
$x \in D$
and set
$s = x \vee \neg x$
. Then we have
$\neg s = \neg (x \vee \neg x) = \bot $
, so
$s \vee \neg s = s \vee \bot = s \neq \top $
, and therefore
$s \in D$
. Define the sets
$$ \begin{align*} C_s = \left\{ {x \in C}\:\middle \vert \:{x \leq s} \right\}, \\ C^s = \left\{ {x \in C}\:\middle \vert \:{x \not\leq s} \right\}, \end{align*} $$
and notice that
$ \vert C_s \vert \leq \vert C^s \vert $
since
$x \mapsto \neg x$
gives an injective function from
$C_s$
to
$C^s$
. Since
$C_s \cup C^s = C$
it follows by cardinal arithmetic that
$ \vert C^s \vert = \vert C \vert $
. We now construct an injective map from
$C^s$
to D, thus showing that
$ \vert C \vert = \vert C^s \vert \leq \vert D \vert $
. Consider the function
$$ \begin{align*} f: C^s \rightarrow D,~ ~ ~ ~\\ f(x) = s \wedge x\text{.} \end{align*} $$
First we show that f is well-defined. Take an arbitrary
$x\in C^s$
and assume for a contradiction that
$f(x) \not \in D$
. Then
$f(x) \in C$
, so that
$(s \wedge x) \vee \neg (s \wedge x) = \top $
. Noticing that
$\neg (s \wedge x) = \neg (x \wedge s) = x \rightarrow \neg s = x \rightarrow \bot = \neg x$
, we calculate as follows:
$$ \begin{align*} s \vee \neg x &= s \vee \neg (s \wedge x) \\ &= s \vee (s \wedge x) \vee \neg (s \wedge x) &\text{(absorption)} \\ &= s \vee \top &\text{(by}\ s \wedge x \in C) \\ &= \top. \end{align*} $$
But then
$x \wedge s = (x \wedge s) \vee (x \wedge \neg x) = x \wedge (s \vee \neg x) = x$
, so
$x \leq s$
, contradicting
$x \in C^s$
. This shows the well-definedness of the function
$f: C^s \rightarrow D$
. Now we need to show that f is injective. So assume that
$s \wedge x = s \wedge y$
for some
$x,y \in C^s$
. Then we have
$\neg x = \neg (s \wedge x) = \neg (s \wedge y) = \neg y$
by repeating an argument above, and since
$x, y \in C$
we can negate both sides to get
$x = y$
.
Corollary 4.8. An infinite
$T_0$
topological space is either discrete or has more non-closed open sets than clopen sets.
Proof The lattice of open sets of a topological space forms a (complete) Heyting algebra if we define
$x \rightarrow y$
as the interior of
$\overline {x} \cup y$
, so Theorem 4.7 applies.
We remark that for each equation
$\varphi (x)$
in one free variable which does not have a finite satisfiability gap, one can use standard model-theoretic techniques to construct an infinite Heyting algebra
$H_\varphi $
such that
$H_\varphi \not \models \varphi $
, but where only finitely many elements of H fail to satisfy
$\varphi $
. Whether this is a coincidence, or a deep feature of degree of satisfiability in Heyting algebras, remains to be seen.
5. Towards black-box lattice theory
Babai and Szemerédi introduced black-box groups in their seminal 1984 article [Reference Babai and Szemeredi2], as a uniform idealized setting for the study of randomized algorithm complexity on permutation and matrix groups. Since then, the field of black-box algebra has found applications in cryptography, and has so far come to encompass the study of black-box groups and fields, and to some extent rings and even black-box projective planes [Reference Borovik and Yalçinkaya4].
Borovik and Yalçınkaya pioneered a successful integrated approach [Reference Borovik, Yalçinkaya, Bigatti, Carette, Davenport, Joswig and de Wolff5] to black-box algebra, characterized by the application of black-box constructions associating higher structures to black-box algebraic structures (e.g., studying a black-box ring R by constructing black-box R-modules, or black-box fields F by constructing projective planes with underlying field F [Reference Borovik and Yalçinkaya4]). Many algebraic (not to mention universal algebraic) constructions associate lattices to group-like and ring-like structures: e.g., Coquand [Reference Coquand6] suggests that ring spectra are best treated in terms of distributive lattices in settings where obtaining prime ideals is computationally difficultFootnote 1 . Such constructions serve to motivate the black-box algebraic investigation of lattice-like structures.
In this section we make the basic observation that finite satisfiability gap results yield efficient one-sided Monte Carlo algorithms for black-box structures. In particular, due to Theorem 2.2, there is an efficient such algorithm for testing whether a black-box Heyting algebra is Boolean. Our Definition 5.1 coincides with the generic axiomatic description of black-box algebraic structures given by Borovik and Yalçınkaya [Reference Borovik, Yalçinkaya, Bigatti, Carette, Davenport, Joswig and de Wolff5], specialized to the case of Heyting algebras.
Definition 5.1. A black-box Heyting algebra consists of the following data:
-
• a finite underlying Heyting algebra
$\langle H, \wedge , \vee , \rightarrow , \bot , \top \rangle $
, -
• a set of cryptoelements X, bitstrings of a fixed finite length
$\ell (X)$
, -
• a decryption function
$\pi : X \rightarrow H$
,
along with the following fixed algorithms operating on bitstrings:
-
• BB1: a randomized algorithm that takes no inputs and produces a random cryptoelement as output, in such a way that repeatedly applying the decryption function
$\pi $
to the output of the algorithm produces uniformly distributed elements over H (but not necessarily over X!); -
• BB2: algorithms
$\hat {\vee }$
(
$\hat {\rightarrow }$
, etc.) that take as input two cryptoelements
$x, y \in X$
, and produce as output a cryptoelement
$x \hat {\vee } y$
(
$x \hat {\rightarrow } y$
etc.) such that
$\pi (x \hat {\vee } y) = \pi (x) \vee \pi (y)$
(etc.); -
• BB2’: an algorithm that produces a cryptoelement
$\hat {\bot } \in X$
such that
$\pi (\hat {\bot }) = \bot $
(the similar algorithm for
$\top $
could be given but is redundant); -
• BB3: an algorithm that takes as input two cryptoelements
$x, y$
, and produces the output bitstring
$1$
only if
$\pi (x) = \pi (y)$
, and outputs
$0$
otherwise.
When considering uniformly given families of black-box structures, the additional assumption is made that these algorithms operate in time polynomial in the size of
$\ell (X)$
.
Definition 5.2. Consider a first-order sentence
$\varphi $
in the language of Heyting algebras. A one-sided black-box Monte Carlo algorithm for testing property
$\varphi $
is a randomized algorithm A that takes as input
$\langle X, \hat {\vee }, \dots \rangle $
for a black-box Heyting algebra
$\langle H, X, \pi , \hat {\vee }, \dots \rangle $
, such that:
-
• if
$H \models \varphi $
then A returns the bitstring
$1$
; -
• if
$H \not \models \varphi $
then with probability larger than
$\frac {1}{2} A$
returns the bitstring
$0$
, and the bitstring
$1$
otherwise;
all in time polynomial in
$\ell (X)$
.
Theorem 5.3. There is a one-sided black-box Monte Carlo algorithm for testing whether a black-box Heyting algebra is a Boolean algebra.
Proof Use BB1 to pick a random element
$x \in X$
, then BB2’ to obtain
$\hat {\bot }, \hat {\top }$
and BB2 to compute
$x \hat {\vee } (x \hat {\rightarrow } \hat {\bot })$
. Using BB3, decide if
$$ \begin{align*}\pi( x \hat{\vee} (x \hat{\rightarrow} \hat{\bot}) ) = \pi(x) \vee \neg \pi(x) = \pi(\hat{\top}) = \top.\end{align*} $$
Repeat the same process with another random element
$y \in X$
. If both
$\pi (x) \vee \neg \pi (x) = \top $
and
$\pi (y) \vee \neg \pi (y) = \top $
hold, output the bitstring
$1$
. Otherwise, output the bitstring
$0$
.
If H is Boolean, then of course
$\pi (x) \vee \neg \pi (x) = \pi (y) \vee \neg \pi (y) = \top $
always holds, so the algorithm outputs
$1$
as desired. Otherwise, by Theorem 2.2, the probability that both
$\pi (x)$
and
$\pi (y)$
belong to the center of H is no more than
$\frac {4}{9}$
, so with probability larger than
$\frac {1}{2}$
the algorithm returns the bitstring
$0$
.
The idea behind Theorem 5.3 clearly generalizes to any first-order property of structures that is definable by an equation with finite satisfiability gap, establishing a fruitful application of degree of satisfiability to black-box algebra.
Problem 5.4. Is there a one-sided black-box Monte Carlo algorithm that tests whether a black-box Heyting algebra is a Boolean algebra in time polynomial in
$\ell (X)$
, but does not invoke the oracle
$\hat {\vee }$
? What about an algorithm that does not use
$\hat {\bot }$
? Relatedly, can we find an equation
$\varphi $
in the language
$\langle \wedge , \rightarrow , \bot , \top \rangle $
(resp. the language
$\langle \wedge , \vee , \rightarrow , \top \rangle $
) so that
$\varphi $
is a classical principle with finite satisfiability gap?
6. Discussion
6.1. Anti-exceptionalism
Anti-exceptionalism—the belief that logic should be accepted, rejected, and revised according to the same standards as other (e.g., scientific) theories—plays a distinguished role in the leading contemporary realist metaphysical accounts of reasoning (see, e.g., Part 3 of G. Russell’s Justification [Reference Russell16]). In his methodological treatise, T. Williamson [Reference Williamson17] asserts that purported logical laws should be judged, at least in part, based on “the fit between their consequences and what is independently known”. As such, in Williamson’s account, it is possible to have disconfirming physical evidence against purported logical laws. Namely, if a well-confirmed theory yields disconfirmed consequences according to the consequence relation of a logic, that counts as evidence against the logic. For the reader interested in anti-exceptionalism, we recommend O. T. Hjortland’s summary [Reference Hjortland10] of Williamson’s account, which gives several worked-out examples.
Although Williamson argued that his variant of anti-exceptionalism provides evidential criteria that favors classical logic over other, competing logical theories in realist metaphysical accounts of reasoning, there are several objections to this view. Beyond the ones summarized by Hjortland [Reference Hjortland10], we further point out the non-existence of a neutral interpretation relating the structure of logical formulae to “disconfirming physical evidence”: what one counts as disconfirming physical evidence for a compound sentence (think, e.g.,
$((P \rightarrow Q) \rightarrow P) \rightarrow P$
) may depend on the flavor of logic one chooses to use.
Even if the objections discussed above were resolved, it is still questionable whether there could be any physical situation that would allow one to distinguish between classical and intuitionistic logic using Williamson’s methodology. While investigating the full implications of our technical results to Williamson’s anti-exceptionalist argument will require a longer philosophical treatise, we note that, were one able to devise a large number of such situations, one could apply Heyting algebras as a semantic model, and use our results (in particular, Theorem 2.2 and its black-box formulation, Theorem 5.3) to argue that whenever the classical laws of propositional logic fail in a given setting, the evidence disconfirming them is abundant. Conversely, Theorem 6.1 shows that in all contexts where the law of excluded middle holds to any appreciable degree, some non-tautologies of intuitionistic logic hold universally.
Theorem 6.1. For any natural
$n \geq 2$
, let
$f_n$
be one of the formulae
$\{i_{n+1}, d_n\}$
in the Rieger–Nishmiura lattice. There is a strictly monotone function g such that, given any finite Heyting algebra H, if
$\operatorname {\mathrm {\mathbf {ds}}}_H(d_2)> \frac {2}{g(n)}$
, then
$\operatorname {\mathrm {\mathbf {ds}}}_H(f_n) = 1$
.
Proof Let
$g(n)$
denote the smallest integer m such that some Heyting algebra M with
$ \vert M \vert = m$
fails to satisfy
$f_n$
. Assume that
$\operatorname {\mathrm {\mathbf {ds}}}_H(d_2)> \frac {2}{g(n)}$
. Using the inductive argument in the proof of Theorem 2.2, we can write H as the product
$H \cong H_1 \times H_2 \times \cdots \times H_k$
where all the factors
$H_i$
have trivial center, and by Proposition 1.9,
$\operatorname {\mathrm {\mathbf {ds}}}_{H_i}(d_2)> \frac {2}{g(n)}$
holds for each factor
$H_i$
. This means that
$ \vert H_i \vert < g(n)$
, so
$\operatorname {\mathrm {\mathbf {ds}}}_{H_i}(f_n) = 1$
holds for each i by the definition of
$g(n)$
. It follows that
$\operatorname {\mathrm {\mathbf {ds}}}_{H}(f_n) = 1$
.
6.2. Open problems
On one hand, the classification of Theorem 2.11 raises many follow-up questions about the case of multiple variables. For example, are there infinitely many different equations in
$n \geq 2$
free variables with finite satisfiability gap? Similarly, can the classification be extended from equations to equations in two variables where one of the variables is universally quantified? In group theory, such formulae frequently have well-behaved gaps as a consequence of Lagrange’s theorem. That said, we expect that the complicated structure of the free Heyting algebras on multiple generators to make all investigation in this vein quite difficult in the Heyting algebra setting.
On the other hand, while Theorem 2.11 provides a complete classification, it does not say anything about relative degrees of satisfiability: for example, it could be useful to classify the pairs of one-variable equations,
$(\varphi , \psi )$
which cannot both hold with arbitrarily high (but
$\neq 1$
) probability in the same algebra. For example, the equations
$\neg x \vee \neg \neg x = \top $
and
$\neg \neg x = x$
constitute one such pair. We expect that a thorough understanding of all such pairs would lead to much more elegant proofs of Theorem 2.11. Similarly, one could attempt classification in more restricted (say Gödel algebras) and less restricted (modular lattices) settings: the former would have applications in intermediate logics, while the latter would be useful for the development of black box lattice theory discussed in Section 5.
As a long-term goal, one would wish to see a classification of those intermediate logics which can be defined by an equation with finite satisfiability gap. As a stepping stone, one would want to obtain well-behaved families of formulae with finite gap: note that, e.g., the Yankov formulae do not constitute such a family.
Acknowledgements
We are grateful to the anonymous referees for their thorough review and valuable suggestions, including an idea that streamlined the proof of Theorem 2.2. Z. A. Kocsis acknowledges the use of CSIRO’s national facilities in undertaking this research. Both authors contributed equally to this work.
Funding
B. M. Bumpus was supported both by an EPSRC studentship, and by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant Agreement No. 803421, ReduceSearch).
