Commutativity of addition in polymorphic lambda calculus

Question

In the article "Extensional models of polymorphism" by Breazu-Tannen and Coquand, natural numbers are presented using a Church-like encoding:

$polyint = \forall t . (t \to t) \to t \to t$

Addition for this encoding is introduced as:

$\mathsf{Add} = \lambda u,v : polyint . \Lambda t . \lambda f : t \to t . \lambda x : t . u t f (v t f x)$

Then they say that commutativity of addition cannot be proved, and they say that $\mathsf{Add} u v = \mathsf{Add} v u$ does not follow from polymorphic lambda calculus theory by a simple Church-Rosser argument. What's this Church-Rosser argument? Is it related to the Church-rosser property? How can I prove it?

EDIT: the exact statement is:

"However, the pure $\lambda^{\forall}$ is not sufficient for that, as it cannot even prove, for example, that the operation of addition is commutative:

$\mathsf{Add}\ u\ v = \mathsf{Add}\ v\ u$

with arbitrary $u, v : polyint$ is not provable in $\lambda^{\forall}$ (by a simple Church-Rosser argument)".

Answer 1

The fact that $\mathsf{Add}\ u\ v = \mathsf{Add}\ v\ u$ is not provable for arbitrary $u$ and $v$ does indeed follow from the Church-Rosser property.

Write $u =_\beta v$ if $u \mathrel{({}_\beta\!\!\leftarrow\cup\rightarrow_\beta)^\ast} v$, where $\rightarrow_\beta$ is $\beta$-reduction in System F and $(\cdot)^\ast$ is the reflexive-transitive closure operator (this is a possible definition of $\beta$-equality, which Breazu-Tannen and Coquand denote simply by $=$. Here I will use the $\beta$ subscript and keep the $=$ symbol for strict equality, i.e., $\alpha$-equivalence if you like). It follows immediately from the definition that if two terms have a common reduct, i.e., $u\rightarrow_\beta^\ast w$ and $v\rightarrow_\beta^\ast w$, then $u=_\beta v$. The Church-Rosser theorem states that the converse also holds: $$u=_\beta v \quad \textrm{implies}\quad \exists w.\ u\rightarrow^\ast w\textrm{ and }v\rightarrow^\ast w.$$ It follows that $\beta$-equivalent normal forms are necessarily identical: $$u,v\textrm{ normal and }u=_\beta v\textrm{ implies }u=v.$$

Read contrapositively, the above says that different normal forms can never be $\beta$-equivalent. Now, suppose $\mathsf{Add}\ u\ v=_\beta\mathsf{Add}\ v\ u$ for arbitrary $u$, $v$. In particular, this holds when $u=x$ and $v=y$ are distinct variables of type $polyint$. But it is easy to show (just apply a couple of steps of $\rightarrow_\beta$) that $\mathsf{Add}\ x\ y=_\beta u'$ and $\mathsf{Add}\ y\ x=_\beta v'$ with $u'$ and $v'$ distinct normal forms. Contradiction.