Arity hierarchies (Q2563982)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Arity hierarchies |
scientific article |
Statements
Arity hierarchies (English)
0 references
21 April 1997
0 references
For many extensions \(L\) of first-order logic considered for finite structures there is a natural notion of arity of a formula (e.g., the maximal arity of a bounded second-order variable in a formula of fixed-point logic). Denote by \(L^k\) the fragment of \(L\) consisting of the sentences of \(L\) of arity \(\leq k\). The main lemma shows that there is a quantifier-free formula \(\varphi (x_1, \dots, x_k,y_1, \dots, y_k)\) in the language of graphs such that the transitive closure of \(\varphi\) is not expressible in \(s\text{-PFP}^{k-1}\), where \(s\text{-PFP}\) denotes simultaneous partial fixed-point logic. This result implies that the arity hierarchy (even on the class of graphs) is strict for all ``natural'' logics between transitive closure logic and \(s\text{-PFP}\) and it can be used to obtain the strictness of the corresponding hierarchies of pure DATALOG and several of its extensions and of the class of implicitly definable queries. The proof of the main lemma is based on an ingenious construction of structures ``homogeneous in the \((k-1)\)-tuples''. An iteration of this construction is needed to show the hierarchy result for deterministic transitive closure logic.
0 references
extensions of first-order logic
0 references
strictness of hierarchies
0 references
finite structures
0 references
simultaneous partial fixed-point logic
0 references
arity hierarchy
0 references
transitive closure logic
0 references
DATALOG
0 references