# Computational consequences of Friedman's (unprovable) Upper Shift Fixed Point theorem?

Harvey Friedman showed that there is a neat fixed point result that cannot be proved in ZFC (the usual Zermelo-Frankel set theory with the Axiom of Choice). Many modern logics are built on fixed point operators, so I was wondering: are there any consequences known of the Upper Shift Fixed Point theorem for theoretical computer science?

Unprovable Upper Shift Fixed Point Theorem
For all $R \in \text{SDOI}(Q^k,Q^k)$, some $A = \text{cube}(A,0) \setminus R[A]$ contains $\text{us}(A)$.

The USFP Theorem seems to be a $\Pi^1_1$ statement, so it might be "close enough" to computability (such as checking non-isomorphism of automatic structures), to impact theoretical computer science.

For completeness, here are the definitions from Friedman's MIT talk from November 2009 (see also the draft book on "Boolean Relation Theory").

$Q$ is the set of rational numbers. $x, y \in Q^k$ are order equivalent if whenever $1 \le i,j \le k$ then $x_i \lt x_j \Leftrightarrow y_i \lt y_j$. When $x \in Q^k$ then the upper shift of $x$, denoted $\text{us}(x)$, is obtained by adding 1 to every non-negative coordinate of $x$. A relation $A \subseteq Q^k$ is order invariant if for every order invariant equivalent $x,y \in Q^k$ it holds that $x \in A \Leftrightarrow y \in A$. A relation $R \subseteq Q^k \times Q^k$ is order invariant if $R$ is order invariant as a subset of $Q^{2k}$, and is strictly dominating if for all $x,y \in Q^k$ whenever $R(x,y)$ then $\max(x) \lt \max(y)$. Further if $A$ is a subset of $Q^k$ then $R[A]$ denotes $\{ y | \exists x \in A R(x,y)\}$, the upper shift of $A$ is $\text{us}(A) = \{\text{us}(x) | x \in A\}$, and $\text{cube}(A,0)$ denotes the least $B^k$ such that $0 \in B$ and $A$ is contained in $B^k$. Let $\text{SDOI}(Q^k,Q^k)$ denote the set of all strictly dominating order invariant relations $R \subseteq Q^k \times Q^k$.

Edit: As Dömötör Pálvölgyi points out in comments, taking $k=1$ and $R$ to be the usual ordering on rationals seems to yield a counterexample. First, the set $A$ cannot be empty, as $R[A]$ is then also empty and $A$ would then have to contain 0 by the cube condition, a contradiction. If the non-empty set $A$ has an infimum then it cannot contain any rationals greater than this, so it must be a singleton, which contradicts the upper shift condition. If on the other hand $A$ has no infimum then $R[A] = Q$ so $A$ must be empty, a contradiction. Any comments on whether there are any hidden non-obvious definitional problems, such as perhaps an implicit nonstandard model of the rationals?

Further edit: The argument above is roughly correct, but is wrong in the application of the upper shift. This operator only applies to non-negative coordinates, so setting $A$ to be any negative singleton set yields a fixed point, as desired. In other words, if $m < 0$ then $A = \{m\}$ is a solution, and there are no other solutions.

• Could someone please explain to me the statement in more detail? Eg. if k=1 and R is x<y, then what will be A? Nov 17, 2010 at 12:05
• R is SDOI. If A has no infimum, then R[A] will be Q, and A is empty. So let m be the infimum of A. Then R[A] will include all rationals above m. Hence A must exclude all rationals above m, so must be precisely the singleton set containing m. However, us(A) must then contain m+1, contradiction. So the only consistent case is that A is empty. Nov 17, 2010 at 17:12
• I was thinking along the same lines, but I feel a little cheated. Why does cube(A,0) not contain 0? Maybe I don't understand the definition of something. If the empty set works in this case, why would it not work for all R? Nov 17, 2010 at 22:33
• You have a good point, have added a note and will need to do some more digging. Nov 18, 2010 at 11:53
• @domotorp: Mystery resolved: check the definition of us(x) again. Nov 19, 2010 at 9:10