[TYPES] Gödel's T extended with an eta-like rul e for the recursor

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Let N be the natural numbers and A any type in the hierarchy of simple
types over N. Let s : (N)N be the successor function and let f : (N)A be
arbitrary. Then, for variables x : N, y : A we may form the term

[x, y]f(s(x)) : (N)(A)A

Let R be the recursor for type A. Then, for any term n : N, we have

R( f(0) , [x, y]f(s(x)) , n ) : A

By the reduction rules for R one can see that f and R( f(0) , [x, y]f(s(x))
) agree on the numerals.

Suppose we add the following eta-like reduction rule to Gödel's T:

R( f(0) , [x, y]f(s(x)) , x ) --> f(x)

Is it known whether the resulting system is (strongly) normalizing and
confluent?


------------
Ansten Klev
Czech Academy of Sciences, Department of Philosophy