어느 히키코모리의 블로그

몇 시간 동안 증명이 안 될 때가 가끔(아니 자주?) 있는데, 은근히 단순하게 풀리는 경우가 많다. 귀류법을 쓰면 빨리 끝나는데 생각을 못해서 질질 끄는 경우도 꽤 있다.

soundness와 completeness for FOL에 대한 증명을 접했는데, 놀랍도록 엄밀하면서 아름답고 어렵다.. 기본적인 아이디어는 soundness for PL과 compactness for PL를 이용하지만, FOL자체가 PL보다 복잡한 체계이기 때문에 증명이 매우 길다.

블로그에는 아마 soundness, completeness, compactness와 각각의 동치들&응용을 살펴보는 걸로 기본적인 논리학 정리들이 어느 정도 기틀이 잡힐 것 같다. 벤슨 메이츠 교재를 쓰는 학교를 기준으로 했을 때, 아마 completeness까지가 기본적인 철학과 학부수준의 정리라고 생각한다. 그 이후는 논리학심화(?)라고 해야할 것 같다.

compactness 이후엔 model theory와 괴델정리, 이차논리가 남는데, 이걸 블로그에 써야할지 모르겠다. 고민이다..

we'll introduce some theorems later used. i won't give full proof for below theorems but some basic ideas. readers are welcomed to prove for his own.

theorem A : $\Gamma \vdash \varphi$ iff $\Gamma \cup \Lambda$ tautologically implies $\varphi$.

proof

for $(\rightarrow)$, use induction for all $i<k $ at deduction sequence $<a_1,\ldots, a_n>$ where $a_n=\varphi$ theorem of $\Gamma$. for $a_k$, use induction principle(2 cases. $\varphi \in \Gamma \cup \Lambda$ and $\varphi$ is obtained by modus ponens).

for $(\leftarrow)$, use compactness theorem for sentential logic(second version). then you can get tautology and by using modus ponens finitely, you can get deduction of $\varphi$ from $\Gamma$

Generalization theorem : let $\Gamma \vdash \varphi$ and $x$ does not occur free in any formula in $\Gamma$. then $\Gamma \vdash \forall x \varphi$.

proof

define $S=\{\varphi | \Gamma \vdash \forall x \varphi\}$ where $\varphi$ is any theorem of $\Gamma$. use induction principle introduced at FOL(3). then you can get the result that every theorem $\varphi$ of $\Gamma$ belongs to $S$.

Rule T : if $\Gamma \vdash \alpha_1$, $\ldots$, $\Gamma \vdash \alpha_n$ and $\{\alpha_1, \ldots, \alpha_n \} \models \beta$, $\Gamma \vdash \beta$.

proof : $\alpha_1 \rightarrow \alpha_2 \rightarrow \ldots \rightarrow \alpha_n \rightarrow \beta$ is tautology. now use modus ponens at deduction from $\Gamma$ where $a_n$ for all $n \in \mathbb{N}$ is enumerated.

Deduction theorem : if $\Gamma ;\gamma \vdash \varphi$, then $\Gamma \vdash (\gamma \rightarrow \varphi)$.

