A fundamental thesis in quantified modal logic, first isolated by the 20th-century American philosopher Ruth Barcan Marcus. It was originally the schema that ◊(∃x)Ax strictly implies (∃x)◊Ax (informally: if possibly something is A, then something is possibly A). Adding this to a standard modal logic is equivalent to adding ◊(∃x)Ax → (∃x)◊Ax or (∀x)□ Fx → □(∀x)Fx, and either of these may be called the Barcan formula. Informally the latter means that if everything is necessarily F, then necessarily everything is F. The formula has been criticized on the grounds that when we consider possible worlds with different objects in them, then although the antecedent might be true of the actual world, the consequent may be false. For instance, it may be possible that there should be things of a different species from any actual living organism, but not possible of any living organism that it should be of a different species.