So my teacher for formal methods of logicgave this definition for variant sequences and I just cannot follow what this is asking me. When he explained the concept it made since but then he gave us an example on the board that said
Consider the language $$L = \{R\}$$ with a single relational predicate $R$ and model $$M = \langle D, I \rangle$$ for $L$ with domain $$D = \{a, a', b, b'\}$$ such that $$I(R) = \{\langle a, a \rangle, \langle a, a' \rangle, \langle a', a' \rangle, \langle b, b \rangle, \langle b, b' \rangle, \langle b', b' \rangle\}$$. Let $s: Var → D$ be such that $$s(x) = a\text{ for all }x ∈ Var.$$ $[\![Rv_0v_1]\!]^{s_{[v_1\mapsto d]}}$
and I just couldn't figure it out. Is x now v1 in the example? and where does v0 go to??? Sorry for the terrible notation I tried to use MathJax but was struggling to get it to work the way I wanted it to. definition
$x$ is a placeholder for any variable. $x$ stands for $v_1$ and also $v_0$.
Where $s_{[v_1 \mapsto d]}$ sends it to. In the given model, $s$ sends all variables to $a$, so $s(v_0) = a$. And applying the definition of a variant sequence, $s_{[v_0 \mapsto d]} =$ the same as $s(v_0)$ if $v_0$ is a different variable than $v_1$, and $s_{[v_0 \mapsto d]} = d$ if $v_0$ is the variable in question $v_1$. So which is it?
(BTW, you must have a typo in your post, as there is no $d$ in $D$.)