On existential declarations of independence in IF logic

We analyze the behaviour of declarations of independence between existential quantifiers in quantifier prefixes of Independence-Friendly (IF) sentences; we give a syntactical criterion to decide whether a sentence beginning with such prefix exists, such that its truth values may be affected by removal of the declaration of independence. We extend the result also to equilibrium semantics values for undetermined IF sentences. The main theorem defines a schema of sound and recursive inference rules; we show more explicitly what happens for some simple special classes of sentences. In the last section, we extend the main result beyond the scope of prenex sentences, in order to give a proof of the fact that the fragment of IF sentences with knowledge memory has only first-order expressive power.