어느 히키코모리의 블로그

lowenheim-skolem theorem is fundamental theorem to model theory with completeness and compactness theorem. we'll see this theorem for countable lanuage and expand to any infinite cardinal.

I assume readers have some set-theoretic knowledge.

define $\mathfrak{A}$ is finite iff $|\mathfrak{A}|$ is finite. $\mathcal{L}$ is finite iff the set of symbols is finite

(Lowenheim-Skolem for countable language) : If $\Gamma$ of formulas is satisfiable in countable language $\mathcal{L}$, then $\Gamma$ is satisfiable in countable structure $\mathfrak{C}$.

proof : by soundness,$\Gamma$ is consistent in $\mathcal{L}$. thus $\Gamma$ is satisfiable in some countable $\mathfrak{C}$ by completeness theorem(remind $\mathfrak{B}$ used in completeness theorem for FOL. we can map one-to-one $\mathfrak{B}$ to $\mathfrak{A}$ using axiom of choice).

we can generalize this to any transfinite cardinality. now give up and down theorem.

(Upward Lowenheim-Skolem theorem) : let $\Gamma$ be satisfiable in $\mathcal{L}$ where $Card\mathcal{L}=\lambda$ and in infinite structure. then $\Gamma$ is satisfiable in $\mathfrak{A}$ of which cardinality is $\kappa \geq\lambda$ for every $\kappa$.

proof : add $C$ a set of new constant symbols where every member of $C$ does not occur in $\mathcal{L} $ and cardinality $\kappa$. define $\Sigma=\{c_{\alpha}\neq c_{\beta}| \alpha\neq\beta, c_{\alpha},c_{\beta} \in C \}$. consider any finite subset of $\Gamma \cup \Sigma$. then we can make some structures satisfying this finite subset(consider infinite structure $T$ for $\Gamma$. then since $T$ is infinite, we can assign finite constant symbols differently). thus by compactness theorem, $\Gamma \cup \Sigma$ is satisfiable. since cardinality of $C$ is $\kappa$, $\Gamma \cup \Sigma$ is satisfiable in some structure whose cardinality is at least $\kappa$.

