Independence friendly logic with classical negation via flattening is a second-order logic with weak dependencies

SANTIAGO FIGUEIRA; DANIEL GORÍN; RAFAEL GRIMSON

JOURNAL OF COMPUTER AND SYSTEM SCIENCES

ACADEMIC PRESS INC ELSEVIER SCIENCE

Lugar: Amsterdam; Año: 2014 vol. 80 p. 1102 - 1118

0022-0000

It is well-known that Independence Friendly (IF) logic is equivalent to existential second-order logic ($Sigma^1_1$) and, therefore, is not closed under classical negation. The Boolean closure of IF sentences, called Extended IF-logic, on the other hand, corresponds to a proper fragment of $Delta^1_2$. In this article we consider slfl, IF-logic extended with Hodges´ flattening operator $downarrow$, which allows to define a classical negation. Furthermore, this negation, in Hodges´ style, may occur also under the scope of IF quantifiers. slfl contains Extended IF-logic and hence it is at least as expressive as the Boolean closure of $Sigma^1_1$. We prove that slfl corresponds to a weak syntactic fragment of sol which we show to be strictly contained in $Delta^1_2$. The separation is derived almost trivially from the fact that $Sigma^1_n$ defines its own truth-predicate. We finally show that slfl is equivalent to the logic of Henkin quantifiers, which shows, we argue, that Hodges´ notion of negation is adequate.