BEGIN:VCALENDAR VERSION:2.0 PRODID:researchseminars.org CALSCALE:GREGORIAN X-WR-CALNAME:researchseminars.org BEGIN:VEVENT SUMMARY:Andrej Bauer DTSTART:20220512T170000Z DTEND:20220512T180000Z DTSTAMP:20260404T033112Z UID:ToposInstituteColloquium/57 DESCRIPTION:Title: The countable reals\nby Andrej Bauer as part of Topo s Institute Colloquium\n\n\nAbstract\nJoint work with James E. Hanson from the University of Maryland\, https://james-hanson.github.io.\n\nIn 1874 G eorg Cantor published a theorem stating that every sequence of reals is av oided by some real\, thereby showing that the reals are not countable. Can tor's proof uses classical logic. There are constructive proofs\, although they all rely on the axiom of countable choice. Can the real numbers be s hown uncountable without excluded middle and without the axiom of choice? An answer has not been found so far\, although not for lack of trying.\n\n We show that there is a topos in which the real numbers are countable\, i. e.\, there is an epimorphism from the object of natural numbers to the obj ect of Dedekind reals. Therefore\, higher-order intuitionistic logic canno t show the reals to be uncountable.\n\nThe starting point of our construct ion is a sequence of reals\, shown to exist by Joseph S. Miller from Unive rsity of Wisconsin–Madison\, with a strong counter-diagonalization prope rty: if an oracle Turing machine computes a specific real number\, when gi ven any oracle representing Miller's sequence\, then the number appears in the sequence. One gets the idea that the reals ought to be countable in a realizability topos built from Turing machines with oracles for Miller's sequence. However\, we cannot just use ordinary realizability\, because al l realizability toposes validate countable choice and consequently the unc ountability of the reals.\n\nTo obtain a topos with countable reals\, we d efine a variant of realizability which we call parameterized realizability . First we define parameterized partial combinatory algebras (ppca)\, whic h are partial combinatory algebras whose evaluation depends on a parameter . We then define parameterized realizability toposes. In these realizers w itness logical statements uniformly in the parameters. The motivating exam ple is the parameterized realizability topos built from the ppca of oracle Turing machines parameterized by oracles for Miller's sequence. In this t opos\, Miller's sequence is the desired epimorphism from natural numbers t o Dedekind reals.\n LOCATION:https://researchseminars.org/talk/ToposInstituteColloquium/57/ END:VEVENT END:VCALENDAR