  Hintikka and Sandu originally proposed Independence Friendly Logic (IF) as a
first-order logic of imperfect information to describe game-theoretic phenomena
underlying the semantics of natural language. The logic allows for expressing
independence constraints among quantified variables, in a similar vein to
Henkin quantifiers, and has a nice game-theoretic semantics in terms of
imperfect information games. However, the IF semantics exhibits some
limitations. It treats the players asymmetrically, considering only one of the
two players as having imperfect information when evaluating truth, resp.,
falsity, of a sentence. In addition, the truth and falsity of sentences
coincide with the existence of a uniform winning strategy for one of the two
players in the semantic imperfect information game. As a consequence, IF does
admit undetermined sentences, which are neither true nor false, thus failing
the law of excluded middle. In this paper, we investigate an extension of IF,
called Alternating Dependence/Independence Friendly Logic (ADIF), tailored to
overcome these limitations. To this end, we introduce a novel compositional
semantics, generalising the one based on trumps proposed by Hodges for IF. The
new semantics (i) allows for meaningfully restricting both players at the same
time, (ii) enjoys the property of game-theoretic determinacy, (iii) recovers
the law of excluded middle for sentences, and (iv) grants ADIF the full
descriptive power of Second Order Logic. We also provide an equivalent
Herbrand-Skolem semantics and a game-theoretic semantics for the prenex
fragment of ADIF, the latter being defined in terms of a determined
infinite-duration game that precisely captures the other two semantics on
finite structures.
