Arithmetical predicates and function quantifiers

Abstract

2) The normal form and enumeration theorems for l>0 can be rewritten using a instead of 5, where sW=IIi<. P?m+1 (cf-[7]). Thus in IM pp. 291, 292 we have T?(z, a, x) = T\(a(x), z, a, x). Putting t[{w, 0, a) = T[(Y[i<a(w) pi exp (w)i~l, z, a, lh(a>)), then T\(a(x), z, a, x) = T\{a{x), z, a).