It is a well-known (and frankly magical) property that first-order logic is strongly semantically complete (Gödels completeness theorem).
Independence-friendly logic is just like first-order logic but it allows quantifiers to only depend on some of the variables outside its scope.
For example: $\forall w \forall x \exists y_{\setminus{w}} \exists z_{ \setminus x} P(w,x,y,z)$ would state that y only depends on w and z only depends on x. This is not expressible in first-order logic.
My question is: Is there an equivalent of the completeness theorem for independence-friendly logic?
In a precise sense the answer is no.
In terms of expressive power, IF-logic is equivalent to existential second-order logic ESO. Now while ESO is reasonably tame in several ways (e.g. compactness and Lowenheim-Skolem), as far as complexity goes it's quite wild: for example, we can reduce the problem of telling whether a first-order sentence is true in $\mathbb{N}$ to the problem of telling whether a related universal second-order sentence is valid. Using a proof procedure for IF-logic, we could enumerate the ESO validities and so co-enumerate the USO validities, and this means that any such proof procedure must be "within one Turing jump" of computing true first-order arithmetic. In particular, this means there is no computable proof procedure for ESO (or equivalently IF).
See also Feferman, *What kind of logic is "independence-friendly logic"?.