<p>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.</p>

<p>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.</p>

<p>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.</p>

<p>Are these axioms <em>true</em>? 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 <em>scientific</em> induction, which may always be falsified by experiment -- Edward Nelson has famously hoped to prove exponentiation is a partial function! </p>

CC BY-SA 2.5
2010-11-16T19:00:09.110Z
2010-11-16T19:00:09.110Z
Neel Krishnaswami
<p>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?</p>

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

<p>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.</p>

<p>For completeness, here are the definitions from <a href="http://www.math.ohio-state.edu/~friedman/pdf/MITLogicSem110309.pdf" rel="nofollow">Friedman's MIT talk from November 2009</a> (see also the <a href="http://www.math.ohio-state.edu/~friedman/manuscripts.html" rel="nofollow">draft book on "Boolean Relation Theory"</a>).</p>

<p>$Q$ is the set of rational numbers.  $x, y \in Q^k$ are <em>order equivalent</em> 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 <em>upper shift</em> 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 <em>order invariant</em> if for every order <strike>invariant</strike> <em>equivalent</em> $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 <em>strictly dominating</em> 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$.</p>

<hr>

<p><em>Edit:</em> 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.  <strike>Any comments on whether there are any hidden non-obvious definitional problems, such as perhaps an implicit nonstandard model of the rationals?</strike></p>

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

CC BY-SA 2.5
2010-11-17T12:05:11.853Z
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?
domotorp
CC BY-SA 2.5
2010-11-17T17:12:56.533Z
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.
András Salamon
CC BY-SA 2.5
2010-11-17T22:33:34.883Z
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?
domotorp
CC BY-SA 2.5
2010-11-18T11:53:23.710Z
You have a good point, have added a note and will need to do some more digging.
András Salamon
CC BY-SA 2.5
2010-11-19T09:10:52.027Z
@domotorp: Mystery resolved: check the definition of us(x) again.
András Salamon
CC BY-SA 2.5
2010-11-19T10:06:06.907Z
Right, thanks! For k=1 there are no other relations (right?), so in this case we have proved the theorem, if I understood it correctly. I guess the unprovability comes from the fact that we have to prove it for all k.
domotorp
CC BY-SA 2.5
2010-11-19T10:29:55.230Z
@domotorp: For all $k$ sounds like the easy part, for all $R$ sounds hard.
András Salamon
CC BY-SA 2.5
2010-11-20T01:03:09.987Z
Why, isn't |SDOI| bounded by some function of k?
domotorp
CC BY-SA 2.5
2010-11-21T20:32:49.013Z
@domotorp: A priori, I would think that |SDOI| must be uncountably infinite for even small $k$.  Certainly |SDOI| is at least countably infinite even for $k=1$.
András Salamon
CC BY-SA 2.5
2010-11-21T21:55:16.060Z
Why, I think there are only a finite number of order invariant relations. For k=1 there are only 8 depending on whether (0,1), (0,0) and (1,0) are in the relation or not. (And 4 of these are strictly dominating.)
domotorp
CC BY-SA 2.5
2010-11-21T22:45:20.173Z
@domotorp: you are right; back to the drawing board.  If there are only finitely many SDOI relations for each k, then I don't see how this can be unprovable.  This is even more intriguing than initially!
András Salamon
<computability><lo.logic>
Computational consequences of Friedman's (unprovable) Upper Shift Fixed Point theorem?
András Salamon
# Computational consequences of Friedman's (unprovable) Upper Shift Fixed Point theorem?

(Asked by: username_0 on 2010-11-16)

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](http://www.math.ohio-state.edu/~friedman/pdf/MITLogicSem110309.pdf) (see also the [draft book on "Boolean Relation Theory"](http://www.math.ohio-state.edu/~friedman/manuscripts.html)).

$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.

**Tags:** computability, lo.logic

> **Comments:**
> **username_1**: 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?  
> **username_0**: 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.  
> **username_1**: 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?  
> **username_0**: You have a good point, have added a note and will need to do some more digging.  
> **username_0**: @username_1: Mystery resolved: check the definition of us(x) again.  
> **username_1**: Right, thanks! For k=1 there are no other relations (right?), so in this case we have proved the theorem, if I understood it correctly. I guess the unprovability comes from the fact that we have to prove it for all k.  
> **username_0**: @username_1: For all $k$ sounds like the easy part, for all $R$ sounds hard.  
> **username_1**: Why, isn't |SDOI| bounded by some function of k?  
> **username_0**: @username_1: A priori, I would think that |SDOI| must be uncountably infinite for even small $k$.  Certainly |SDOI| is at least countably infinite even for $k=1$.  
> **username_1**: Why, I think there are only a finite number of order invariant relations. For k=1 there are only 8 depending on whether (0,1), (0,0) and (1,0) are in the relation or not. (And 4 of these are strictly dominating.)  
> **username_0**: @username_1: you are right; back to the drawing board.  If there are only finitely many SDOI relations for each k, then I don't see how this can be unprovable.  This is even more intriguing than initially!  

---

## 1 answers

### Answer by username_2 on 2010-11-16. Score: 8 | Accepted answer

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!


---