proof : use theorem A. the converse part can be got from modus ponens(for this, you've to check if $\Gamma_1 \vdash \varphi$, then $\Gamma_2 \vdash \varphi$ where $\Gamma_1 \subseteq \Gamma_2$, which is trivial from definition of 'deduction'. rigorously, use induction for deduction sequence)

Contraposition theorem : if $\Gamma ; \varphi \vdash \neg \psi$, then $\Gamma ; \psi \vdash \neg\varphi$.

proof : use rule T and deduction theorem.

reduction to absurdity(reductio ad absurdum, RAA) : if $\Gamma ; \varphi$ is inconsistent, then $\Gamma \vdash \neg\varphi$.

(*$\Gamma$ is inconsistent iff $\Gamma \vdash \beta$ and $\Gamma \vdash \neg\beta$ for some $\beta$)

proof : use definition of inconsistent, deduction theorem, and rule T. actually, antecedent and consequent of RAA is equivalent if you konw 'if $\Gamma_1 \vdash \varphi$, then $\Gamma_2 \vdash \varphi$ where $\Gamma_1 \subseteq \Gamma_2$'.

Generalization on constants : Assume that $\Gamma \vdash \varphi$ and that $c$ is a constant symbol that does not occur in $\Gamma$. Then there is a variable $y$ (which does not occur in $\varphi$) such that $\Gamma \vdash \forall y \varphi_{y}^{c}$. Furthermore, there is a deduction of  $\forall y \varphi_{y}^{c}$ from $\Gamma$ in which $c$ does not occur.

(*$\varphi_{y}^{c}$ is a result of replacing $c$ to $y$)

proof

part 1 : consider deduction sequence of $\varphi$ from $\Gamma$. $<a_1,\ldots, a_n>$ where $a_n=\varphi$. verify $<{a_1}_{y}^{c},\ldots,{a_n}_{y}^{c}>$ is a deduction from $\Gamma$ using defintion of deduction(use strong induction for all $i<k$)(you can find $y$ for any variable that does not occur in deduction sequence). then we get $\Gamma \vdash \varphi_{y}^{c}$.

part 2 : consider $\Phi \subseteq \Gamma$ finite set which is used for deducing $\varphi_{y}^{c}$. then trivially $\Phi \vdash \varphi_{y}^{c}$. then $y$ does not occur in $\Phi$(consider the case $a_k \in \Gamma$. then you can understand $y$ does not occur in $a_k$ by assumption. and since c does not occur in $a_k$, $(a_k)_{y}^{c}=a_k$). then by generalization theorem, $\Phi \vdash \forall y \varphi_{y}^{c}$. thus $\Gamma \vdash \forall y \varphi_{y}^{c}$.

Theorem B : Assume that $\Gamma \vdash \varphi_{c}^{x}$ , where the constant symbol $c$ does not either occur in $\Gamma$ or in $\varphi$. Then $\Gamma \vdash \forall x \varphi$, and there is a deduction of $\forall x \varphi$ from $\Gamma$ in which $c$ does not occur.

proof : use generalization theorem and axiom group 2 and re-replacement lemma.

(* re-replacement lemma : if $y$ does not occur in $\varphi$, then $x$ is substitutable for $y$ in $\varphi_{x}^{y}$ and $(\varphi_{y}^{x})_{x}^{y}=\varphi$)(for this, use induction for formulas)

Rule EI : let $c$ does not occur in $\varphi,\psi, \Gamma$ and $\Gamma ; \varphi_{c}^{x} \vdash \psi$. then $\Gamma ; \exists \varphi \vdash \psi$.

proof : use contraposition theorem and rule T(or use tautology that $(\alpha \rightarrow \beta) \rightarrow (\neg\beta \rightarrow \neg\alpha)$. also use theorem B.

alphabetic variants theorem : let $\varphi$ be any formula, $t$ a term, $x$ a variable. then there exists $\varphi'$ such that $\varphi \vdash \varphi'$ and $\varphi' \vdash \varphi$, and $t$ is substitutable for $x$ in $\varphi'$.

proof : use induction for formulas. for atomic, $\varphi'=\varphi$. and each case, take $(\neg\varphi)'=\neg\varphi'$, $(\varphi \rightarrow \psi)'=\varphi' \rightarrow \psi'$. but situation differs about $\forall y \varphi$. in this case, take $(\forall y \varphi)'=\forall z(\varphi')_{z}^{y}$. and divide cases into $x$ does not occur free, and $x$ does occur free in $\varphi'$ where $t$ is substitutable for $x$ in $\varphi'$ by inductive hypothesis. the intuitive idea for quantifier is like this;

suppose we want to have '$y$ is substitutable for $x$' in $\forall y Pxy$ for getting axiom group2 formula $\vdash \forall x \forall y Pxy \rightarrow \forall y Pyy$. but this always fails. to get this, we can change some variables in $\forall x \forall y Pxy$ like $\forall x \forall z Pxz$ where they are deducible from each other. then clearly $y$ is substitutable for $x$ in $\forall x \forall z Pxz$ we've taken and thus $\vdash \forall x \forall z Pxz \rightarrow \forall y Pyy$. thus if you can calculate $\vdash \forall x \forall y Pxy \rightarrow \forall x \forall z Pxz$, original formula can be proved.

Equality theorem(equivalence relation of '=')

(i) '=' is reflexive : $\vdash x=x$

(ii) '=' is symmetric : $\vdash x=y\rightarrow y=x$

proof

$\vdash x=x\rightarrow (x=x \rightarrow x=y)$ by axiom group6

$\vdash x=x\rightarrow x=y$ since $x=x$ is in axiom group5 & using rule T

(iii) '=' is transitive : $\vdash x=y\rightarrow y=z\rightarrow x=z$

proof

$\vdash y=x \rightarrow y=z\rightarrow x=z$ by axiom group5

then $x=y\vdash y=x$ thus $x=y\vdash y=z\rightarrow x=z$. hence,

$\vdash x=y\rightarrow y=z\rightarrow x=z$ by deduction theorem.

using generaliation theorem on (i), (ii), (iii), we get

$\vdash \forall x x=x$

$\vdash \forall x \forall y x=y\rightarrow y=x$

$\vdash \forall x \forall y \forall z x=y\rightarrow y=z\rightarrow x=z$

For saying 'syntax', we mean we have some formal rules which indicates how to yields some formulas from inference rules. In this part, basically, we don't inquire any semantical concepts; just do give some finite sequences from selected rules.

now define deduction of $\varphi$ from $\Gamma$ as a finite sequence $<a_1,\ldots,a_n>$ of formulas where $a_n = \varphi$, and for every formula $a_k$,

(a) $a_k \in \Gamma \cup \Lambda$ or

(b) $a_k$ is obtained by modus ponens from $a_i$ and $a_j=(a_i \rightarrow a_k)$ where for some $i,j<k$.

if there is a deduction of $\varphi$ from $\Gamma$, we call $\varphi$ is a theorem of $\Gamma$ or $\varphi$ is deducible from $\Gamma$. In our notation, we define this $\Gamma \vdash \varphi$.

$\Lambda$ is a set of axioms. basic axioms we'll use are divided into 6 groups.

1. tautologies.

2. $\forall x \alpha \rightarrow \alpha_{t}^{x}$, where $t$ is substitutable for $x$ in $\alpha$

3. $\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)$

