Complexity of syntactical tree fragments of Independence-Friendly logic

TL;DR

This paper extends the classification of Independence-Friendly logic fragments from quantifier prefixes to more general syntactical tree structures, identifying new NP-complete expressing fragments and criteria for first-order characterization.

Contribution

It develops new methods to analyze non-prenex regular IF sentences using syntactical tree prefixes, expanding the classification of logical complexity.

Findings

Identifies three tree prefixes that express NP-complete problems.

Provides criteria for determining first-order nature of IF sentences.

Extends classification from quantifier prefixes to syntactical trees.

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.