FOL(8) - completeness theorem

 

 there are many versions of proving completeness theorem for FOL which is proved by godel first in his thesis. but we'll not see the version by godel, but by henkin which is universally introduced in any logic book(but our proof is modified some). basically, we'll prove

 

(i) any consistent $\Gamma$ in countable language can be extended to maximal consistent set $\Delta$ in given launage;

(ii) $\Delta$ is satisfiable.

 

now go through proof for completeness theorem for FOL in countable language.

 

(I) Let any set $\Gamma$ of formulas is consistent in countable language $\mathcal{L}$. define $\mathcal{L'}=\mathcal{L}\cup\{c_i | i < \omega\}$ where $c_i$ is new constant symbol does not occur in $\mathcal{L}$. then $\Gamma$ is consistent in $\mathcal{L'}$.

 

proof : suppose not. then $\Gamma \vdash \alpha \wedge \neg\alpha$ in $\mathcal{L'}$. then we get $\Gamma\vdash\alpha_{y}^{c} \wedge\neg\alpha_{y}^{c}$ by generalization on constants. since every formula is finite, we can eliminate every new constant $c$ introduced in $\mathcal{L'}$(and $c$ is replaced by a variable). thus we get $\Gamma\vdash\alpha_{y}^{c} \wedge\neg\alpha_{y}^{c}$ in $\mathcal{L}$(since every new $c$ is eliminated, this deduction in $\mathcal{L'}$ equals $\mathcal{L}$). this yields contradiction.

 

now add the formula for every formula $\varphi$ in $\mathcal{L'}$, $\exists x \varphi \rightarrow \varphi_{c}^{x}$ to $\Gamma$(this formula will do some useful operations later).

 

define $\Theta_{n+1}=\Theta_n;\theta_{n+1}$ where $\theta_n = (\exists x_n \varphi_n \rightarrow \varphi_{c_n}^{x_n})$ and in $\Theta_{n+1}$, $c_{n+1}$ is the first new constant symbol in $\mathcal{L'}$such that does not occur in $\Theta_{n}$ and $\varphi_{n+1}$(fixed enumeration is always possible since we're dealing with countable language). define $\Theta = \cup_{n \in \mathbb{N}} \Theta_n$. then $\Gamma \cup \Theta$ is consistent.

 

proof : suppose not. then $\Gamma \cup\Theta\vdash\varphi\wedge\neg\varphi$. then we get $\Gamma\cup\Theta_{m+1}\vdash\varphi\wedge\neg\varphi$. thus $\Gamma \cup \Theta_{m+1}$ is inconsistent(and we can take the smallest $m \geq 0$). then by RAA, $\Gamma\cup\Theta_m \vdash\theta_{m+1}$. then by rule T, we get $\Gamma\cup\Theta_m \vdash \exists x \varphi_{n+1}$ and $\Gamma\cup\Theta_m \vdash \neg\varphi_{c_{n+1}}^{x_{n+1}}$. then by generalization on constants(actually its collorary), we get $\Gamma\cup\Theta_m \vdash \neg\exists x \varphi_{n+1}$. thus $\Gamma\cup\Theta_m$ is inconsistent which is contradiction to leastness of $m$.

 

 

now construct maximal consistent set $\Delta$ for $\mathcal{L'}$. suppose we are given enumeration of every formula $\varphi$(this is possible since our language is countable) in $\mathcal{L'}$. define $$\Delta_{n+1} = \Delta_n;\varphi_{n+1} \quad\text{if consistent},\quad\text{or}\quad\Delta_n ;\neg\varphi_{n+1}\text{otherwise} $$ where $\Delta_0=\Gamma\cup\Theta$. define $\Delta= \cup_{n\in\mathbb{N}}\Delta_n$. then $\Delta_i$ for any $i\in\mathbb{N}$ and $\Delta$ is consistent.

 

proof for $\Delta_i$ : let $\Delta_i$ is consistent and $\Delta_i ;\varphi_{i+1}, \Delta_i ;\neg\varphi_{i+1}$ are inconsistent. thus we get $\Delta_i\vdash\varphi_{i+1}$ and $\Delta_i\vdash\neg\varphi_{i+1}$. this yields contradiction. and since $\Delta_0=\Gamma\cup\Theta$ is consistent, $\Delta_i$ for any $i\in\mathbb{N}$ is consistent.

 

proof for $\Delta$ : suppose not. then we get $\Delta' \subseteq \Delta$ finite and inconsistent. since $\Delta'$ is finite, we can enumerate every member of $\Delta'$ and find $\varphi'$ which is last member of some $\Delta_k$. then trivially $\Delta' \subseteq\Delta_k$. thus we get $\Delta_k$ is inconsistent which is contradiction.

 

clearly only one of these holds; $\varphi \in\Delta$ or $\neg\varphi\in\Delta$(if not it is inconsistent).

 

now claim that $\varphi \Delta \Longleftrightarrow \Delta\vdash\varphi$. right-side condition is trivial.

for the left side,

$\Delta\vdash\varphi \Rightarrow \Delta\not\vdash\neg\varphi$(consistency)

$\Rightarrow \neg\varphi \notin\Delta$

$\Rightarrow \varphi\in\Delta$.

 

now we'll make some variable assignment and structure which satisfies $\Delta$(actually, we'll construct two structures; one for preliminary for the other structure). define $\mathfrak{A}$ for $\mathcal{L'}$,

 

(i) $|\mathfrak{A}|$ is the set of all terms in $\mathcal{L'}$

(ii) $<t_1,t_2>\in E^{\mathfrak{A}}$ iff $t_1=t_2 \in \Delta$

(iii)$<t_1,\ldots,t_n>\in P^{\mathfrak{A}}$ iff $Pt_1\ldots t_n \in \Delta$

(iv) $f^{\mathfrak{A}}(t_1,\ldots,t_n)=ft_1\ldots t_n$

(v) $c=c^{\mathfrak{A}}$ and $s(x)=x$(thus trivially $\bar{s}(t)=t$)

 

 

$\mathfrak{A}$ is preliminary structure for $\mathfrak{B}$ which'll satisfy $\Delta$. intuitive idea for this is similar to compactness theorem for PL(review the idea at compactness theorem for PL. see the idea for satisfaction of $\Delta$). but different thing is about $E$. since we cannot notice equality symbol('=') in that idea, we've to introduce binary predicate $E$ like above. and notation for $E$ is, $tEt' \Longleftrightarrow <\bar{s}(t'),\bar{x}(t')>\in E^{\mathfrak{C}}$ where $\mathfrak{C}$ is some given structure).

 

unfortunately, we observe that in this structure, '=' is not satisfied. considering our semantical definition of $\models_{\mathfrak{A}}t_1=t_2[s]$ iff $\bar{s}(t_1)=\bar{s}(t_2)$, we cannot express $E$ like this. that is, if $(t=u)\in\Gamma\subseteq\Delta$, then $<t,u>\in E^{\mathfrak{A}}$. and we don't have clue to transform this to $\bar{s}(t)=\bar{s}(u)$.

 

thus we've to make some structure such that $tEt'$ iff $\bar{s}(t)=\bar{s}(t')$. for this, we'll use the property of $E$ being made by equality symbol the equivalent relation(idea is to make $tEt'$ iff $[t]=[t']$, which is some basic set theoretic knowledge. you can prove this easily using equality theorem;see syntax(2). I'll leave this.).

 

now define equivalence class on $\mathfrak{A}$ $[t]=\{t'|tEt'\}$(observe that $[t]=[t'] \Longleftrightarrow tEt'$(this is set-theoretic concept). now define structure $\mathfrak{B}$ which will satisfy $\Delta$. define $\mathfrak{B}$ as below.

 

(i) $|\mathfrak{B}|$= the set of all equivalence classes of $\mathfrak{A}$ on $E$.

(ii)$<[t_1],\ldots,[t_n]>\in P^{\mathfrak{B}}$ iff $<t_1,\ldots,t_n>\in P^{\mathfrak{A}}$

(iii) $f^{\mathfrak{B}}([t_1],\ldots,[t_n])= [f^{\mathfrak{A}}(t_1,\ldots,t_n)]$

(iv) $c^{\mathfrak{B}}=[c^{\mathfrak{A}}]$ and $s(x)=[x]$(thus $\bar{s}(t)=[t]$)

 

now check expected property is met.

$\alpha\in\Delta$ iff $<t,t'>\in E^{\mathfrak{A}}$ iff $[t]=[t']$ iff $<\bar{s}(t),\bar{s}(t')>\in E^{\mathfrak{B}}$ iff $\models_{\mathfrak{B}}t=t'[s]$ where $\alpha$ is the form of $t=t'$. thus remainer is clear.

 

now we'll prove $\varphi\in\Delta \Longleftrightarrow \models_{\mathfrak{B}}\varphi[s]$ by induction on the number of $\neg$, $\rightarrow$,$\forall$ in $\varphi$.

 

(i) $\varphi$ is atomic formula.

(a) $\varphi$ is $t=t'$. proved by above fact.

(b) $\varphi$ is $Pt_1\ldots t_n$. then,

$Pt_1\ldots t_n\in\Delta$ iff $<t_1,\ldots,t_n>\in P^{\mathfrak{A}}$ iff $<[t_1],\ldots,[t_n]>\in P^{\mathfrak{B}}$ iff $\models_{\mathfrak{B}} Pt_1\ldots t_n[s]$

 

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

$\phi\in\Delta$ iff $\models_{\mathfrak{B}}\phi[s]$ and this is equivalent to

$\phi\notin\Delta$ iff $\not\models_{\mathfrak{B}}\phi[s]$ thus by definition of satisfaction and $\Delta$ property,

$\neg\phi\in\Delta$ iff $\models_{\mathfrak{B}}\neg\phi[s]$ thus

$\varphi\in\Delta \Longleftrightarrow \models_{\mathfrak{B}}\varphi[s]$

 

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

$\phi\rightarrow\psi\in\Delta$ iff $\Delta\vdash\phi\rightarrow\psi$ iff $\neg\phi\in\Delta \vee \psi\in\Delta$(if not trivial, you can prove this by constructing contradiction) iff $\models_{\mathfrak{B}}\neg\phi[s] \vee \models_{\mathfrak{B}}\psi[s]$ iff $\models_{\mathfrak{B}}(\phi\rightarrow\psi)[s]$. thus

$\varphi\in\Delta \Longleftrightarrow \models_{\mathfrak{B}}\varphi[s]$

 

(iv)$\varphi=\forall x \phi$.

 

(a) right-side part. use contraposition.

$\not\models_{\mathfrak{B}}\forall x\phi[s] \Rightarrow \not\models_{\mathfrak{B}}\phi[s(x|[t])]$ for some $[t]\in |\mathfrak{B}|$

$\Rightarrow\not\models_{\mathfrak{B}}\psi[s(x|[t])]$ by alphabetic variants&soundness theorem

$\Rightarrow\not\models_{\mathfrak{B}}\psi_{t}^{x}[s]$ by substitution lemma

$\Rightarrow\psi_{t}^{x}\notin\Delta$ by inductive hypothesis

$\Rightarrow\forall x \psi\notin\Delta$(axiom group2)

$\Rightarrow \forall x \phi\notin\Delta$ alphabetic variants&soundness

 

(b)left-side part.

$\models_{\mathfrak{B}}\forall x\phi[s] \Rightarrow \models_{\mathfrak{B}}\phi[s(x|[c])]$ for some $[c]\in |\mathfrak{B}|$

$\Rightarrow \models_{\mathfrak{B}}\phi_{c}^{x}[s]$ by substitution lemma

$\Rightarrow \phi_{c}^{x}\in\Delta$ by inductive hypothesis

$\Rightarrow \forall x\phi\in\Delta$ by $(\exists x\neg\phi \rightarrow \neg\phi_{c}^{x})\in\Delta$

 

last part is the form of $\exists x\psi \rightarrow \psi_{c}^{x}$ we introduced where $\psi$ is any $\psi$ in $\mathcal{L'}$

 

thus $\varphi\in\Delta \Longleftrightarrow \models_{\mathfrak{B}}\varphi[s]$. then since $\Gamma\subseteq\Delta$, we have every member of $\Gamma$ which is satisfiable in $\mathcal{L'}$. then restrict $\mathfrak{B}$ to $\mathcal{L}$. $\Gamma$ is satisfiable in $\mathcal{L}$ also.

 

 

※ $\varphi\in\Delta \Longleftrightarrow \models_{\mathfrak{B}}\varphi[s]$에 대한 induction에 주의하시길 바랍니다. $\neg$, $\rightarrow$, $\forall$의 개수에 대해서 induction이 사용됩니다. 말하자면, 총 n개의 $\neg$, $\rightarrow$, $\forall$를 지닌 임의의 $\varphi$에 대해서 inductive hypothesis를 사용하고 (n+1)에 대해서 위의 성질이 성립함을 증명하는 것임을 유의하시길 바랍니다.

 

 

※증명은 이걸로 끝이긴 하지만, 아무리 생각해도 쉽게 설명하기가 어렵네요.. 아무래도 집합론을 어느 정도 전제하지 않고는 설명하기가.. 여튼 completeness까지 끝났으니 앞으론 조금 쉬었다가 돌아오겠습니다.