Premium
The quantifier complexity of polynomial‐size iterated definitions in first‐order logic
Author(s) -
Buss Samuel R.,
Johnson Alan S.
Publication year - 2010
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200910111
Subject(s) - mathematics , quantifier (linguistics) , iterated function , quantifier elimination , lemma (botany) , polynomial , discrete mathematics , order (exchange) , combinatorics , range (aeronautics) , computer science , artificial intelligence , finance , economics , composite material , biology , mathematical analysis , ecology , materials science , poaceae
Abstract We refine the constructions of Ferrante‐Rackoff and Solovay on iterated definitions in first‐order logic and their expressibility with polynomial size formulas. These constructions introduce additional quantifiers; however, we show that these extra quantifiers range over only finite sets and can be eliminated. We prove optimal upper and lower bounds on the quantifier complexity of polynomial size formulas obtained from the iterated definitions. In the quantifier‐free case and in the case of purely existential or universal quantifiers, we show that Ω( n /log n ) quantifiers are necessary and sufficient. The last lower bounds are obtained with the aid of the Yao‐Håstad switching lemma (© 2010 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)