Proving that the value for two variable assignments are equal

Question

I need to show that $Val^M_s(t) = Val^M_{s'}(t)$ where t is free for x in $∃yφ$ and s and s' are y variants of eachother (so if s is a variable assignment then s' is a y-variant of s if s' differs by at most y). The only thing I know is that if s and s' agree on all variables in t then $Val^M_s(t) = Val^M_{s'}(t)$ so I figured that I need to use the fact that s and s' are y variants of eachother to show this but I'm not sure where to go from there.

Answer 1

The question seems to be extrapolated from a more general problem: thus, I'll discard the reference to the quantified formula and I'll consider only the question in the title :

prove that two variable assignment functions $s$ and $s'$ such that $s(v) = s'(v)$ for every variable $v$ in the term $t$, then $\text {Val}_s^M(t) = \text {Val}_{s'}^M(t)$.

We need induction on the complexity of the term $t$. If $t$ is either a variable or a constant symbol, the result is immediate.

If $t = f(t_1,t_2, \ldots, t_n)$, then due to the fact that $s(t_i) = s'(t_i)$ for $1 \le i \le n$ by the inductive hypothesis, the definition of $s(t)$ and that of $s'(t)$ are identical.

Thus, $f^M(s(t_1),\ldots, s(t_n))=f^M(s'(t_1),\ldots, s'(t_n))$ and so the two functions assign the same value to the term $t$, i.e.$\text {Val}_s^M(t) = \text {Val}_{s'}^M(t)$

---

Following your previous post, I imagine that - having proved the base case - you are trying with the induction step (clause for $\exists$) of:

to prove that $M,s \vDash \varphi [t/x]$ iff $M,s' \vDash \varphi$.

If so, we have:

• $M,s \vDash \exists y \ \varphi [t/x]$ iff for some $y$-variant $s'$ of $s$ we have: $M,s' \vDash \varphi(y)[t/x]$.

By condition of $t$ "being free for" $x$ in the formula, we know that $y$ is not free in $t$.

Thus, every $s''$ that agrees with $s'$ except for $y$ is such that $\text {Val}_{s'}^M(t) = \text {Val}_{s''}^M(t)$ and so, applying the induction hypotheses, we have:

• $M,s' \vDash \varphi(y)[t/x]$ iff $M,s'' \vDash \varphi(y)$.

Then:

• $M,s'' \vDash \varphi(y)$, for some $y$-variant $s''$ of $s'$, iff $M,s' \vDash \exists y \ \varphi$.