When expanding a tableau, from a previous answer in this site I learned that I have to expand the outer first. Does the same rule work when interpretating a First Order sentence:
$\forall x \exists y\ x < y$, with domain $\mathbb{Z}$
I try to expand the outside one and I get $\exists y\ 1<y$ and $\exists y\ 2<y$ and $\exists y\ 3<y$ and so on. So given that I can find for all of them one y, therefore this is a valid statement. Is this method of elaborating first order sentences correct?
Yes and no, depending on whether you're evaluating the sentence in a particular model or not, i.e. if you're talking about truth in a particular model (denoted $M \models \varphi$ for model $M$ and sentence $\varphi$) or provability in a theory (denoted $T \vdash \varphi$ for a theory $T$ and a formula $\varphi$).
If you view $(\mathbb{Z},0,1,+,-,<)$ as a model of the first-order language $\mathcal{L} = \{\mathbf{0},\mathbf{1},\oplus,\ominus,\lessdot\}$ ($\ominus$ is supposed to be unary minus here, not subtraction), then of course $$ \mathbb{Z} \models \forall x\, \varphi(x) \text{ exactly if } \mathbb{Z} \models \varphi(\underline{n}) \text{ for all $n \in \mathbb{Z}$} $$ (where $\underline{n}$ means $\mathbf{0}$ if $n=0$, $\underbrace{\mathbf{1}\oplus\ldots\oplus\mathbf{1}}_{\text{$n$ times}}$ if $n > 0$, and $\ominus(\underbrace{\mathbf{1}\oplus\ldots\oplus\mathbf{1}}_{\text{$-n$ times}})$ if $n < 0$).
But if $T$ is some theory over $\mathcal{L}$, then it may be that $$ T \vdash \varphi(\underline{n}) \text{ for all } n \in \mathbb{Z} \quad\text{but}\quad T \not\vdash \forall x\, \varphi(x) \text{.} $$ An (a bit contrived) example where that happens is $$\begin{eqnarray} T &:=& \left\{\underline{n} \lessdot \underline{n+1} \,:\, n \in \mathbb{Z}\right\} \cup \left\{\forall x\, \left(x \oplus (\ominus x)\right) = \mathbf{0}, \,\forall x\,\forall y\, x\oplus y=y\oplus x\right\}, \\ \varphi &:=& \forall x\, (x \lessdot x \oplus 1) \text{.} \end{eqnarray}$$ Here, $T$ contains all the statements $\underline{1} \lessdot \underline{2}$, $\underline{2} \lessdot \underline{3}$, $\underline{-1} \lessdot \underline{0}$, $\underline{-2} \lessdot \underline{-1}$ and so on, but since it doesn't provide any form of induction, you won't be able to prove $\forall x\, (x \lessdot x\oplus 1)$.
However, first-order logic does have the property that if $$ T \vdash \varphi(x) $$ and if $x$ isn't a free variable in any of the axioms in $T$, then $$ T \vdash \forall x\, \varphi(x) \text{.} $$ But, as you can see from the example above, $T$ needs to really prove $\varphi(x)$, not just a bunch of special cases $\varphi(\underline{n})$ that you happen to imagine make up all the cases. (Imagine is the keyword here - the problem is exactly that there might (and will!) be models where the cases don't cover all the possibilities).