Proof by induction on First Order Formula

27 Views Asked by At

I am confused about how to prove that $(\mathcal{A}, i) \models \varphi \leftrightarrow (\mathcal{A}, i') \models \varphi$ given that two interpretations $i$ and $i'$ agree on all free variables in $\varphi$. Do I need to prove for each true form (below) of the language? And how I do this?

Let $\mathcal{A} \in STRUC[\tau]$ be a structure and $\tau$ a vocabulary. We can inductively define wether a formula $\varphi \in > \mathcal{L}(\tau)$ is true in $(\mathcal{A}, i)$:

  • $(\mathcal{A}, i) \models t_{1} = t_{2} \leftrightarrow i(t_{1}) = i(t_{2})$
  • $(\mathcal{A}, i) \models R_{j}(t_{1}, ..., t_{a_{j}}) \leftrightarrow \langle i(t_{1}),...,i(t_{a_{j}}) \rangle \in R_{j}^{\mathcal{A}}$
  • $(\mathcal{A}, i) \models \neg \varphi \leftrightarrow$ it is not the case that $(\mathcal{A}, i) \models \varphi$
  • $(\mathcal{A}, i) \models \varphi \wedge \psi \leftrightarrow (\mathcal{A}, i) \models \varphi$ and $(\mathcal{A}, i) \models \psi$
  • $(\mathcal{A}, i) \models (\exists x) \varphi \leftrightarrow$ $($there exists $a \in |\mathcal{A}|(\mathcal{A,i,a/x})) \models \varphi$, where $(i, a/x)(y) = \begin{Bmatrix} i(y) & \text{ if } y \neq x\\ a & \text{ if } y = x \end{Bmatrix}$