Lower bound results on lengths of second-order formulas (Q1071760)

Let L be the language of second order predicate calculus with equality \(=\) and ordering \(<\). C(s,h) denotes the class of prenex formulas from L such that \(F\in C(s,h)\) iff: (1) the only free variable in F is monadic, (2) only predicate variables with \(\leq s\) number of places occur in F, (3) the prefix of F has \(\leq h\) quantifier changes. A formula G belongs to the class \(C^*(s,h)\) iff there is an \(F\in C(s,h)\) and a two place predicate variable Q free for in F such that G results from F by substitution of Q for \(<\). F(P)\(\in C(s,h)\) is true in \(D_ n=\{0,...,n- 1\}\) under the assignment of \(P^*\subseteq D_ n\) to P if it is true when second order quantifiers range over the associated set of relations on \(D_ n\), while individual quantifiers range over \(D_ n\), with \(=\), \(<\) interpreted as equality and natural order on \(D_ n\). \(| F(P)|\) denotes the length of F(P). The basic result is: Theorem 1: There are integers \(A,c>0\) as follows. Given \(s\geq 3\), \(h\geq 0\) there is a formula E(P)\(\in C(s+1,c+h+2s)\) and an \(n_ s\) with the property: (*) if \(n\geq n_ s\), \(t\leq s-3\) and F(P)\(\in C(t,h)\) are such that F(P)\(\equiv E(P)\) is identically true on \(D_ n\), then \(| F(P)|^ 3\geq (At^ 2)^{-1}n^{s-t-2}\). The formula E(P) has \(\leq h+6\) second order quantifier changes. Definition: For \(F(P,Q)\in C^*(s,h)\) (P monadic, Q second order) put \(S_ n(F)=\{(P^*,Q^*)/\) \(P^*\subseteq D_ n\), \(Q^*\subseteq D^ 2_ n\) and \(F(P^*,Q^*)\) true in \(D_ n\}\). The set \(S(F)=\{S_ n(F)/\) \(n=1,2,...\}\) is the generalized second order spectrum of F. Corollary: Let c be as in theorem 1, \(s\geq 3\), \(h\geq 0\). Then there is a formula E(P,Q)\(\in C^*(s+1,c+h+2s)\) such that S(F)\(\cap S(E)\) is finite whenever \(t\leq s-3\) and F(P,Q)\(\in C^*(t,h).\) There are further results of a similar type. The proofs are based on techniques introduced by the author in Trans. Am. Math. Soc. 284, 203-218 (1984; Zbl 0548.03018).