Definability of second order generalized quantifiers (Q964457)

The article introduces a notion of when a second-order generalized quantifier \(Q\) is definable in a logic \(L\). The structures considered are always finite and the logics are always extensions of first-order logic, \text{FO}, by generalized (first or second-order) quantifiers. First it is shown that if \(Q\) is definable in \(\text{FO}(B)\), where \(B\) is a collection of Lindström quantifiers, then \(\text{FO}(Q,B)\equiv\text{FO}(B)\), i.e. the logics \(\text{FO}(Q,B)\) and \(\text{FO}(B)\) have the same expressive power on finite structures. Then the paper focuses mostly on second-order generalized quantifiers of `type ((1))'; such a quantifier \(Q\) corresponds to a class of finite second-order structures of the form \((M,G)\) where \(G\) is a subset of \(P(M)\), the powerset of \(M\), which is closed under isomorphism. The author proves that if \(B\) is the collection of all Lindström quantifiers and \(Q\) a second-order generalized quantifier of type ((1)), then \(Q\) is definable in \(\text{FO}(B)\) \textit{by a flat formula} if and only if, for some positive integer \(n\), membership of \((M,G)\) in \(Q\) depends only on whether \((M,G(n))\) belongs to \(Q\), where \(G(n)\) is the set of all \(X\) in \(G\) such that \(|X| < n\) or \(|M - X| < n\). Roughly speaking, a formula in \(\text{FO}(B)\) is \textit{flat} if no nesting occurs of an auxiliary first-order quantifier symbol which plays a role in the definition of \(Q\) being definable in \(\text{FO}(B)\). The author proves that if \(B\) is the collection of all Lindström quantifiers, then there are several generalized second-order quantifiers which are not definable in \(\text{FO}(B)\); examples include \(n\)-ary second-order existential quantification, for every \(n\). Furthermore, for every countable collection \(B\) of Lindström quantifiers, there is a second-order generalized quantifier \(Q\) of type ((1)) such that \(\text{FO}(Q,B)\equiv\text{FO}(B)\) and \(Q\) is not definable in \(\text{FO}(B)\). Hence, the converse of the first result mentioned above does not hold. Finally, it is proved that if \(B\) is the collection of all Lindström quantifiers, then there is a generalized second order quantifier \(Q\) of type ((1)) such that \(\text{FO}(Q)\equiv \text{FO}\) and \(Q\) is not definable in \(\text{FO}(B)\).