for above, we need compactness theorem for arbitrary language;thus completeness for arbitrary(i don't prove this here. you can use same method used in countable. different thing is for uncountable, you've to use ordinal numbers&zorn's lemma)

(Downward Lowenheim-Skolem theorem) : let $\Gamma$ be satisfiable in $\mathcal{L}$ where $Card\mathcal{L}=\lambda$ and in infinite structure. then $\Gamma$ is satisfiable in $\mathfrak{A}$ of which cardinality is $\kappa \leq \lambda$.

proof : consider lowenheim-skolem theorem for countable language. same method is used for uncountable and arbitrarily large cardinals if we know completeness for arbitrary language.

(Full Lowenheim-Skolem theorem) Let $\Gamma$ be satisfiable in a language $\mathcal{L}$ of transfinite cardinality $\lambda$. If $\Gamma$ is satisfiable in some infinite structures and $\lambda \leq \kappa$, there exists a structure $\mathfrak{A}$ whose cardinality is exactly $\kappa$($\kappa$ is any cardinal satisfying above).

proof : use 'up and down' lowenheim-skolem theorem.

기획했던 작업이 어느 정도 마무리된 것 같다.

명제논리(PL)의 의미론, 구문론, 건전성, 완전성, compactness

1차논리(FOL)의 의미론, 구문론, 건전성, 완전성, compactness

(위의 내용들은 모두 Mathematical introduction to Logic(Enderton)의 저서에 담긴 내용입니다. 필요없는 것빼고, 필요한 것들 추가해서 포스팅했습니다)

개인적인 책 진도도 여기까진 다 끝났고 블로그에도 끝났다. 건전성 정리까지는 정말 무난하게 왔는데, 완전성 정리에서 난이도가 확 올라서 놀랐다. 사실 alphabetic existence theorem을 쓰지 않고 증명하는 방법도 있는데(사실 이게 더 간단한 증명인 듯하다), 어쩌다보니 이렇게 되었다.

1차술어논리까지의 compactness가 증명된 이후로는 대개 compactness의 응용과 model들에 대한 정리가 잠깐잠깐 등장한다. 그 내용들은 model theory를 공부하기 위한 초석이라는 듯하다. 본격적으로는 집합론 공부할 때도 듣도 못한 ultraproduct라는 개념이 등장하여 compactness를 간단히 증명해버리기도 하고..

지금까지 달려오느라(?) 힘들었기 때문에 체력을 보충하고 돌아올 예정이다. 그러나 방학이 얼마 남지 않아서 방학 기간 동안 새글을 쓰기는 무리인 것 같다. 학기 시작하면 학업에 열중해야하므로 다음 방학까지 글은 쓰지 못할 것 같다. 일단은 여기까지 쉬고 기약없이 언젠가 돌아오지 않을까싶다. 그때는 incompleteness를 증명할 수 있기를 바란다(뭐... 잠깐잠깐 들러서 글을 쓸 수도 있습니다).

 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까지 끝났으니 앞으론 조금 쉬었다가 돌아오겠습니다.

compactness theorem(a) : if $\Gamma \models \varphi$, then there exists some finite $\Gamma_0 \subseteq \Gamma$ such that $\Gamma_0 \models \varphi$.

compactness theorem(b) : $\Gamma$ is finitely satisfiable iff $\Gamma$ is satisfiable.

(*definition : $\Gamma$ is finitely satisfiable iff every finite subset of $\Gamma$ is satisfiable)

(a) : suppose $\Gamma \models \varphi$. then $\Gamma\vdash\varphi$ by completeness. now consider deduction sequence $<a_1,\ldots,a_n>$ where $a_n=\varphi$ from $\Gamma$. define $\overline{\Gamma} =\{a_k|a_k \in \Gamma\}$(this is always possible since deduction is finite. and also by axiom of choice). trivially $\overline{\Gamma}$ is finite subset of $\Gamma$. thus we get $\overline{\Gamma}\vdash\varphi$(intuitively trivial. but if you want a proof, use induction for $a_i$ for all $i<k$ in deduction seqence). then by soundness, we get $\overline{\Gamma}\models\varphi$.

(b) same as in compactness for PL, it suffices to show that rightarrow condition. now suppose (b) is false. then $\Gamma$ is finitely satisfiable and $\Gamma$ is unsatisfiable. then by completeness theorem(b), we get $\Gamma$ is inconsistent. thus $\Gamma \vdash \varphi$ and $\Gamma\vdash\neg\varphi$. sames as (a), we get finite $\Gamma_0$ such that $\Gamma_0\vdash\varphi$ and $\Gamma_0\vdash\neg\varphi$. since $\Gamma_0$ is finite, it is satisfiable. thus consistent(by soundness(b)). now contradiction occurs.

now equivalence of (a) and (b) should be introduced.

$(a)\rightarrow (b)$. suppose (a) holds and (b) does not. then $\Gamma$ is finitely satisfiable but unsatisfiable. then we get $\Gamma\models\varphi$ and $\Gamma\models\neg\varphi$. then by (a), we get finite $\Gamma_0, \Gamma_1 \subseteq \Gamma$ such that $\Gamma_0\models\varphi$ and $\Gamma_1\models\neg\varphi$. define $\overline{\Gamma}=\Gamma_0 \cup \Gamma_1$. then we get $\overline{\Gamma}\models \varphi$ and $\overline{\Gamma}\models \neg\varphi$(*). since $\overline{\Gamma}$ is finite, by (b), $\overline{\Gamma}$ is satisfiable. thus we get $s$ and $\mathfrak{A}$ such that $\models_{\mathfrak{A}}\varphi[s]$ and $\models_{\mathfrak{A}}\neg\varphi[s]$. and latter part equals $\not\models_{\mathfrak{A}}\varphi[s]$. this yields contradiction.

*if $\Gamma \subseteq \Gamma^{*}$, then $\Gamma \models\varphi \rightarrow \Gamma^{*}\models\varphi$.

proof : suppose not. then $\Gamma^{*}\not\models\varphi$. then there exist some $s$ and $\mathfrak{A}$ such that $\Gamma^{*}$ with $s$ is satisfied but $\not\models_{\mathfrak{A}}\varphi[s]$. since $\Gamma^{*}$ is satisfied, its subset $\Gamma$ is satisfied. thus we get $\models_{\mathfrak{A}}\varphi[s]$ which is contradiction.

$(b)\rightarrow (a)$. same method in compactness theorem for PL is used. suppose (b) holds. use contraposition to (a). that is,

*useful fact : $\Gamma;\neg\varphi$ is unsatisfiable iff $\Gamma\models\varphi$

$\Gamma_0 \not\models \varphi$ for every finite $\Gamma_0 \subseteq \Gamma$

$\Rightarrow$ $\Gamma_0;\neg\varphi$ is satisfiable for every finite $\Gamma_0\subseteq\Gamma$

$\Rightarrow$ $\Gamma;\neg\varphi$ is finitely satisfiable

$\Rightarrow$ $\Gamma;\neg\varphi$ is satisfiable (by b)

$\Rightarrow$ $\Gamma\not\models\varphi$.

thus (a) and (b) are equivalent.

후... 드디어 끝났네요

여기까지가 기본적인 수리논리의 분야로 들어가기 위한 첫걸음마입니다. 앞으로는 기본적인 model theory와 computability theory의 개념들을 살펴보고, 괴델의 불완전성 정리(간략한 증명은 카테고리 '학문/미분류' 참조)를 증명할 것입니다. 괴델까지 끝난다면, 한국 학부 수준에서 배울 수 있는 수리논리학은 끝이라고 봐도 무방할 것 같습니다. 그 이후에는 별 계획은 없지만 양상논리(modal logic)을 살펴보거나, 연재된 글들을 전제해서 수리논리의 각 분야(model theory, set theory, proof theory, computability theory)를 탐구할 것입니다.

※이 글은 FOL(8) - completeness theorem 다음에 오는 글입니다. completeness는 복잡하여 아직 올라오지 않았기에 보다 쉬운 이 글이 먼저 올라왔습니다.

 we'll prove completeness theorem. but before that, we'll look at equivalence first.

completeness theorem(a) : $\Gamma \models \varphi \rightarrow \Gamma \vdash \varphi$.

completeness theorem(b) : if $\Gamma$ is consistent, then $\Gamma$ is satisfiable.

we'll prove (a) and (b) are equivalent and finally, on later posting, (b) will be considered.

$(a)\rightarrow (b)$. assume (a) holds but not (b). then $\Gamma$ is consistent and $\Gamma$ is unsatisfiable. that is, there does not exist $s$ and $\mathfrak{A}$ which satisfies all member of $\Gamma$ with $s$. thus vacuosly, we get $\Gamma \models \varphi$ and $\Gamma \models \neg\varphi$. then by (a), we get $\Gamma \vdash \varphi$ and $\Gamma \vdash \neg\varphi$ which is contradiction to consistency.

$(b)\rightarrow (a)$. suppose (b) holds and but (a) does not. then $\Gamma \models \varphi$ and $\Gamma \not\vdash \varphi$. then we get $\{\Gamma;\neg\varphi\}$ is unsatisfiable(*). using contraposition of (b), we get $\Gamma;\neg\varphi$ is inconsistent. thus $\Gamma;\neg\varphi \vdash \varphi$ and $\Gamma;\neg\varphi\vdash\neg\varphi$. thus we get $\Gamma \vdash \neg\varphi\rightarrow\neg\varphi$ and $\Gamma\vdash\neg\varphi\rightarrow\varphi$ using deduction theorem. then by rule T, we get $\Gamma\vdash\varphi$. which is contradiction.

* $\Gamma;\neg\varphi$ is unsatisfiable iff $\Gamma \models \varphi$.

$(\rightarrow)$. using definition of 'satisfiable' and satisfaction, $\Gamma;\neg\varphi \models \varphi$ and $\Gamma;\neg\varphi \models \neg\varphi$. then $\Gamma\models\neg\varphi\rightarrow\varphi$ and $\Gamma\models\neg\varphi\rightarrow\neg\varphi$. thus we get $\Gamma\models\varphi$

$(\leftarrow)$. $\Gamma\models\varphi$. then $\Gamma\models\varphi\rightarrow\varphi$. then $\Gamma\models\neg\varphi\rightarrow\neg\varphi$. then we get $\Gamma;\neg\varphi\models\neg\varphi$. and since $\Gamma\models\varphi$, trivially $\Gamma\models \neg\varphi\rightarrow\varphi$. thus $\Gamma;\neg\varphi\models\varphi$. then using definition of 'satisfaction(the meaning of $\models$)', we get $\Gamma;\neg\varphi$ is unsatisfiable.

since (a) and (b) are equivalent, it suffices to show that (b) can be proved.

soundness theorem(a) : $\Gamma \vdash \varphi \rightarrow \Gamma \models \varphi$.

soundness theorem(b) : if $\Gamma$ is satisfiable, then $\Gamma$ is consistent.

(a) and (b) are equivalent. we'll prove this.

first, give definition.

Define $\Gamma$ to be satisfiable iff there is some $\mathfrak{A}$ and $s$ such that $\mathfrak{A}$ satisfies every member of $\Gamma$ with $s$.

proof

$((a) \rightarrow (b))$. suppose (a) holds and (b) does not. then we get $\Gamma$ is satisfiable, but $\Gamma$ is inconsistent. then by definition of inconsistent, we get $\Gamma \vdash \varphi$ and $\Gamma \vdash \neg\varphi$. then by (a), we get $\Gamma \models \varphi$ and $\Gamma \models \neg\varphi$. so we get both $\Gamma \models \varphi$ and $\Gamma \models \varphi$ which is contradiction. thus $(a) \rightarrow (b)$ holds.

$((b) \rightarrow (a))$. suppose (b) holds and (a) does not. then $\Gamma \vdash \varphi$ and $\Gamma \not\models \varphi$. since $\Gamma \vdash \varphi$, we get $\Gamma;\neg\varphi$ is inconsistent(see reductio ad absurdum in syntax(2)). then $\Gamma;\neg\varphi$ is unsatisfiable(contraposition of (a)). that is, there does not exist $s$ and $\mathfrak{A}$ such that $\mathfrak{A}$ satisfies every member of $\Gamma;\neg\varphi$ with $s$. so, for all $s$ and $\mathfrak{A}$, $\Gamma$ with $s$ is unsatisfiable or $\not\models_{\mathfrak{A}} \neg\varphi[s]$.

now consider $\Gamma \not\models\varphi$. this means, there exist some $\mathfrak{A}$ and $s$ such that $\Gamma$ with $s$ is satisfiable but $\not\models_{\mathfrak{A}} \varphi[s]$. then we get $\models_{\mathfrak{A}} \neg\varphi[s]$. by above fact, we must get $\Gamma$ with $s$ is unsatisfiable which is contradiction.

this proves (a) and (b) are equivalent. 

P.S. 다음 글에서는 completeness theorem을 증명할 생각입니다. completeness and its equivalent theorem~compactness theorem and its equivalence의 증명이 앞으로 고비일 듯 합니다. 그 이후에는 불완전성 정리에 대한 개념 도입 전까지는 증명이 심하게 길지는 않을 듯 싶습니다.

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.