A logic for constant-depth circuits

Consider a family of boolean circuitsC1,C2,…,Cn,…, constructed by some uniform, effective procedure operating on inputn. Such a procedure provides a concise representation of a family of parallel algorithms for computing boolean values. A formula of first-order logic may also be viewed as a concise representation of a family of parallel algorithms for evaluating boolean functions. The parallelism is implicit in the quantification (a formula ∀x(x) is true if and only if each of the formulas(a) is true, and all these formulas can be checked simultaneously), and universes of different sizes give rise to boolean functions with different numbers of inputs (the boolean values of the formula's predicates on various combinations of elements of the universe). This note presents an extended first-order logic designed to be exactly equivalent in expressiveness to polynomialsize, constant-depth, unbounded-fan-in circuits constructed by Turing machines of bounded computational complexity