Models of first-order logic and cardinalities of the domain In first-order logic, it is possible for a sentence $S$ and its negation $\lnot S$ to both be invalid. That is, it is possible for there to not exist a proof of $S$, and also not of $\lnot S$.
For instance, consider the following sentence $S$, followed by its negation:


*

*$\exists x \exists y \lnot (x = y)$

*$\forall x \forall y (x = y)$


$S$ states that there exist two objects that are not equal, and $\lnot S$ states that all objects are equal. Neither of these sentences are valid, because first-order logic says nothing about the size of the universe. If the universe has only one object, the sentence is true, and if not, it is false.
My question: the problem is that $S$ can hold only in some models of first-order logic, and $\lnot S$ can also hold only in some models. If we restrict the cardinality of the set of objects in our logic, then do we end up in a situation where a sentence either holds (e.g. are "valid" for those models), or where its negation holds?
If not, how does this fail?
Note that this is different than asking whether we can prove every sentence or its negation within some theory, which we know is not true because there can be more than one model of a theory with the same cardinality. I am asking about proving the validity of a first-order sentence in general, or proving its negation, if the cardinality of the universe is somehow specified.
 A: No, restricting the size of the model doesn't change anything. Take e.g. the sentence $S\equiv$ "$\forall x(U(x))$" (where $U$ is a unary predicate symbol); for every cardinal $\kappa$, there will be structures of size $\kappa$ satisfying $S$ and structures of size $\kappa$ satisfying $\neg S$.
Meanwhile, if you are looking only at structures in the empty language, then the answer to your question is "yes," but for a trivial reason: any two structures in the empty language with the same cardinality are isomorphic.
EDIT: here's a quick exercise. Show that a pair $(L,\kappa)$ - where $L$ is a first-order language and $\kappa$ is a cardinal $>0$ - has the property $$\mbox{"Every $L$-sentenceis either true of every structure of size $\kappa$ or false of size $\kappa$"}$$ if and only if one of the following holds:


*

*$\kappa=1$ and $L$ contains no relation symbols. (As is standard, I'm viewing "$=$" as a logical symbol, not a relation symbol, here.)

*$L$ is empty.

*$L$ consists of a single constant symbol.

Also, contra your last paragraph: we can specify the cardinality of the model with a first-order sentence, in some cases. Namely, if we want to restrict attention to structures of cardinality $n$ where $n$ is finite, this can be done: for each finite $n$ there is a sentence $\varphi_n$ in the empty language which is true in exactly those structures of size $n$. "True in every structure of size $n$" (for $n$ finite) is exactly the same as "Provable from the theory $\{\varphi_n\}$." So I'm not really sure what you're getting at, in your last paragraph.
(For completeness: let $\psi_m$ be the sentence "$\exists x_1...\exists x_m(\bigwedge_{1\le i<j\le m}x_i\not=x_j)$." Then we set $\varphi_n=\psi_n\wedge\neg\psi_{n+1}$.)
