You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
John Baez (Feb 28 2024 at 01:48):The Law of Excluded Middle says that for any statement P, "P or not P" is true.
๐๐ ๐๐ต๐ถ๐ ๐น๐ฎ๐ ๐๐ฟ๐๐ฒ? In classical logic it is. But in intuitionistic logic it's not.
So, in intuitionistic logic we can ask what's the ๐ฅ๐ง๐ค๐๐๐๐๐ก๐๐ฉ๐ฎ that a randomly chosen statement obeys the Law of Excluded Middle. And the answer is "at most 2/3 - or else your logic is classical".
This is a very nice new result by @Benjamin Merlin Bumpus (he/him) and @Zoltan A. Kocsis:
https://bmbumpus.com/2024/02/27/degree-of-classicality/
Of course they had to make this more precise before proving it. Just as classical logic is described by Boolean algebras, intuitionistic logic is described by Heyting algebras. They proved that in a finite Heyting algebra, if more than 2/3 of the statements obey the Law of Excluded Middle, then it must be a Boolean algebra!
Ralph Sarkis (Feb 28 2024 at 07:21):Can this also be seen as a theoretical confirmation of the paradox of Zaionc (I learned it from here) saying that "asymptotically almost all classical theorems are intuitionistic" ?
Ryan Wisnesky (Feb 28 2024 at 08:07):there's a caveat: free heyting algebras with more than one generator are infinite, so I'd argue intuitionistic logic isn't captured by finite heyting algebras the way classical logic is with finite boolean algebras.
John Baez (Feb 28 2024 at 08:08):True, but they have lots of finite quotients.
Mike Shulman (Feb 28 2024 at 08:09):The blog post claims that "with much more effort, one can suitably extend this result to infinite Heyting algebras."
John Baez (Feb 28 2024 at 08:09):Ralph Sarkis said:
Can this also be seen as a theoretical confirmation of the paradox of Zaionc (I learned it from here) saying that "asymptotically almost all classical theorems are intuitionistic" ?
That sounds like an almost opposite claim. I also wonder what it really means. In the free Heyting algebra on one generator, I think all but finitely many elements are "classically true" (they map to in the free boolean algebra on one generator) but not true.
Mike Shulman (Feb 28 2024 at 08:13):It looks like what they actually prove in the infinite case is that if an infinite Heyting algebra is not Boolean, then the cardinality of the subset of elements not satisfying LEM must be at least as large as the cardinality of the subset of elements satisfying LEM. So in some sense there must be "at least as many counterexamples to LEM as there are examples" if LEM doesn't hold globally.
Mike Shulman (Feb 28 2024 at 08:15):That's certainly something, but it doesn't seem like quite the same result. In particular, it leaves open the possibility that the Heyting algebra comes with a measure in which the set of elements not satisfying LEM is arbitrarily small or even zero, which seems more relevant to questions of "probability".
Morgan Rogers (he/him) (Feb 28 2024 at 08:41):The blog post makes the comparison to results from group theory, but for a large class of groups one has a canonical "Haar measure" to compare subsets. I too wonder if there is a sufficiently canonical measure on Heyting algebras to compare subsets in this way. After all, the cardinality argument doesn't hold much water when I can divide a countably infinite set into arbitrarily many disjoint subsets of the same cardinality...
John Baez (Feb 28 2024 at 08:47):I wonder if the theory of Fraรฏssรฉ limits applies to Heyting algebras as it does to graphs.
James Deikun (Feb 28 2024 at 10:24):Mike Shulman said:
That's certainly something, but it doesn't seem like quite the same result. In particular, it leaves open the possibility that the Heyting algebra comes with a measure in which the set of elements not satisfying LEM is arbitrarily small or even zero, which seems more relevant to questions of "probability".
I thought at first that the topos of sheaves on the real interval in fact comes with such a measure, but the measure I was thinking of wasn't a measure on truth values.
James Deikun (Feb 28 2024 at 10:31):Then again, for this result to hold measure-theoretically you need some kind of uniformity condition on the measure or it won't hold in even the finite case.
David Michael Roberts (Feb 28 2024 at 10:35):For compact topological groups, normalised to have volume 1 say, the result about proportion of commuting elements in a finite group extends to the measure of commuting elements.
David Michael Roberts (Feb 28 2024 at 10:41):So considering a Heyting algebra as a semiring with extra structure, then one could think about how to extend the group result to semigroups
David Michael Roberts (Feb 28 2024 at 10:47):However, see https://mathoverflow.net/a/180020/4177 where not even finite semigroups are guaranteed to admit an invariant measure
Zoltan A. Kocsis (Feb 28 2024 at 12:24):Morgan Rogers (he/him) said:
The blog post makes the comparison to results from group theory, but for a large class of groups one has a canonical "Haar measure" to compare subsets. I too wonder if there is a sufficiently canonical measure on Heyting algebras to compare subsets in this way. After all, the cardinality argument doesn't hold much water when I can divide a countably infinite set into arbitrarily many disjoint subsets of the same cardinality...
The classical group-theoretic results (such as Gustafson's 5/8) indeed hold for the Haar measure on a locally compact group. I don't know whether one could have a canonical measure on a locally compact Heyting algebra in any analogous sense.
However, the interesting cases of density on a Heyting algebra won't arise from an analogous measure: in most cases outside of topos theory (and in many cases inside), one will want to consider some countable Heyting algebra, such as a free HA on some generators, or one of its quotients. The analogous objects (e.g. free groups) don't admit invariant measures even in group theory, since a countable, locally compact group always carries the discrete topology.
This doesn't stop group theorists from studying the density of nice subsets of groups, though! Even when you don't have a Haar measure, the group structure gives you a convenient gadget to measure density: the index (number of translates of a set required to cover the group). This gives you certain favored ways to enumerate elements (the ways that _measure index uniformly_), which is a major plot point in the group-theoretic works of Antolin, Martino, Ventura, Tointon that inspired our results.
Fortunately, you can obtain similar density-measuring gadgets on Heyting algebras. For example, on finitely presented Heyting algebras, you can use the fact that all such algebras embed into products of finite Heyting algebras in nice, reasonably canonical ways. You can in a sense regard the degrees of satisfiability in these finite factors as providing bounds on the density of solutions in your algebra of interest, using the fact that "ds(phi) in H1xH2" always coincides with "ds(phi) in H1" times "ds(phi) in H2".
If you want to study the non-finitely-presented (but still countable) case, you can fix certain natural ways of expanding a finite subset of the HA by applying the Heyting algebra operations, and characterize what happens to the density of solutions to an equation of interest when you expand a finite subset for a long time.
I've started working on both of these approaches after the current article was sent off, and I have some partial results in both cases: e.g. one can show that, under these natural ways of measuring density, the density of LEM is zero in a free HA on a finite set of generators. But the rest is is all very much work-in-progress for now.
Zoltan A. Kocsis (Feb 28 2024 at 12:36):Mike Shulman said:
That's certainly something, but it doesn't seem like quite the same result. In particular, it leaves open the possibility that the Heyting algebra comes with a measure in which the set of elements not satisfying LEM is arbitrarily small or even zero, which seems more relevant to questions of "probability".
Indeed, and see my comments below on the appropriate notions of density one would use instead of measure, given that on the syntactic side, the most exciting infinite HAs are countable, and lack anything like a uniform measure.
If you do wish to think about probability measures, though, I think our infinite results are mostly interesting because of the negative part: if you take any one-variable equation in the language of Heyting algebras apart from LEM or the two trivial equations, you can construct infinite Heyting algebras where all these equations hold for all but finitely many elements, and therefore will hold with probability zero on _any_ measure that doesn't assign positive measure to singletons.
Zoltan A. Kocsis (Feb 28 2024 at 12:47):David Michael Roberts said:
However, see https://mathoverflow.net/a/180020/4177 where not even finite semigroups are guaranteed to admit an invariant measure
Quite right! Invariant measures won't help much here, since the Heyting algebra operations are, unlike group operations, highly non-bijective. In fact, in many infinite algebras of interest, applying certain HA operations "squashes down" intuitively very large subsets to finite ones, and you generally don't want to concentrate all your measure on a finite set of elements.
But there are other gadgets that allow us to assign reasonable notions of density to subsets of Heyting algebras. I point out some of these in my reply to @Morgan Rogers (he/him) above. A good measure on a Heyting algebra would presumably be something that interacts nicely with these particular gadgets, much like the good measures of group theory interact nicely with the notion of index. The existence of such measures is an interesting question, although I'm personally focusing on things that you can say _without_ fixing a measure for the moment.
Benjamin Merlin Bumpus (he/him) (Feb 28 2024 at 13:49):I see I've joined the party late, but I guess this is the benefit of having a collaborator who is awake while you sleep! Obviously I second everything Zoltan said, and I want to join-in in emphasizing that the negative part of our results is particularly interesting for the infinite case.
Mike Shulman (Feb 28 2024 at 16:19):Thanks for that detailed response! I look forward to seeing the futher results you suggest.
It does seem to me that if one wants to draw philosophical conclusions involving "observations about the real world", then the countable free/presented Heyting algebras are not necessarily as interesting as those that arise "naturally" in semantic toposes, which might be more likely to admit an interesting measure.
Benjamin Merlin Bumpus (he/him) (Feb 28 2024 at 16:40):Mike Shulman said:
Thanks for that detailed response! I look forward to seeing the futher results you suggest.
It does seem to me that if one wants to draw philosophical conclusions involving "observations about the real world", then the countable free/presented Heyting algebras are not necessarily as interesting as those that arise "naturally" in semantic toposes, which might be more likely to admit an interesting measure.
Yes, definitely, I agree with you completely. In fact we don't draw any such conclusions, but we are simply motivated by the desire to.
Tomรกลก Jakl (Feb 28 2024 at 19:41):Just wanted to add a related reference. In Nesetril + Ossona de Mendez' A Model Theory Approach to Structural Limits they define precisely the same thing as what the blog post calls "degree of satisfiability". In the Nesetril + Ossona de Mendez' theory these are called Stone pairings (in subsequent papers), see Definition 1 (page 8) in the above reference.
Zoltan A. Kocsis (Feb 28 2024 at 22:25):Ralph Sarkis said:
Can this also be seen as a theoretical confirmation of the paradox of Zaionc (I learned it from here) saying that "asymptotically almost all classical theorems are intuitionistic" ?
Putting the two questions in the same language (very very roughly!) might help illuminate the differences.
LEM (xโจยฌx=T) would be one of the laws that you exclude from the count in Zaionc's case (since intuitionistic propositions don't all satisfy LEM). On the other hand, we would ignore something like xโ(xโจx)=T (since all intuitionistic propositions satisfy it, there's nothing for us to count), whereas that's precisely the thing Zaionc wants to find.
Of course, to make this precise, you have to pin down the notion of classical/intuitionistic logical law/identity, and explain when you consider two classical identities the same. This also differs in the two settings. When people investigate Zaionc's paradox, they consider two identities the same only if they're syntactically the same (perhaps up to alpha-equivalence). This is way too coarse for us, we consider two identities the same if there cannot be any intuitionistic proposition that satisfies one but not the other.
Zaionc's paradox also depends on some details of the enumeration, which is why Genitrini and Kozik get that in the full propositional language, only 5/8 of classical tautologies are intuitionistically valid (it's an amusing coincidence, but this 5/8 is not related to Gustafson's group-theoretic 5/8). For the purposes of their article, the exact number that they get is not all that important, though: the most interesting part is that one can count this at all, and the general technique that they use to pin down the value.
John Baez (Feb 29 2024 at 02:53):Thanks, that clarifies things!
Notification Bot (Feb 29 2024 at 04:00):This topic was moved here from #theory: category theory > How often does the law of excluded middle hold? by Matteo Capucci (he/him).
Valeria de Paiva (Mar 05 2024 at 22:47):hi @Zoltan A. Kocsis and @Benjamin Merlin Bumpus (he/him) . thanks for the explanations! I wonder if your work would allow you also to count the number of linear implicative propositions that satisfy a intuitionistic implicative law? this was my original interest when I started working with Paul Tarau and talking to Pierre Lescanne about Zaionc's result. you can see the analogy, right? every provable implicative linear logic proposition is also a provable intuitionistic implicative proposition, but not conversely.
Zoltan A. Kocsis (Mar 07 2024 at 00:52):Hi @Valeria de Paiva.
I would love to give this some further thought, and hope we'd be able to say something useful about linear logic.
However, I don't think there are any off-the-shelf solutions where we could deploy the techniques developed for the intuitionistic case directly to questions about linear logic. Our intuitionistic logic results leaned on some fairly specific knowledge. For example, our results about classical identities in multiple variables rely partly on the Pitts quantifier theorem, and on a (not difficult, but fairly obscure) result of Yankov.
If you think this would be an interesting avenue to explore further, or if it such results could be of use in your projects, I'll try to get up to speed on some relevant results about linear logic and evaluate our options, but this will take me some time. Are you interested in some specific identities, or about what can be said generally?
Valeria de Paiva (Mar 07 2024 at 01:19):Hi @Zoltan A. Kocsis , let me explain why I thought there might be an off the shelf adaptation to linear logic. the paper by Pierre Lescanne mentioned by @Ralph Sarkis above simply counts the number of implicative intuitionistic propositions that are also classically valid. Paul Tarau's paper on intuitionistic logic, by contrast, constructs these propositions or theorems (as lambda terms) for increasing numbers of variables. My work with Paul then says that his algorithm for constructing the intuitionistic lambda-terms can be adapted to be linear by a simple modification, see
Deriving Theorems in Implicational Linear Logic, Declaratively. So it seemed to me that your way of looking at Lescanne's proof could possibly be adapted to linear logic too. but of course we're dealing with inferences, not models, so maybe you're right, the adaptation won't work so smoothly.