We consider the language of ?0-formulas with list terms interpreted over hereditarily finite list superstructures. We study the complexity of reasoning in extensions of the language of ?0-formulas with non-standard list terms, which represent bounded list search, bounded iteration, and bounded recursion. We prove a number of results on the complexity of model checking and satisfiability for these formulas. In particular, we show that the set of ?0-formulas with bounded recursive terms true in a given list superstructure HW(M) is non-elementary (it contains the class kExpTime, for all k 1). For ?0-formulas with restrictions on the usage of iterative and recursive terms, we show lower complexity.
展开▼
