The Descriptive complexity of the fixed-points of bounded formulas

We investigate the complexity of the fixed-points of bounded formulas in the context of finite set theory; that is, in the context of arbitrary classes of finite structures that are equipped with a built-in BIT predicate, or equivalently, with a built-in membership relation between hereditarily finite sets (input relations are allowed). We show that the iteration of a positive bounded formula converges in polylogarithmically many steps in the cardinality of the structure. This extends a previously known much weaker result. We obtain a number of connections with the rudimentary languages and deterministic polynomial-time. Moreover, our results provide a natural characterization of the complexity class consisting of all languages computable by bounded-depth, polynomial-size circuits, and polylogarithmic-time uniformity. As a byproduct, we see that this class coincides with LH(P), the logarithmic-time hierarchy with an oracle to deterministic polynomial-time. Finally, we discuss the connection of this result with the well-studied algorithms for integer division