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.