Scott Garrabrant’s problem on recovering Brouwer as a corollary of Lawvere

Edit: Pre-print available here https://​​​​abs/​​2005.01563

Also link to ear­lier post here https://​​­ign­ment­fo­​​posts/​​5bd75cc58225bf06703753a9/​​for­mal-open-prob­lem-in-de­ci­sion-the­ory?fb­clid=IwAR2u-8RVfn­fRtEo51vag5vYWAcfkoHDJAr6ay­dVGqYVmEq0oxn­jwR0Ee34E

Scott Garrabrant has raised the ques­tion of whether there is any topolog­i­cal space for which the ex­po­nen­tial topol­ogy on ex­ists and such that there is a con­tin­u­ous sur­jec­tion . In cited pre-print above I claim to re­solve this ques­tion nega­tively in ZFC (us­ing tech­niques of in­ner model the­ory, Skolem hull ar­gu­ments, and some Re­v­erse Math­e­mat­ics re­sults pre­sented by Stephen Simp­son in “Sub­sys­tems of Se­cond Order Arith­metic”) but also to give an ex­am­ple of a pair of spaces with the same car­rier set, topol­ogy on finer than that on , and a con­tin­u­ous sur­jec­tion with the fol­low­ing prop­er­ties. Take an open sub­set of , take pre-image in un­der eval­u­a­tion map, take pro­jec­tion onto first fac­tor and then pre-image un­der sur­jec­tion , and view this both as a sub­set of and (which have the same car­rier set), this is re­quired to be always open rel­a­tive to both topolo­gies. If this can be achieved then Brouwer fixed point the­o­rem is re­cov­er­able as a corol­lary with “same method of proof” as Law­vere. Re­sults along these lines ap­pear to be es­sen­tially “the best one can do”.

My first ex­am­ple of such a pair of spaces are spaces of car­di­nal­ity which may lead one to think that prac­ti­cal ap­pli­ca­tions are doubt­ful. But there are tech­niques to pro­duce a broad class of re­lated ex­am­ples by re­fin­ing things both along the hi­er­ar­chy of de­scrip­tive com­plex­ity and in­deed even com­pu­ta­tional com­plex­ity. The de­tails of this are out­lined in the fi­nal sec­tion of the pa­per.

One ex­am­ple of a re­sult that can be ob­tained is as fol­lows. Let be the least countable or­di­nal such that there is no polyno­mial-time com­putable re­cur­sive well-or­der­ing of length . (I think it’s prob­a­bly or some­thing, not sure, but this could be figured out. EDIT: Alex Men­nen has clar­ified I was mis­taken about this and the or­di­nal is in fact , which per­haps makes this par­tic­u­lar re­sult of less in­ter­est.) Let be a space of agents in­dexed by re­cur­sive well-or­dered bit-strings of length with some fixed up­per bound on the com­pu­ta­tion com­plex­ity if you wish (but we’ll see we can’t or­ganise it so that they’re all polyno­mial-time com­putable).

Then you do in­deed have a con­tin­u­ous sur­jec­tion from onto the space of all polyno­mial-time-com­putable poli­cies, but you can’t or­ganise things so that ev­ery el­e­ment of is polyno­mial-time com­putable, or so that the sur­jec­tion it­self is polyno­mial-time com­putable. (Edit: By plac­ing an up­per bound on com­plex­ity of bit-strings that can oc­cur in that means ends up be­ing countable, that’s prob­a­bly a bit con­fus­ing, but it’s pos­si­ble to ex­pand so that ar­bi­trary bit-strings can oc­cur in its car­rier set and the same re­sult stated at the start of this para­graph still holds.) Similar re­sults can be ob­tained through­out the en­tire com­pu­ta­tional com­plex­ity hi­er­ar­chy or de­scrip­tive com­plex­ity hi­er­ar­chy. This may be of some in­ter­est from the point of view of the type of ap­pli­ca­tion that Scott Garrabrant origi­nally had in mind when pos­ing the prob­lem in the first place.