Expressive equivalence of least and inflationary fixed-point logic
Proceedings - Symposium on Logic in Computer Science - Trang 403-410
Tóm tắt
We study the relationship between least and inflationary fixed-point logic. By results of Gurevich and Shelah (1986), it has been known that on finite structures both logics have the same expressive power. On infinite structures however the question whether there is a formula in IFP not equivalent to any LFP-formula was still open. In this paper, we settle the question by showing that both logics are equally expressive on arbitrary structures. The proof will also establish the strictness of the nesting-depth hierarchy for IFP on some infinite structures. Finally, we show that the alternation hierarchy for IFP collapses to the first level on all structures, i.e. the complement of an inflationary fixed-point is an inflationary fixed-point itself.
Từ khóa
#Logic #Relational databases #Polynomials #Computer science #History #Arithmetic #Database languages #Calculus #Computational complexity #Artificial intelligenceTài liệu tham khảo
vardi, 1982, The complexity of relational query languages, Proceedings of the 14th ACM Symposium on the Theory of Computing, 137
moschovakis, 1974, On non-monotone inductive definability, Fundamenta Mathematica, 82, 39, 10.4064/fm-82-1-39-83
niwin?ski, 1986, On fixed point clones, LNCS, 226, 464
10.1007/3-540-44802-0_20
bradfield, 1998, The model ?-calculus alternation hierarchy is strict, Theoretical Computer Science, 195, 133, 10.1016/S0304-3975(97)00217-X
aczel, 1977, An introduction to inductive definitions, Handbook of Mathematical Logic Volume 90 of Studies in Logic, 739, 10.1016/S0049-237X(08)71120-0
moschovakis, 1974, Elementary Induction on Abstract Structures
gurevich, 1986, Fixed-point extensions of first-order logic, Annals of Pure and Applied Logic, 32, 265, 10.1016/0168-0072(86)90055-2
emerson, 1986, Efficient model checking in fragments of the propositional mu-calculus, Proc on the First Symp on Logic in Computer Science (LICS), 267
ebbinghaus, 1999, Finite Model Theory
10.2178/bsl/1182353853
1982, Proc 14th Ann ACM Symp on Theory of Computing, 147
10.1016/S0019-9958(86)80029-8