FOL(5) - soundness theorem

 

soundness theorem : $\Gamma \vdash \varphi \rightarrow \Gamma \models \varphi$.

 

basic idea for proving this is same as soundness theorem for PL. give induction for deduction sequence. then case is divided into 3. $\varphi \in \Gamma$, $\varphi \in \Lambda$, or $\varphi$ is obtained by modus ponens. first case is trivial, so is thrid(use satisfaction definition). remaining case is second. for this, we'll prove our axioms are $valid$.

 

 

(i) $\theta$ is valid iff $\forall x \theta$ is valid.

 

$(\rightarrow)$. this is trivial since for given $d \in |\mathfrak{A}|$, $s(x|d)$ is also variable assignment $s$.

$(\leftarrow)$. suppose not. then $\models_{\mathfrak{A}} \theta[x|d]$ for every $d \in |\mathfrak{A}|$. and $\not\models_{\mathfrak{A}} \theta$. then by definition of 'valid', there exist some $s$ and $\mathfrak{A}$ such that $\not\models_{\mathfrak{A}} \theta[s]$. since $s(x) \in \mathfrak{A}$, we can construct $s$ same as $s(x|s(x))$ each belongs to case in $s(x|d)$ where $d$ is any element in $\mathfrak{A}$. thus contradiction occurs.

 

using (i), we can assure any generalization of our axiom group 1-6 is valid if we can prove axiom groups. now we'll prove each axiom group is valid.

 

axiom group 1

 

we'll prove each tautolgy is valid. for this, define truth assignemnt $v$ for every prime formulas $S$ where $v(A) =T$ iff $\models_{\mathfrak{A}} A[s]$ where $A$ is any prime formula. then extend this to $\bar{v}$ where $\bar{v}(\varphi)=T$ iff $\models_{\mathfrak{A}} \varphi[s]$. you can verify this freely(using induction).

 

using this truth assignment, it suffices to show that if $\Gamma$ tautologically implies $\varphi$, then $\Gamma$ logically implies $\varphi$. for this, suppose $\Gamma$ tautologically implies $\varphi$ and $s$ and $\mathfrak{A}$ are arbitrary satisfying $\Gamma$. then now consider above truth assignment. then trivially, $\models_{\mathfrak{A}}\varphi[s]$. then, since every tautology is $\models \sigma$ tautologically, $\models \sigma$ logically. thus axiom group 1 is valid.

 

axiom group 3

 

we'll show $\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$ is valid. then it suffices to show that $\{\forall x(\alpha \rightarrow \beta), \forall x \alpha \} \models \forall x \beta$(for this, you've to prove $\Gamma;\varphi \models \psi$ iff $\Gamma \models \varphi \rightarrow \psi$).

 

now suppose $s$ and $\mathfrak{A}$ are arbitrary, satisfying $\forall x (\alpha \rightarrow \beta)$ $\forall x \alpha$. then $\models_{\mathfrak{A}} (\alpha \rightarrow \beta)[s(x|d)]$ for every $d \in |\mathfrak{A}|$ and $\models_{\mathfrak{A}} \alpha[s(x|e)]$ for every $e \in |\mathfrak{A}|$. now suppose $\not\models_\mathfrak{A} \forall x \beta[s]$. then there exist some $a \in |\mathfrak{A}|$ such that $\not\models_{\mathfrak{A}} \beta[s(x|a)]$. then since $a \in |\mathfrak{A}|$, we must get $\models_{\mathfrak{A}} (\alpha \rightarrow \beta)[s(x|a)]$ and $\models_{\mathfrak{A}} \alpha[s(x|a)]$. then trivially $\models_{\mathfrak{A}} \beta[s(x|a)]$ which is contradiction. hence, axiom group 3 is valid.

 

axiom group 4

 

it suffices to show that $\alpha \models \forall x \alpha$ where $x$ does not occur free in $\alpha$. now suppose any $s$ and $\mathfrak{A}$ satisfying $\alpha$. then $\models_{\mathfrak{A}} \alpha[s]$. then suppose $d \in |\mathfrak{A}|$ is arbitrary, and consider variable assignemnt $s(x|d)$ for $\alpha$. then since $x$ does not occur in $\alpha$, and $s$ and $s(x|d)$ agree at all free variables except $x$, we can get $\models_{\mathfrak{A}} \alpha[s]$ iff $\models_{\mathfrak{A}} \alpha[s(x|d)]$. thus we get $\models_{\mathfrak{A}} \forall x \alpha[s]$. hence axiom group 4 is valid(refer to Lemma for sentence satisfaction).

 

