Choose a variable name among the available names and defineThe formula is obtained by interchanging the names throughout , including bound occurrences. Its only free variable is . A permutation of variable names preserves membership in , so every formula in this recursion still uses at most the original names. In particular, bound variables inside a copy of do not accidentally capture the previous comparison: their scope stays inside that copy.
Induction proves that holds exactly when there is an increasing -tuple of satisfying elements whose first entry is . Any set of distinct points in a linear order can be put in increasing order. Therefore the variable-recycling count on a linear orderis the required sentence. This does not use counting quantifiers or additional variable names, and it applies equally to infinite linear orders.
Articles by others on the same topic
There are currently no matching articles.