Category Theory
Zulip Server
Archive

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.

Stream: theory: category theory

Topic: How often does the law of excluded middle hold?

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 $\top$ 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