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

post by Rupert · 2020-05-04T10:01:56.305Z · score: 25 (10 votes) · LW · GW · 2 comments

Edit: Pre-print available here https://arxiv.org/abs/2005.01563

Also link to earlier post here https://www.alignmentforum.org/posts/5bd75cc58225bf06703753a9/formal-open-problem-in-decision-theory?fbclid=IwAR2u-8RVfnfRtEo51vag5vYWAcfkoHDJAr6aydVGqYVmEq0oxnjwR0Ee34E [AF · GW]

Scott Garrabrant has raised the question of whether there is any topological space for which the exponential topology on exists and such that there is a continuous surjection . In cited pre-print above I claim to resolve this question negatively in ZFC (using techniques of inner model theory, Skolem hull arguments, and some Reverse Mathematics results presented by Stephen Simpson in "Subsystems of Second Order Arithmetic") but also to give an example of a pair of spaces with the same carrier set, topology on finer than that on , and a continuous surjection with the following properties. Take an open subset of , take pre-image in under evaluation map, take projection onto first factor and then pre-image under surjection , and view this both as a subset of and (which have the same carrier set), this is required to be always open relative to both topologies. If this can be achieved then Brouwer fixed point theorem is recoverable as a corollary with "same method of proof" as Lawvere. Results along these lines appear to be essentially "the best one can do".

My first example of such a pair of spaces are spaces of cardinality which may lead one to think that practical applications are doubtful. But there are techniques to produce a broad class of related examples by refining things both along the hierarchy of descriptive complexity and indeed even computational complexity. The details of this are outlined in the final section of the paper.

One example of a result that can be obtained is as follows. Let be the least countable ordinal such that there is no polynomial-time computable recursive well-ordering of length . (I think it's probably or something, not sure, but this could be figured out. EDIT: Alex Mennen has clarified I was mistaken about this and the ordinal is in fact , which perhaps makes this particular result of less interest.) Let be a space of agents indexed by recursive well-ordered bit-strings of length with some fixed upper bound on the computation complexity if you wish (but we'll see we can't organise it so that they're all polynomial-time computable).

Then you do indeed have a continuous surjection from onto the space of all polynomial-time-computable policies, but you can't organise things so that every element of is polynomial-time computable, or so that the surjection itself is polynomial-time computable. (Edit: By placing an upper bound on complexity of bit-strings that can occur in that means ends up being countable, that's probably a bit confusing, but it's possible to expand so that arbitrary bit-strings can occur in its carrier set and the same result stated at the start of this paragraph still holds.) Similar results can be obtained throughout the entire computational complexity hierarchy or descriptive complexity hierarchy. This may be of some interest from the point of view of the type of application that Scott Garrabrant originally had in mind when posing the problem in the first place.

2 comments

Comments sorted by top scores.

comment by AlexMennen · 2020-05-04T18:33:53.650Z · score: 6 (3 votes) · LW(p) · GW(p)
Let α be the least countable ordinal such that there is no polynomial-time computable recursive well-ordering of length α.

, which makes the claim you made about it vacuous.

Proof: Let be any computable well-ordering of . Let be the number of steps it takes to compute whether or not . Let (notice I'm using the standard ordering on , so this is the maximum of a finite set, and is thus well-defined). is computable in time. Let be a bijective pairing function such that both the pairing function and its inverse are computable in polynomial time. Now let be the well-ordering of given by , if is not for any , and if neither nor is of the form for any . Then is computable in polynomial time, and the order type of is plus the order type of , which is just the same as the order type of if that order type is at least .

The fact that you said you think is makes me suspect you were thinking of the least countable ordinal such that there is no recursive well-ordering of length that can be proven to be a recursive well-ordering in a natural theory of arithmetic such that, for every computable function, there's a program computing that function that the given theory can prove is total iff there's a program computing that function in polynomial time.

comment by Rupert · 2020-05-04T19:13:40.926Z · score: 1 (1 votes) · LW(p) · GW(p)

Thanks for the clarification. Possibly that reduces the interest of the observations about computational complexity.