Induction on formulas for substitution

166 Views Asked by At

Let's say that $φ$ is a formula, $M$ is a structure, $t'$ is a term, $s$ is a variable assignment, and $s'$ is an $x$-variant of $s$ such that $s′(x)=Val^M_s(t')$.

I need to use induction on formulas to prove that $M,s⊨φ[t'/x]$ iff $M,s′⊨φ$ where $φ[t'/x]$ is a substitution where I substitute all instances of $x$ with $t'$.

For my base case, my idea is to use $p(t)$ and then I'll say $M,s ⊨ p(t)[t'/x]$ iff $M,s ⊨ p(t[t'/x])$ but from there I don't know where to go. I need to arrive at $M,s' ⊨ p(t)$ so how do I do that?

1

There are 1 best solutions below

0
On BEST ANSWER

The proof is trivial but boring.

Base case: $\phi$ atomic, i.e. either $u_1=u_2$ or $P(u_1,\ldots, u_n)$, where $u_i$ are terms.

First subcase: we have that $M,s \vDash \phi[t'/x]$ (i.e. $M,s \vDash (u_1=u_2)[t'/x]$) holds iff $M,s \vDash (u_1[t'/x]=u_2[t'/x])$.

By the definition of the satisfaction relation, the above holds iff: $\text {Val}_s^M(u_1[t'/x])=\text {Val}_s^M(u_2[t'/x]).$

Now, if $s'$ is a variable assignment function which is an $x$-variant of $s$ with the "fixed" value $\text {Val}_s^M(t')$ for $x$, it behaves exactly like $s$, i.e. $\text {Val}_{s'}^M(u_1[t'/x])=\text {Val}_{s}^M(u_1[t'/x])$ and $\text {Val}_{s'}^M(u_2[t'/x])=\text {Val}_{s}^M(u_2[t'/x])$.

But then: $\text {Val}_{s'}^M(u_1[t'/x])=\text {Val}_{s'}^M(u_2[t'/x])$, i.e. $M,s' \vDash (u_1=u_2)$ (that is: $M,s' \vDash \phi$).

The subcase for $P(u_1,\ldots, u_n)$ is similar: $M,s \vDash P[t'/x]$ iff $(\text {Val}_s^M(u_1[t'/x]),\ldots, \text {Val}_s^M(u_n[t'/x])) \in P^M$, where $P^M$ is the interpretation of the predicate symbol $P$.

Again, every assignment $s'$ which is an $x$-variant of $s$ with the "fixed" value $\text {Val}_s^M(t')$ will satisfy $P$, because $s'$ assign to $x$ the "correct" value $\text {Val}_s^M(t')$, and thus: $M,s' \vDash P$.