4. $\alpha \rightarrow \forall x \alpha$ where $x$ does not occur free in $\alpha$

5. $x=x$

6. $(x=y) \rightarrow (\alpha \rightarrow \alpha')$, where $\alpha$ is an atomic formula, and $\alpha'$ is obtained by replacing zero or more times $x$ by $y$.

then define $\varphi \in \Lambda$ iff $\varphi$ is a generalization of $\psi$. $\varphi$ is a generalization of $\psi$ iff $\varphi = \forall x_1 \ldots \forall x_n \psi$ where $n \in \mathbb{N} \cup \{0\}$.

explanation will be needed for some axiom groups.

1. tautology is a concept of PL. and we can consider each FOL formulas each sentence symbols in PL. for axmple, $Pt$and $\forall x Px$ are regarded as sentence symbols. for precise definition, we've to introduce some notions.

define prime formula $\varphi$ as $\varphi$ is atomic formula or $\varphi = \forall x \psi$. then for every prime formulas, using sentential connectives $\rightarrow, \neg$, we can construct every FOL formulas. and every FOL formula can be regarded as PL formula. using this idea, we'll use tautologies as axioms.

for example, $Px \rightarrow Px$ is tautology and so does $(\forall x Py \rightarrow \neg Pc) \rightarrow (Pc \rightarrow \neg\forall x Py)$. remember any generalizations of these are axioms.

2. now define $\alpha_{t}^{x}$ and '$t$ is substitutable for $x$ in $\alpha$'.

a. we define substitution $\alpha_{t}^{x}$ of $\alpha$ recursively;replacing free variable $x$ of $\alpha$ by term $t$.

(i) if $\alpha$ is atomic formula, then $\alpha_{t}^{x}$ is replacing every $x$ occurs in $\alpha$ by $t$.

(ii) $(\neg \alpha)_{t}^{x} = (\neg \alpha_{t}^{x})$

(iii) $(\alpha \rightarrow \beta)_{t}^{x} = (\alpha_{t}^{x} \rightarrow \beta_{t}^{x})$

(iv) $(\forall y \alpha)_{t}^{x} = \forall y \alpha \quad\text{if $x=y$},\quad \text{or}\quad \forall y (\alpha_{t}^{x}) \quad\text{if $x \neq y$} $.

b. define $t$ is substitutable for $x$ in $\alpha$ recursively.

(i) $t$ is always substitutable for $x$ in any atomic formula $\alpha$.

(ii) $t$ is substitutable for $x$ in $\neg \alpha$ iff $t$ is substitutable for $x$ in $\alpha$

(iii) $t$ is substitutable for $x$ in $\alpha \rightarrow \beta$ iff $t$ is substitutable for $x$ in $\alpha$ and $\beta$

(iv) $t$ is substitutable for $x$ in $\forall y \alpha$ iff (1) $x$ does not occur free in $\forall \alpha$ or (2) $y$ does not occur in $t$ and $t$ is substitutable for $x$ in $\alpha$.

note for substitution.

1. $\varphi_{x}^{x}=\varphi$

2. $x$ is substitutable for $x$ in any formula.

3. if $t$ contains no variables in $\varphi$, then $t$ is substitutable for $x$ in $\varphi$.

(you can check 2-3 using induction for formulas)

now introduce a induction principle for our syntax.

define a set $S$ of formulas is closed under modus ponens if $\alpha \in S$ and $(\alpha\rightarrow\beta) \in S$, then $\beta \in S$.

Induction principle : let a set $S$ of formulas such that $\Gamma \cup \Lambda \subseteq S$ and $S$ is closed under modus ponens. then $S$ contains every theorem of $\Gamma$.

proof : consider any $\varphi$ theorem of $\Gamma$. then there exists a deduction $<a_1,\ldots, a_n>$ where $a_n=\varphi$. give strong induction for all $i<k$ such that $a_i \in S$. now think about $a_k$.

case 1 : $a_k \in \Gamma \cup \Lambda$. then trivially $a_k \in S$.

case 2 : $a_K$ is obtained by modus ponens using earily made formulas $a_i$ and $a_j=(a_i \rightarrow a_k)$ for some $i,j<k$ where $a_i, a_j \in S$ by inductive hypothesis. since $S$ is closed under modus ponens, we get $a_k \in S$ trivially.

we'll use this induction principle many times from now on.

P.S. you may wonder the intuitive idea about 'substitutable'.

revisited; 2. $\forall x \alpha \rightarrow \alpha_{t}^{x}$, where $t$ is substitutable for $x$ in $\alpha$

it is easy to understand for $\alpha_{t}^{x}$ where we change every free variable $x$ in $\alpha$ to term $t$. if $x$ does not freely occur or does not occur in $\alpha$, then $\alpha_{t}^{x}=\alpha$ trivially. this concept is easy to understand. but 'substitutable' is somewhat complicated concept introduced for some reasons(one reason is for the soundness theorem of FOL, but you do not need to care details yet).

consider $\forall x \alpha \rightarrow \alpha_{t}^{x}$. consider $\alpha= \forall x \neg\forall y x=y$. then $\forall x \alpha \rightarrow \alpha_{t}^{x}$ is $\forall x \neg\forall y x=y \rightarrow \neg\forall y y=y$. since latter part of conditional is always false, we cannot say without the condition '$t$ is substitutable for $x$', axiom group 2 could be false. so for this not to happen, we gave that condition.

In contrast with PL, in FOL, the concept of T/F differs by structures. by stucture, I mean we have some rules translating formal language into given language.

we define structure a function $\mathfrak{A}=<|\mathfrak{A}|;P,f,c>$ whose domain is parameters satisfying below.

1.  $\mathfrak{A}$ assigns to $\forall$ the universe of $\mathfrak{A}$, $|\mathfrak{A}|$ which is nonempty set.

2. $\mathfrak{A}$ assigns to every $P$ of $n$-place predicate symbol a relation $P^{\mathfrak{A}} \subseteq |\mathfrak{A}|^n$ where $P^{\mathfrak{A}}$ a set of n-tuples given by some interpretation.

3. $\mathfrak{A}$ assigns to each $n$-place function symbol $f$ a function $f^{\mathfrak{A}} : |\mathfrak{A}|^n \rightarrow |\mathfrak{A}|$.

4. $\mathfrak{A}$ assigns to each constant symbol c $c^{\mathfrak{A}} \in \mathfrak{A}$.

intuitionistic idea of structure is giving meaning to parameters(function, predicate, constant symbol). if we are given some structure, then $\forall$ means everything in $|\mathfrak{A}|$, $P$ $P^{\mathfrak{A}}$, $f$ $f^{\mathfrak{A}}$, and $c$ $c^{\mathfrak{A}}$.

now define concept of truth. be careful that in FOL, 'truth' is defined in some structures. truth concept without structure is not defined in FOL(but defined in PL). thus we must define 'sentence $\sigma$ is true in structure

$\mathfrak{A}$'. we symbolize this as '$\models_{\mathfrak{A}} \sigma$'. before defining this, we have to give some boring concepts about wffs.

$\models_{\mathfrak{A}}\sigma$
 

let $\varphi$ be a wff of the given language, and $\mathfrak{A}$ a given structure. we'll define '$\mathfrak{A}$ satisfies $\varphi$ with $s$' symbolized as $\models_{\mathfrak{A}} \varphi[s]$.

define $s : V \rightarrow |\mathfrak{A}|$ where $V$ is a set of variables, and $|\mathfrak{A}|$ the universe of our structure. and extend $s$ to $\bar{s}$ where $$\bar{s} : T \rightarrow |\mathfrak{A}|$$ where $T$ is a set of terms satisfying below.

1. if $x \in V$, $\bar{s}(x)=s(x)$

2. for each constant symbol $c$, $\bar{s}(c)=c^{\mathfrak{A}}$.

3. if $t_1,t_2,\ldots, t_n$ are terms and $f$ is a function symbol, then $\bar{s}(ft_1\ldots t_n)=f^{\mathfrak{A}}(\bar{s}(t_1),\ldots, \bar{s}(t_n))$.

now define satisfaction as below.

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

2. for a $n$-place predicate symbol P, $\models_{\mathfrak{A}} Pt_1\ldots t_n[s]$ iff $<\bar{s}(t_1), \ldots, \bar{s}(t_n)> \in P^{\mathfrak{A}}$.

1-2 is about atomic formulas.

3. $\models_{\mathfrak{A}} \neg \varphi[s]$ iff $\not\models_{\mathfrak{A}} \varphi[s]$

4. $\models_{\mathfrak{A}} (\varphi \rightarrow \psi)[s]$ iff $\not\models_{\mathfrak{A}} \varphi[s]$ or $\models_{\mathfrak{A}} \psi[s]$

5. $\models_{\mathfrak{A}} \forall \varphi$ iff for every $d \in |\mathfrak{A}|$, $\models_{\mathfrak{A}} \varphi[s(x|d)]$ where $s(x|d)$ is exactly same with $s$ except at $x$. at $x$, $s(x|d)(x)=d$. which is expressed as $$s(x|d)(y) = s(y)\quad\text{if y $\neq$ x}, \text{or}\quad d \quad\text{if y=x} $$

Lemma for sentence satisfaction : assume that $s_1$ and $s_2$ are functions from $V$ into $|\mathfrak{A}|$ which agree at all variables (if any) that occur free in the wff $\varphi$. Then $\models_{\mathfrak{A}} \varphi[s_1]$ iff $\models_{\mathfrak{A}} \varphi[s_2]$.

proof : use induction on formulas type 2-5(especially, at atomic formula, use strong induction for terms for all $i<k$).

theorem : for a sentence $\sigma$, one of (a), (b) holds.

(a) $\mathfrak{A}$ satisfies $\psi$ for every $s$, or
(b) there does not exist $s$ where $\sigma$ is satisfied in $\mathfrak{A}$.

if (a) holds, we say $\sigma$ is true in $\mathfrak{A}$, and $\mathfrak{A}$ is a model of $\sigma$. otherwise, $\sigma$ is false in $\mathfrak{A}$. each is symbolized as $\models_{\mathfrak{A}} \sigma$ and $\not\models_{\mathfrak{A}} \sigma$

satisfaction of abbrevated some formulas.

1. $\models_{\mathfrak{A}} (\alpha \wedge \beta)[s]$ iff $\models_{\mathfrak{A}} \alpha[s]$ and $\models_{\mathfrak{A}} \beta[s]$

2. $\models_{\mathfrak{A}} (\alpha \vee \beta)[s]$ iff $\models_{\mathfrak{A}} \alpha[s]$ or $\models_{\mathfrak{A}} \beta[s]$

3. $\models_{\mathfrak{A}} (\alpha \leftrightarrow \beta)[s]$ iff $\models_{\mathfrak{A}} (\alpha \rightarrow \beta)[s]$ and $\models_{\mathfrak{A}} (\beta \rightarrow \alpha)[s]$

4. $\models_{\mathfrak{A}} \exists x \alpha[s]$ iff for some $d \in \mathfrak{A}$, $\models_{\mathfrak{A}} \alpha[s(x|d)]$.

Logical Implication

definition : Let $\Gamma$ be a set of wffs, $\varphi$ a wff. Then $\Gamma$ logically implies $\varphi$, written $\Gamma \models \varphi$ iff for every structure $\mathfrak{A}$ for the language and every function $s : V \rightarrow |\mathfrak{A}|$ such that $\mathfrak{A}$ satisfies every member of $\Gamma$ with $s$, $\mathfrak{A}$ also satisfies $\varphi$ with $s$.

simply, $\Gamma \models \varphi$ iff for every $s$ and $\mathfrak{A}$, $\models_{\mathfrak{A}} \Gamma[s] \rightarrow \models_{\mathfrak{A}} \varphi[s]$.

another deifnitions.

$\psi \models \varphi$ and $\varphi \models \psi$ iff $\psi$ and $\varphi$ are logically equivalent. and $\varphi$ is valid iff $\emptyset \models \varphi$(shortly $\models \varphi$).

completeness theorem : $\Sigma \models \tau \rightarrow \Sigma \vdash \tau$.

Proof

let $\Sigma \models \tau$. then by compactness theorem^[각주:1], we get some finite set $\Sigma_0 \subseteq \Sigma$ such that $\Sigma_0 \models \tau$. let $\Sigma_0 =\{a_0, a_1, \ldots, a_n\}$. then $\{a_0, a_1, \ldots, a_n\} \models \tau$. then we get $\models a_0 \rightarrow a_1 \rightarrow a_2 \ldots \rightarrow a_n \rightarrow \tau$. for this, you must check $\Sigma;\alpha \models \beta \leftrightarrow \Sigma \models (\alpha \rightarrow \beta)$. i'll leave out this for readers.

consider deduction sequence $<b_0,b_1,\ldots,b_i>$ends with $\tau$ from $\Sigma$.

for $\models a_0 \rightarrow a_1 \rightarrow a_2 \ldots \rightarrow a_n \rightarrow \tau$, choose $b_0=a_0 \rightarrow a_1 \rightarrow a_2 \ldots \rightarrow a_n \rightarrow \tau$ which is tautology. then $b_1=a_0$, and by modus ponens, we get $b_2=a_1 \rightarrow a_2 \ldots \rightarrow a_n \rightarrow \tau$. by using modus ponens finitely, we get $a_k=\tau$ for some $k$ finite. this means there exist some deduction ends with $\tau$ from $\Sigma$. now we get $\Sigma \vdash \tau$. hence, completeness theorem is proved.

define a deduction from a set of wffs $\Sigma$ to be finite sequence $<a_0,a_1, \ldots, a_n>$ of wffs such satisfying either (i), (ii), (iii) for each $k \leq n$.

(i) $a_k$ is a tautology

(ii) $a_k \in \Sigma$

(iii) for some $i, j < k$, $a_i=a_j \rightarrow a_k$. this is the inference rule for PL, we'll use, named Modus Ponens.

if there exists a deduction ends with $\varphi$ from $\Sigma$, we'll symbolize this as $\Sigma \vdash \varphi$.

Soundness theorem : $\Sigma \vdash \tau \rightarrow \Sigma \models \tau$.

Proof : let $\Sigma \vdash \tau$. then there exists a deduction sequence from $\Sigma$ such that $<a_0,a_1, \ldots, a_n>$ which ends with $\tau$.

we'll use induction for all $k<i$. give inductive hypothesis that for all $i<k$,  $\Sigma \models a_k$. then by showing $\Sigma \models a_i$, our proof will be over.

since $a_k$ an element of deduction sequence, $a_k$ must satisfy one of (i), (ii), (iii). now check each case.

case 1 : $a_k$ is a tautology. then $\models a_k$. trivially $\Sigma \models a_k$ since tautology cannot be false in any case.

case 2 : $a_k \in \Sigma$. this case is also trivial. by definition, if $\Sigma$ is satisfied, clearly the member $a_k$ is true. thus $\Sigma \models a_k$.

case 3 : $a_k$ is obtained by some priorly made elements of deduction sequence $a_i$ and $a_j=(a_i \rightarrow a_k)$. and by inductive hypothesis, $\Sigma \models a_i$ and $\Sigma \models a_j$

consider any truth assignemnt for $\Sigma$ which is satisfied. then by hypothesis, we get $\bar{v}(a_i)=T$ and $\bar{v}(a_i \rightarrow a_k)=T$. let $\bar{v}(a_k)=F$. then since $\bar{v}(a_i)=T$ and $\bar{v}(a_k)=F$, we must get $\bar{v}(a_i \rightarrow a_K)=F$ which is contradicton. thus $\bar{v}(a_k)=T$. now $\Sigma \models a_k$.

all case is satisfied. now by strong mathematical induction, $\Sigma \models a_k$ for all $a_k$ of deduction sequence for $\tau$. hence, the last element $a_n=\tau$ is also satisfied. therefore, $\Sigma \models \tau$.

 내가 아는 한, 한국 학부 수업에서 정기적으로 괴델정리를 제대로 다루는(증명) 곳은 연대뿐이고, 가끔씩 고대에서도 관련 강의가 열린다. 그 외에는 여러 철학과에서 벤슨 메이츠의 기호논리학 정도를 다루는 것밖에 보지 못했다. 안타까운 상황이다. 영미권 학교 강의들을 훑어보면 학부에서도 수리논리를 적지 않게 다루고, 철학과에서도 많이 다룬다.

예시로 MIT 학부 철학과에는 다음과 같은 과목들이 있다.

Paradox and Infinity

Logic I

Logic II

Classical Set Theory

Modal Logic

Theory of Models

Philosophy of Mathematics

Foundations of Probability

Topics in Philosophical Logic

한국의 모든 철학과와 비교가 되지 않는가.. 상황이 이렇다보니 영미권의 연구자와 한국의 연구자는 엄청난 차이가 있을 수밖에 없다. 정말 안타까운 상황이다.

그래서 언젠가 기회가 된다면 여러 주제를 가지고 논리학 세미나를 진행해보고 싶다. 여러 사람들에게 논리학이라는 분야가 도대체 뭔지 구체적으로 소개해보고 싶다.

교양수준에서 배우는 논리학을 잠깐하고, 집합론~수리논리~양상논리 정도면 괜찮지 않을까 생각하고 있다.

...

근데 기회가 있으려나 모르겠다. 애초에 한국에 논리학에 관심이 있는 사람이 많기나 할까.