Addendum to: Finite Variable Logics.
Ian Hodkinson · Bulletin of the European Association for Theoretical Computer Science · 1994
8. p 133, k-variable property. Related results are given in the paper On bounded theories by J. Flum (in Proc. Computer Science Logic 91, Berne, eds. E. Boerger, G. Jaeger, H. Kleine Buening, M.M. Richter, Springer LNCS 626, 111–118). There, a first-order theory T in signature L is said to be k-bounded if (essentially) every first-order L-formula is T -equivalent to one where at most k distinct variables are bound in any branch of its formation tree. If L is relational, of arity < k, then it can be shown (cf. [HS, §3.2]) that T is k-bounded iff for all n ≥ k, every formula φ(x1, . . . , xn) is T -equivalent to a formula φ (x1, . . . , xn) written with only n variables (‘T has the non-monadic n-variable property for all n ≥ k’). Flum also gives an example (suggested by Ziegler) of a theory T that is not k-bounded for any k, but such that any formula can be equivalently rewritten over T using only one bound variable. (The example of [HS] mentioned on p 133 is in some ways similar.)