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

• 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 α.

, which makes the claim you made about it vac­u­ous.

Proof: Let be any com­putable well-or­der­ing of . Let be the num­ber of steps it takes to com­pute whether or not . Let (no­tice I’m us­ing the stan­dard or­der­ing on , so this is the max­i­mum of a finite set, and is thus well-defined). is com­putable in time. Let be a bi­jec­tive pairing func­tion such that both the pairing func­tion and its in­verse are com­putable in polyno­mial time. Now let be the well-or­der­ing of given by , if is not for any , and if nei­ther nor is of the form for any . Then is com­putable in polyno­mial time, and the or­der type of is plus the or­der type of , which is just the same as the or­der type of if that or­der type is at least .

The fact that you said you think is makes me sus­pect you were think­ing of the least countable or­di­nal such that there is no re­cur­sive well-or­der­ing of length that can be proven to be a re­cur­sive well-or­der­ing in a nat­u­ral the­ory of ar­ith­metic such that, for ev­ery com­putable func­tion, there’s a pro­gram com­put­ing that func­tion that the given the­ory can prove is to­tal iff there’s a pro­gram com­put­ing that func­tion in polyno­mial time.

• Thanks for the clar­ifi­ca­tion. Pos­si­bly that re­duces the in­ter­est of the ob­ser­va­tions about com­pu­ta­tional com­plex­ity.