Is the formal semantics of first-order logic ambiguous? When defining the semantics of propositional and particularly first-order logic, it has always made me uneasy when reading, for example:
$$M \models A \lor B \quad\text{iff}\quad M \models A \text{ or } M \models B$$
Where does the “or” on the right hand side comes from? What's its definition?
I know this is supposed to be in the “meta” language and, somehow, we all mathematicians agree on what that “or” is supposed to mean. You could even be a bit more cautious, point me to a truth table and say: “That! Use that if are unsure of what we mean”. Fine.
But then it baffles me even more when I read something along the lines of
$$M \models \forall x A \quad\text{iff}\quad M_x \models A \text{ for all $x$-variants $M_x$ of $M$}$$
What is the meaning of this “for all”?? Most of our intuitions would probably agree on what to do if the domain of $M$ is finite, check all the possibilities one by one; but what if the domain is some weird infinite non-recursively enumerable monstrous set, how can we know whether $M_x \models A$ is true “for all” values of $x$?
A bit more to the point, how would you argue whether
$$\lnot\forall x A \rightarrow \exists x \lnot A$$
is valid or not? (from a purely semantical point of view)
It seems, at least to me, that the given definitions are not enough, as you also have to specify what sorts of arguments do mathematicians accept at the “meta” language (e.g. is proof by contradiction valid to show the existence of elements? or did you meant a constructive/intuitionistic proof?)
Update:
Ok, now I am firmly convinced that the answer to my original question (is the definition of FOL semantics ambiguous?) is: No. All sensible mathematicians should agree that the semantics are well defined.
Indeed, as Carl argues on his answer:

Given some structure M, and a property A that each element of M may or may not have, either every element of M has the property, or there is some element that does not have the property

That is, the definition does make the assumption that, with respect to the model, each property is either true or is false. No other options are allowed. Now a constructivist or even a paraconsistent mathematician may not agree on this assumption, and suggest that other options should be considered as well. And that's why they can get away with rejecting things like the law of the excluded middle; not because they think “or” should mean something different, but because they are making different assumptions about their logic systems.
Furthermore, even they would agree that if one assumes that a property can only be true or false, as FOL definition states, then for a model $M$ we have that either every element of the domain has the property, or some element of the domain does not have the property. End of story.
And this is why we can unambiguously state that $\lnot\forall x A \rightarrow \exists x \lnot A$ is valid with respect to this definition of the semantics.
Furthermore, this is true even if there might be some particular model $M$ and property $A$ for which we might never know whether $M \models \forall x A$ or not (because $M$ is “monstrous” or the property A is strange, and mathematicians are never able to figure it out).
 A: How would I argue semantically that $\lnot (\forall x) A \to (\exists x) \lnot A$?

Assume $M$ is a model of the theory at hand and assume that $M$ satisfies $\lnot (\forall x) A(x)$. Then, by the definition of the satisfaction predicate, it is not the case that $M$ satisfies $(\forall x) A(x)$. Thus, looking at the definition of the satisfaction predicate, there is some $z$ in $M$ such that $M$ does not satisfy $A(z)$. Hence $M$ satisfies $\lnot A(z)$, and thus $M$ satisfies $(\exists x)\lnot A(x)$. 

Most mathematics takes place in an informal natural-language metatheory, and mathematical logic is no exception. The above argument is not particularly different from the argument that every cyclic group is isomorphic to either $\mathbb{Z}$ or to $\mathbb{Z}_n$ for some $n$, which does not show that we can tell which case holds in an algorithmic way. 
Just like any other area of mathematics, we can use a formal metatheory such as ZFC to formalize these informal arguments. Both arguments I have mentioned here can be easily formalized in ZFC. But mathematics itself is typically carried out in an informal metatheory, with few mentions of any formal metatheory. 
The question was edited to replace "check" with "know", but that still misses the point of classical logic. Classical logic is designed for studying the properties of abstract structures that have truth values regardless whether we have any effective way to determine those truth values. Given some structure $M$, and a property $A$ that each element of $M$ may or may not have, either every element of $M$ has the property, or there is some element that does not have the property; that claim is not related to our ability to find the element, only to our abstract reasoning about what "all elements have the property" and "not all elements have the property" mean in English. We may never know whether all elements have the property $A$, but we can still argue abstractly that $\lnot (\forall x) A \to (\exists x) \lnot A$. 
The definition of the satisfaction predicate is not meant to tell us how to effectively verify truth values; it is just meant to capture the relationships between truth values of compound statements and truth values of simpler statements.  Intuitively, this is why the completeness theorem for first-order logic links provability with truth in all structures - we may never really know everything about a particular structure, but when we reason abstractly about the properties that an arbitrary structure must have we end up proving results that are true for all structures. 
