Suppose I have the FOL-Formula $F := \forall x \exists y. R(x, y)$ in negation normal form. Now I want to show that $F$ is satisfiable using the tableaux calculus (TC1).
By application of rules I get the completed and clash-free tableaux:
$$\forall x \exists y. R(x, y)$$ $$|$$ $$\exists y. R(t, y)$$ $$|$$ $$R(t, a)$$
Clearly, $F$ is satisfiable. But how would I go about constructing am model from the tableaux?
I see two approaches:
The domain is $D=\{a, t\}$ and the extension of $R$ is $I(R) = \{(t, a)\}$. But this is clearly not a model of $F$.
The domain is $D=\{a\}$, the extension of $R$ is $I(R) = \{(t, a)\}$ and $t$ is treated as 0-ary function symbol with $I(t) = a$.
I am not confident with any of those approaches and be very happy about some help :)
Note that when you 'instantiated' the universal, you used a $t$, but when instantiating the existential, you used $a$. This is an important difference: the $a$ is an individual constant: it refers to a specific object. The $t$, however, works more like a variable. Indeed, if $t$ were a constant, then just because we can satisfy $\exists y . R(t,y)$ does not mean that we have satisfied $\forall x \ \exists y . R(x,y)$
So, I assume that there is some rule in the system you are using ('TC1') that says that you should always make sure to instantiate the $t$ with any constant that occurs in the same branch that it occurs in.
The upshot is that you should not treat $t$ as a specific object of your domain. That is, it makes little sense to use a domain of $\{ a,t\}$. Thus, your option $1$ is out. Likewise, your option $2$ does not work, since if you say that $I(R)= \{ (t,a) \}$, you are still treating $t$ as a specific object.
What does work, however, is to say that your domain is $\{a\}$, and that $I(R)=\{ (a,a) \}$.