<div dir="ltr"><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><font face="verdana, sans-serif">EricS,<br><br>You write:<br><i style="">I bring up this debate in mathematics because it seems significant to me<br>how long and how intensely it has been going on, with both sides wanting a<br>notion of “truth”, and neither being able to claim to have achieved it in terms<br>satisfied by the other.  If the intuitionists had never been able to build a<br>real system around their position, the formalists could just declare victory<br>and go home.  But the debate seems still live, even within math and not only in<br>philosophy, with clear trade-offs that there are proofs that each side will<br>accept that the other rejects.</i><br><br>It would surprise me to meet a mathematician who feels intensely one way<br>or an other about a particular choice of topos. For mathematical-logicians,<br>what seems more interesting are the geometric morphisms between toposes.<br>I would argue that the formalists to some extent <b>did</b> <i>just declare victory</i><br>many times over and that their are still pockets of scientific/mathematical<br>culture that believe everything can be <i>reduced to bits</i>. Still, and not just as<br>with the intuitionists, richer toposes are there to be found and explored.<br><br></font></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><font face="verdana, sans-serif">My two favorite examples come from algebraic geometry and from</font></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><font face="verdana, sans-serif">quantum cosmology. In the former case, Grothendieck arrives at the</font></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><font face="verdana, sans-serif">idea of a non-boolean topos while writing the foundations of algebraic</font></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><font face="verdana, sans-serif">geometry. In the latter, <a href="https://en.wikipedia.org/wiki/Fotini_Markopoulou-Kalamara">Fontini Markopoulou-Kalamara</a> develops her</font></div><div class="gmail_default" style="font-size:small;color:rgb(51,51,51)"><font face="verdana, sans-serif">non-boolean topos in the context of quantum gravity†.<br><br>Jon<br><br>†) Tangentially related to other parts of the overall discussion, Fotini<br>is also a design engineer working on embodied cognition technologies.</font><br></div></div>