My good friend Zoltan Kocsis and I finally got our paper “Degree of Satisfiability in Heyting Algebras” published in the Journal of Symbolic Logic. Yay! Since Zoltan is half-way across the world, we can’t grab a beer together and celebrate, so instead here’s a celebratory blog post (you can find the ArXiv version of our paper here).

Let’s start with a fun question about groups:

Let \(G\) be a finite group, for uniformly and independently chosen elements \(x\) and \(y\) in \(G\), what the the probability that \(x\) and \(y\) commute?

In other words we ask: what is the value of $$\mathsf{ds}_G(xy= yx) := \frac{|\{(x,y) \mid x, y \in G \text{ and } xy = yx\}|}{|G|^2}?$$

The answer is well-known: either \(G\) is Abelian, in which case \(\mathsf{ds}_G(xy= yx) = 1\), or \(G\) is not Abelian and one has \(\mathsf{ds}_G(xy= yx) \leq 5/8\).

This was first shown by Erdős and Turán and and later generalized by Gustafson. The result for finite groups is not hard and I recommend John Baez’s wonderful blog post about this, if you want to learn the proof.

Framing this result a bit more conceptually, it is asking: how close can a group be to being Abelian without actually being Abelian? Clearly one can ask this kind of question about any mathematical structure and indeed this falls into the more general setting of determining the degree of satisfiability of some property \(p\) in some finite structure \(M\); in other words one asks: “what is the probability that uniformly chosen elements of \(M\) satisfy \(p\)?” Formally it is defined as follows.

Def: 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
$$ \frac{ | \{ (a_1, \dots, a_n) \in M^n \mid \varphi(a_1, \dots, a_n) \} | }{ | M | ^n }$$
the degree of satisfiability of the formula \(\varphi\) in the structure \(M\), and denote it \(\mathsf{ds}_M(\varphi)\). One says that a formula \(\varphi\) has finite satisfiability gap \(\varepsilon\) for \(0 < \varepsilon < 1\) if for all \(M\) either \(\mathsf{ds}_M(\varphi\) = 1\) or \(\mathsf{ds}_M(\varphi) \leq 1 – \varepsilon\).

For groups there are many results establishing such finite satisfiability gaps. Some of these were developed by my friend Zoltan in his paper “Degree of Satisfiability of Some Special Equations” which is also where the terminology “degree of satisfiability” comes from. But what’s particularly interesting is the sheer quantity of known gap results (see our paper for pointers for further reading); indeed, as of now, the existence of an equation in the language of group theory that does not have finite satisfiability gap remains open. This is even in the case of equations in only one free variable; for example only partial results about finite satisfiability gaps are known for the equation \(x^p = 1\) for any \(p\) at least five.

Why Heyting Algebras?

Having said all this, it looks like the story for groups gets quite hard rather fast, so what about other structures? This is exactly what Zoltan asked me when he approached me about working on this topic. We studied Heyting Algebras and hopefully you’re now asking yourself: “why Heyting algebras?”. The answer is that the choice was motivated by both practical concerns and philosophical ones. On the practical side, Zoltan suspected that interaction of algebraic and order-theoretic structure would be helpful for our purposes; this was overwhelmingly true. On the philosophical side, studying degree of satisfiability in Heyting algebras lets us shed light on anti-exceptionalism: this is the contention that logic itself should be accepted, rejected and revised
according to the same standards as other theories in science. In other words one should attempt to disprove the validity of a given logical system by searching for empirical evidence that falsifies a true statement in that logic.

Now the question is: suppose you wanted to test whether we should reason about the universe using classical or intuitionistic logic, what would do? Even if you only find evidence for classical logic (i.e. you find that all of your experiments so far agree with with what one would expect in classical logic), that doesn’t equip you with any sense of how likely it is for you to never encounter a situation in which one must think intuitionistically, but not classically. But this is where degree of satisfiability can be useful. Suppose you knew that there is an equation \(\varphi = \top\) which is tautological in classical logic, but not intuitionistically. If we know that \(\varphi = \top\) has finite satisfiability gap \(\varepsilon\), then, as we examine the universe, collecting data about the validity of the equation \(\varphi = \top\) as we go, and, because this equation has finite satisfiability gap, we can quantify how likely it is that the following two assertions hold simultaneously: (1) so far, all of our data points satisfy \(\varphi = \top\) (which, recall, is a classical principle) while (2) the universe we inhabit exhibits evidence against classical logic (i.e. there exist data points which do not satisfy \(\varphi = \top\)).

Some examples of classical principles (i.e. formulae that are tautological if and only if the logical system we inhabit is the classical one) include:

• \(x \lor \neg x = \top\) (i.e. the law of excluded middle)
• \(\neg \neg x = x\) (i.e. double negation elimination) and
• \( x \to y = \neg x \lor y\) (i.e. material implication).

So do there exist classical principles which have finite satisfiability gap? And what does this have to do with Heyting Algebras?

Surprisingly the short answer is yes! This is part of what we show in our paper. But, before I spoil the fun, let’s answer the second question: we care about Heyting algebras because they are to intuitionistic logic what Boolean algebras are to classical logic. Formally this is what I mean:

(1) a propositional formula \(\varphi\) is provable in classical logic precisely if, for every Boolean algebra \(B\), one has that \(B \models (\varphi = \top)\) and

(2) a propositional formula \(\varphi\) is provable in intuitionistic logic precisely if, for every Heyting algebra \(H\), one has that \(H \models (\varphi = \top)\).

These two two statements mean that we can think about all of this wonderful business of anti-exceptionalism in very mathematically concrete terms; we ask: are there any classical principles (such as the ones I listed above) which have finite satisfiability gap in Heyting algebras?

To understand what this means, note that, if the answer were no, then this would mean that it’s essentially hopeless to try to empirically assert the validity of classical logic over intuitionistic logic. This is because, for any classical principle \(\varphi\) , there would be Heyting algebras \(H\) (plausible models of the logical structure of the universe we inhabit) in which the classical principle does not hold (i.e. \(H\) is not Boolean), but where the probability of satisfying the equation \(\varphi = \top\) is arbitrarily high when one samples points from \(H\) independently at random.

Fascinatingly, it turns out that this is not the case! Indeed we showed that the law of excluded middle does have finite satisfiability gap (this is the theorem below) and moreover, with much more effort, one can suitably extend this result to infinite Heyting algebras.

Theorem [B. , Kocsis]: for any heyting algebra \(H\), either \(H\) is Boolean (in which case \(\mathsf{ds}_H(x \lor \neg x = \top) = 1\)) or one has that \(\mathsf{ds}_H(x \lor \neg x = \top) \leq 2/3\).

We prove many more results, for instance we show that, although double negation elimination also is a classical principle, it does not have finite satisfiability gap. In other words, there are Heyting algebras which are not Boolean, but in which double negation elimination holds with arbitrarily high probability!

This is the starting point for another one of our results which yields a complete classification of all the one-variable equations of Heyting algebras in terms of their degree of satisfiability.

Theorem [B., Kocsis]: 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 \lor \neg p = \top\).

Where to next?

This project was incredibly fun particularly because it involved a blend of combinatorics (e.g. to prove that material implication has no gap), lattice theory and logic. Furthermore, the results are very encouraging compared to the case of finite groups, so perhaps there is a big untold story lurking here in the realms of lattice theory. I wonder what we might uncover next…

Until next time,

Ben