Finite information logic

We introduce a generalization of Independence Friendly (IF) logic in which Eloise (the ∃ player) is restricted to a finite amount of information about Abelard’s ( ∀ ’s) moves. This logic is shown to be equivalent to a sublogic ∃ ∀ of first-order logic, to have the finite model property, and to be decidable. Moreover, it gives an exponential compression relative to ∃ ∀ logic.