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

Question

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.

Answer 1

I don't know of any consequences of this particular theorem, but normalization proofs of lambda calculi like the calculus of inductive constructions rely on large cardinal axioms -- even though the set of lambda-terms is as countable as you could want.

I think the best way to understand the computational significance of set-theoretic axioms asserting the existence of large cardinals is to think of set theory as a way of phrasing the theory of graphs. That is, a model of a set is a collection of elements equipped with a binary relation used to interpret membership. Then, the axioms of set theory tell you properties of the membership relation, including how you can form new sets from old. In particular, the axiom of foundation means that the membership relation is well-founded (ie, it has no infinite descending chains). This well-foundedness in turn means that if you can line up the execution states of a program with the transitive membership of the elements of a set, then you have a termination proof.

So an assertion that a "big" set exists has a computational payoff as a claim that a certain class of loops in a general recursive programming language terminate. This interpretation works uniformly, all the way from the plain old axiom of infinity (which justifies natural number iteration) all the way up to large cardinal axioms.

Are these axioms true? Well, if the axiom is false you can find a program in one of these classes which doesn't terminate. But if it's true, we will never be sure, thanks to the Halting theorem. Everything from natural number induction on is a matter of scientific induction, which may always be falsified by experiment -- Edward Nelson has famously hoped to prove exponentiation is a partial function!