On bounded theories. (English) Zbl 0783.03020
Börger, Egon (ed.) et al., Computer science logic. 5th workshop, CSL ’91, Berne, Switzerland, October 7-11, 1991. Proceedings. Berlin etc.: Springer-Verlag. Lect. Notes Comput. Sci. 626, 111-118 (1992).
Arising in the context of the relationship between the computational complexity of a query and its expressibility in first-order logic with a fixed number of bound variables, N. Immerman and D. Kozen [Inf. Comput. 83, 121-139 (1989; Zbl 0711.03004)] have studied theories satisfying the “\(k\)-variable property” (every first-order formula is equivalent under theory \(\Sigma\) to a formula with at most \(k\) bound variables). Since the notion of \(k\)-variable property of Immerman and Kozen [loc. cit.] proved to be not “stable”, the author introduces the (more restrictive) notion of \(k\)-boundedness: a theory \(\Sigma\) is \(k\)- bounded if every first-order formula \(\varphi(x_ 1,\dots,x_ n)\), with \(n\geq k\), is equivalent to a formula \(\psi(x_ 1,\dots,x_ n)\) with bound variables among \(x_ 1,\dots,x_ n\) such that in each subformula at most \(k\) variables are in the scope of a quantifier of \(\varphi\). The new definition entails interesting results: (1) Every \(k\)-bounded theory is \((k+1)\)-bounded; (2) Every \(k\)-bounded theory has the \(k\)-variable property; (3) The examples of theories of Immerman and Kozen [loc. cit.] having the \(k\)-variable property are \(k\)-bounded; (4) There is an algebraic characterization of \(k\)-boundedness in terms of partial isomorphisms; (5) The use of \(\omega\)-saturated structures simplifies considerably the proofs.
For the entire collection see [Zbl 0772.68004].
For the entire collection see [Zbl 0772.68004].
Reviewer: N.Curteanu (Iaşi)
MSC:
03D15 | Complexity of computation (including implicit computational complexity) |
68Q25 | Analysis of algorithms and problem complexity |
03B25 | Decidability of theories and sets of sentences |
03B20 | Subsystems of classical logic (including intuitionistic logic) |