axiom group 5

 

we've to show $x=x$ is valid. this is trivial from $\models_{\mathfrak{A}} =t_1t_2$ iff $\bar{s}(t_1)=\bar{s}(t_2)$. since $s(x)=s(x)$, we get $\models_{\mathfrak{A}} =xx[s]$ for every $s$ and $\mathfrak{A}$. thus axiom group 5 is valid.

 

axiom group 6

 

we've to show $x=y \rightarrow (\alpha \rightarrow \alpha')$ is valid($\alpha$ is atomic formula). it suffices to show that $\{x=y, \alpha \} \models \alpha'$. assume that $\models_{\mathfrak{A}} (x=y)[s]$ and $\models_{\mathfrak{A}} \alpha[s]$. now we'll prove $s(t)=s(t')$ where $t'$ is obtained from $t$ replacing $x$ in term $t$ by $y$ zero or more times.

 

(i) $t$ is a constant symbol. then $s(t)=s(t')$ trivial since there does not exist $x$ that can be chngaed.

(ii) $t$ is a variable. if $t=x$, then $t'$ can be $x$ or $y$. if $t'=x$, $s(x)=s(x)$ trivially. if $t'=y$, since we assumed $\models_{\mathfrak{A}}x=y[s]$, we get $s(x)=s(y)$. thus $s(t)=s(t')$.

(iii) let $t_1, \ldots, t_n$ are terms where $\bar{s}(t_i)=\bar{s}(t_i')$ for all $i$. then $\bar{s}(ft_1\ldots t_n)=f(\bar(t_1), \ldots, \bar{s}(t_n)) = f(\bar{s}(t_1'), \ldots, \bar{s}(t_n')) = \bar{s}(ft_1' \ldots t_n')$. thus by inductive hypothesis, we get $\bar{s}(t)=\bar{s}(t')$ for all term $t$.

 

given this fact, we'll prove $\alpha = \alpha'$.

 

case 1 : $\alpha = (t_1=t_2)$ where $t$ is a term. then

$\models_{\mathfrak{A}} \alpha[s]$ iff $\models_{\mathfrak{A}} =t_1t_2[s]$ iff $\bar{s}(t_1)=\bar{s}(t_2)$ iff $\bar{s}(t_1')=\bar{s}(t_2')$ iff  $\models_{\mathfrak{A}} =t_1't_2'[s]$ iff $\models_{\mathfrak{A}} \alpha'[s]$.

 

case 2 : $\alpha = Pt_1 \ldots t_n$. then

$\models_{\mathfrak{A}} \alpha[s]$ iff $\models_{\mathfrak{A}} Pt_1 \ldots t_n[s]$ iff $<\bar{s}(t_1), \ldots, \bar{s}(t_n)> \in P^{\mathfrak{A}}$ iff $<\bar{s}(t_1'), \ldots, \bar{s}(t_n')> \in P^{\mathfrak{A}}$ iff $\models_{\mathfrak{A}} Pt_1' \ldots t_n'[s]$ iff $\models_{\mathfrak{A}} \alpha'[s]$.

 

this proves axiom group 6 is valid.

 

axiom group 2

 

now we'll prove axiom group 2 is valid. but this requires 2 lemmas. before proving lemmas, i'll give intuitive idea why we need some lemmas that look complicated.

 

we've to prove $\models \forall x \alpha \rightarrow \alpha_{t}^{x}$ where $t$ is substitutable for $x$ in $\alpha$. it suffices to show that $\{\forall x \alpha\} \models \alpha_{t}^{x}$ where $t$ is substitutable for $x$ in $\alpha$.

 

suppose $s$ and $\mathfrak{A}$ are arbitary such that $\models_{\mathfrak{A}} \forall x \alpha[s]$. then $\models_{\mathfrak{A}} \alpha[s(x|d)]$ for every $d \in |\mathfrak{A}|$. for proving $\models_{\mathfrak{A}} \alpha_{t}^{x}[s]$, it suffices to show that $\models_{\mathfrak{A}} \alpha_{t}^{x}[s]$ iff $\models_{\mathfrak{A}} \alpha[s(x|\bar{s}(t))]$. then since $\bar{s}(t) \in |\mathfrak{A}|$, later on proof is clear.

 

and proving $\models_{\mathfrak{A}} \alpha_{t}^{x}[s]$ iff $\models_{\mathfrak{A}} \alpha[s(x|\bar{s}(t))]$, we must confirm each term changed by operation $\alpha_{t}^{x}$ is same in $\alpha[s(x|\bar{s}(t))]$. for this, give a definition $u_{t}^{x}$.

 

$u_{t}^{x}$ is a term obtained by changing variable $x$ to $t$ in a term $u$. recursively,

(i) $u$ is a constant symbol. then $u_{t}^{x}=u$

(ii) if $u$ is a variable, then $u_{t}^{x}= t$ if $u=x$, and $u_{t}^{x}=u$ if $u \neq x$

(iii) $u_1, \ldots, u_n$ are terms. then $(f u_1 \ldots u_n)_{t}^{x}= f {u_1}_{t}^{x} \ldots {u_n}_{t}^{x}$.

 

now we claim that $\bar{s}(u_{t}^{x})=\overline{s(x|\bar{s}(t))}(u)$.

 

 

Lemma 1 : $\bar{s}(u_{t}^{x})=\overline{s(x|\bar{s}(t))}(u)$

 

proof : use induction on terms(i-iii case). this is easy.

 

 

Lemma 2(substitution lemma) : if $t$ is substitutable for $x$ in $\varphi$, then $\models_{\mathfrak{A}} \varphi_{t}^{x}[s]$ iff $\models_{\mathfrak{A}} \varphi[s(x|\bar{s}(t))]$.

 

proof : use induction on formulas.

 

(i) $\varphi$ is atomic formula. suppose $t$ is substitutable for $x$ in $\varphi$.

(a) $\varphi$ is $=t_1t_2$. then

$\models_{\mathfrak{A}} \varphi_{t}^{x}[s]$ iff $\models_{\mathfrak{A}} (=t_1t_2)_{t}^{x}[s]$ iff $\models_{\mathfrak{A}} ({t_1}_{t}^{x}={t_2}_{t}^{x})[s]$ iff $\bar{s}({t_1}_{t}^{x})=\bar{s}({t_2}_{t}^{x})$ iff $\overline{s(x|\bar{s}(t))}(t_1)=\overline{s(x|\bar{s}(t))}(t_2)$(by Lemma 1) iff $\models_{\mathfrak{A}} (t_1=t_2)[\overline{s(x|\bar{s(t)})}]$.

 

(b)$\varphi$ is $Pt_1 \ldots t_n$. you can do this similarly as (a).

 

(ii) $\varphi = (\neg \phi)$. trivial.

(iii) $\varphi = (\phi \rightarrow \psi)$. also trivial.

(iv) $\varphi = \forall y\phi$. we have 'if $t$ is substitutable for $x$ in $\phi$, then $\models_{\mathfrak{A}} \phi_{t}^{x}[s]$ iff $\models_{\mathfrak{A}} \phi[s(x|\bar{s}(t))]$' by inductive hypothesis. now let $t$ is substitutable for $\varphi$.

 

case 1 : $x$ does not occur free in $\varphi$. then $s$ and $s(x|\bar{s}(t))$ agree at all free variables in $\varphi$. thus by lemma for sentence satisfaction, $\models_{\mathfrak{A}} \varphi_{t}^{x}[s]$ iff $\models_{\mathfrak{A}} \varphi[s(x|\bar{s}(t))]$.

 

case 2 : $x$ does occur free in $\varphi$. since $t$ is substitutable for $x$ in $\varphi$, we get $y$ does not occur in $t$ and $t$ is substitutable for $x$ in $\phi$(c.f. definition of 'substitutable'). for we have $t$ is substitutable for $x$ in $\phi$, we get $\models_{\mathfrak{A}} \phi_{t}^{x}[s]$ iff $\models_{\mathfrak{A}} \phi[s(x|\bar{s}(t))]$. and $x \neq y$; otherwise, $x$ does not occur free in $\varphi$. thus $\varphi_{t}^{x}=\forall y \phi_{t}^{x}$. then,

 

$\models_{\mathfrak{A}} \varphi_{t}^{x}[s]$ iff $\models_{\mathfrak{A}} \phi_{t}^{x}[s(y|d)]$ for every $d \in |\mathfrak{A}|$ iff $\models_{\mathfrak{A}} \phi[s(y|d)(x|\bar{s}(t))]$ for every $d |\in \mathfrak{A}|$(inductive hypothesis) iff $\models_{\mathfrak{A}} \varphi[s(x|\bar{s}(t))]$.

 

thus soundness is proved.