Recently, in response to deciding the Continuum Hypothesis $CH$, Hamkins and Gitman have proposed consider a multiverse of set-theoretic universes, some in which $CH$ is true, some in which $\neg CH$ is true (and some in which $CH$ is not a relevant hypothesis?).

In formulating logical languages, there has been an outstanding problem: that of deciding the Law of the Excluded Middle $p\vee\neg p$. In classical logic $p\vee\neg p$ is true, but in intuitionistic logic this is not the case. With $CH$, the pragmatic mathematician tries to avoid invoking $CH$; if he assumes $CH$ or $\neg CH$, he will state it clearly. In everyday mathematics practice, the mathematician does use $p\vee\neg p$, but we do see an effort to give * effective constructions*, and *hard estimates in analysis.*

It seems that people are using classical logic basically because it's a core logic, in analogy to the constructible universe $L$ in which $CH$ is true. It is the logic first discovered (and often wrongly attributed as the Platonic choice) and the consistency and strength of other languages proven in terms of this core logic. Afterwards people come up with other logics, like Brouwer coming up with intuitionistic logic, in which a fundamental principle, the Law of the Excluded Middle, does not hold. It seems to me that this debate regarding the Law of Excluded Middle can be formalized using the multiverse approach.

So has anyone tried to use the multiverse approach towards considering these plurality of languages? Perhaps by considering a multiverse of topoi?

**PS.** The difficulty for arithemetizable syntax to describe continuous properties of geometric/measure-theoretic space is central (may I say?) to the difficulty of deciding $CH$. In a like fashion, the difference between classical and intuitionistic logic plays up in comparing the Dedekind-reals and the Cauchy-reals. In other words, continuous properties have different descriptions in these two logics. I'm hoping that work on the Law of the Excluded Middle will shed some light on trying to use discrete languages to model continuous properties. There's more where this comes from, but it is enough for now...

3more comments