Complexity of syntactical tree fragments of Independence-Friendly logic
Abstract
A dichotomy result of Sevenster (2014) completely classified the quantifier prefixes of regular Independence-Friendly (IF) logic according to the patterns of quantifier dependence they contain. On one hand, prefixes that contain "Henkin" or "signalling" patterns were shown to characterize fragments of IF logic that capture NP-complete problems; all the remaining prefixes were shown instead to be essentially first-order. In the present paper we develop the machinery which is needed in order to extend the results of Sevenster to non-prenex, regular IF sentences. This involves shifting attention from quantifier prefixes to a (rather general) class of syntactical tree prefixes. We partially classify the fragments of regular IF logic that are thus determined by syntactical trees; in particular, a) we identify three tree prefixes that are neither signalling nor Henkin, and yet express NP-complete problems and other second-order concepts; and b) we give more general criteria for checking the first-orderness of an IF sentence.
Keywords
Cite
@article{arxiv.1610.03406,
title = {Complexity of syntactical tree fragments of Independence-Friendly logic},
author = {Fausto Barbero},
journal= {arXiv preprint arXiv:1610.03406},
year = {2019}
}
Comments
Major revision. The notion of tree reduction is now only shortly presented in Appendix C; all usages of tree reduction are replaced by sentence equivalence. One result (Thm 7.4 of previous version) downgraded to Conjecture 8.6. Corrections to statement and proof of Theorem 8.4. Proofs of Theorems 6.13 and Lemma 7.3 made more detailed and postponed to Appendixes A and B