 The Barcan Formula is controversial. There is, however, a second line of argument that does not rest on the validity of the Barcan Formula, relying instead on combining standard truth definitions for quantified and modal sentences in the most straightforward way. Alien is true under an interpretation I just in case there is a world w accessible from the distinguished world of I with an object in its domain that is not in the domain of the distinguished world of I. This is because its truth requires that ∃x¬A∃y(y=x) is true with respect to w and so, it is tempting to conclude, that there is a witness that satisfies the condition ¬A∃y(y=x) at w. But that is the rub. If actualism is true, then there is no such witness, even if there could have been. If we are realistic about possible worlds semantics, the model theory for modal talk itself does not contain primitive modality, instead containing worlds as points of evaluation and the notion of truth at a world, in which case ‘there is’ in the above truth recursion does not occur inside the scope of a possibility operator. So, if Alien is true, there is some object o and accessible possible world w such that o satisfies ¬A∃y(y=x) at w, which seems to run contrary to the thesis of actualism, as that witness does not actually exist. (For further discussion of this problem and some of the solutions considered below, see the entry on the  possibilism-actualism debate.)