不完全性定理（菊池、共立出版）を読んでみた　（絶賛執筆中）

# はじめに
不完全性定理について勉強しようと思い立ち、本書[「不完全性定理」（菊池、共立出版）](https://www.amazon.co.jp/%E4%B8%8D%E5%AE%8C%E5%85%A8%E6%80%A7%E5%AE%9A%E7%90%86-%E8%8F%8A%E6%B1%A0-%E8%AA%A0/dp/432011096X)を手に取りました:laughing:
しかし、大学教養程度の数学しか知らない私にとっては、内容が難しく、このままでは理解できないと感じました:sob::sob::sob:
そこで、本書の要点だけを纏めたノートを作れば、少しは理解が深まるかと思い、簡単に纏めてみることとしました:muscle::innocent:

![不完全性定理（菊池）](https://images-na.ssl-images-amazon.com/images/I/31Zf1T4T-CL._SX353_BO1,204,203,200_.jpg "不完全性定理（菊池、共立出版）")

**これから、不完全性定理を勉強しようと思っている方へ**
本ノートだけでも、概要はつかめるように書いていくつもりです。しかし、ぜひ概要が分かったら本書にもチャレンジしてみてください！

<font color="DeepPink">本稿は絶賛執筆中のため、まだまだ不完全なところがあります。
気力がいつまで続くかも分からないので、このノートが完成するかどうかも、分かりません。
でも、少しでも役に立てばと思い、公開しています。ご了承ください。
### 記法
本ノートは、以下に分けて、説明を進めていきます。
:pencil: **用語の解説**
用語の定義を解説します。
:symbols: **記号の解説**
記号を解説します。
:point_up: **ポイント**
重要な考え方を解説します。
:pushpin: **まとめ**
理解すべきことを、要所ごとにまとめていきます。この纏め方は、本書に準拠していません。
個人的な見解については、斜体であらわします。*カレーが食べたいなぁ。*

# 第二章　命題論理

## 命題、論理式
:pencil: **原子的命題**
分解不可能な基本的な命題。「ポチは走る」等。

:pencil: **命題論理**
原子的命題から命題結合子（後述）を用いて構成された命題に対し、論理的な振る舞いを分析する枠組み。

:pencil: **述語論理**
原子的命題は「主語＋述語」の形式として、命題結合子と量子化（すべての、存在する）を用いて構成された命題に対し、論理的な振る舞いを分析する枠組み。
*本章では扱わない。この後、勉強することになる。*

:pencil: **命題結合子**
命題をつないで新たな命題を作るもの。「でない($\neg $)、かつ($\wedge $)、または($\vee $)、ならば($\rightarrow $)」の4種類が存在するが、2種類あれば十分。本書では「でない($\neg $)、ならば($\rightarrow $)」だけを使っている。

:pencil: **論理式** $\phi, \psi, \dots$
命題変数*（原子的命題のことと思っておけば十分）*と、これに命題結合子を繋げたもの。再帰的に定義されており、命題結合子はどんな繋げ方で、いくつ繋げてもよい。

:pencil: **理論（形式的理論、公理系）** $T$
論理式の集合

:pencil: **非論理的公理（公理）**
ある理論の要素である論理式

:pushpin: **命題、論理式のまとめ**
*原子的命題に命題結合子を繋げていくことで、論理式を構成することができる。この論理式が、まさに命題。
理論というのは、論理式（非論理的公理）の寄せ集め。なぜ"非論理的"なのかは、あとで分かります。*

## 真理値と割り当て
:pencil: **真理値**
真[$\mathbb{T}$]と偽[$\mathbb{F}$]の2つの記号

:pencil: **真理値の割り当て（付値、割り当て）** $v$
命題変数全体の集合から真理値の集合への関数。*命題変数については、詳しく説明されていないが、原子的命題だと捉えて差し支えなさそう。*
つまり、命題を入力として、真か偽かを出力する関数。
命題変数$A$が真ならば、$ v(A) = \mathbb{T} $
偽ならば、$ v(A) = \mathbb{F} $
と表す。

:point_up: **真理値の割り当ての拡張** $\bar v$
真理値の割り当てが存在する状況で、命題変数のみならず、すべての論理式に真理値を与えること。
命題結合子「でない、ならば」を含む論理式に対して、それぞれの真と偽を再帰的に定義する。

1. $ \bar v (A) = v (A) $
1. $ \bar v (\phi) = \mathbb{T} $ ならば $ \bar v (\neg\phi) = \mathbb{F}$、  $ \bar v (\phi) = \mathbb{F} $ ならば $ \bar v (\neg\phi) = \mathbb{T}$
1. $ \bar v (\phi) = \mathbb{T} $ かつ $ \bar v (\psi) = \mathbb{F} $ ならば $ \bar v (\phi \rightarrow \psi) = \mathbb{F} $、それ以外は $ \bar v (\phi \rightarrow \psi) = \mathbb{T}$


「真理値の割り当て$v$」と「真理値の割り当ての拡張$\bar v$」は一対一対応するので、後者も「真理値の割り当て$v$」と称する。

:symbols: **論理式の真偽** [割り当て]$\models$[論理式],  [割り当て]$\not \models$[論理式]
真理値の割り当て$v$と論理式$\phi$について、
$ v(\phi) = \mathbb{T} $ を $ v \models \phi$
$ v(\phi) = \mathbb{F} $ を $ v \not \models \phi$
と表す。

:pencil: **恒真式**
すべての真理値の割り当て（広義）に対して、真となる論理式。
つまり、原子的命題の真偽によらず真となる命題のこと。

:pencil: **モデル**
ある理論に対して、これが含むすべての論理式が真になるような、真理値の割り当て

:symbols: **モデル** [割り当て]$\models$[理論]
割り当て$v$が理論$T$のモデルであることを、$ v \models T$と表す。

:pencil: **帰結、論理的帰結**
ある理論におけるすべてのモデルに対して、真となる論理式
*理論に含まれる論理式がすべて正しいと仮定して（モデル）、それ以外の論理式の真偽にかかわらず、常に真になる論理式のこと。*

:symbols: **帰結** [理論]$\models$[論理式], [理論]$\not \models$[論理式]
論理式$\phi$が理論$T$の帰結であることを、$ T \models \phi$と表す。
論理式$\phi$が理論$T$の帰結でないことを、$ T \not \models \phi$と表す。

:pushpin: **真理値と割り当てのまとめ**
*命題に対して真偽を与えることを、割り当てという概念で説明した。
理論（命題の集合）に含まれる全命題が、すべて真となる割り当てをモデルと称し、このなかでどんなモデルを持ってきても真になる命題を、その理論の帰結という。*

## 証明

:point_up: **命題論理の体系** $\mathfrak{S}$
証明を形式的に表現するための、論理的公理、推論規則からなる枠組み。論理的公理、推論規則の選び方にはさまざまな流派が存在する。本書はHilbert流。

:pencil: **論理的公理**
正しいことが自明である命題。恒真式であることが明らかな論理式。
*証明なしに恒真式と分かるもの。非論理的公理は論理的公理とは異なり、背景に論理性がなくても公理とみなせるから、"非論理的"だったのだ。*

:pencil: **推論規則**
証明の構成に用いてよい推論。
論理式$\phi_1, \dots, \phi_n$があって、$v \models \phi_1, \dots, v \models \phi_n$を満たすすべての割り当て$v$において、$v \models \psi$になる場合、「$\phi_1, \dots, \phi_n$（仮定）から$\psi$（結論）を導く」推論という。
記号では、$\frac{\phi_1\quad \dots \quad \phi_n}{\psi}$と表現する。
*モデルと帰結の関係に似ているなぁ。*

:point_up: **証明とは**
論理式の有限列。$(\phi_1, \dots, \phi_n)$
理論と、命題論理の体系（＝論理的公理＋推論規則）が定義されているとして、各論理式が
・非論理的公理（理論の要素）
・論理的公理
・既出の論理式を仮定とし推論規則で結論づけることが可能な論理式
のいずれかであるもの。

:pencil: **定理**
証明として導くことが可能な論理式

:symbols: **証明可能** [理論]$\vdash$[論理式], [理論]$\not \vdash$[論理式]
理論$T$のもとで論理式$\phi$を導く証明が存在することを、$T \vdash \phi$と書く。
理論$T$のもとで論理式$\phi$を導く証明が存在しないことを、$T \not \vdash \phi$と書く。
特に理論$T$が空集合で、$\phi$を導く証明が存在することを、$\vdash \phi$と書く。

:point_up: **証明に関する補題**
・証明となる論理式の有限列を、最初から任意の個数で打ち切ったものも、また証明である。
・定理を証明に用いてよい
・ある理論と、そのすべての要素を含むより大きな理論を考えたとき、もとの理論における定理は、より大きな理論でも定理である。
・ある理論におけるモデルがあったとして、この理論における定理は、このモデルのもとで真である。

:pushpin: **証明のまとめ**
*証明は、論理式の有限列。
理論（必須ではない）と、命題論理の体系（＝論理的公理＋推論規則）から、順番に導かれていくものである。*

## Hilbert流の命題論理の体系

:point_up: **Hilbert流の命題論理の体系** $\mathfrak{S_0}$
3つの論理的公理と、1つの推論規則からなる体系である。
論理的公理：
- [Ax1] $\phi \rightarrow ( \psi \rightarrow \phi)$
- [Ax2] $\left( \phi \rightarrow (\psi\rightarrow\rho) \right) \rightarrow ( (\phi\rightarrow\psi) \rightarrow(\phi \rightarrow \rho) )$
- [Ax3] $(\neg\phi \rightarrow \neg\psi) \rightarrow (\psi\rightarrow\phi)$
推論規則：
- [MP] $\frac{\phi \quad (\phi\rightarrow\psi)}{\psi}$（φかつ(φ→ψ)ならば、ψである）
*ちょっと分かりにくいけど、
[Ax1]は、「成立している命題は、どんな前提を置いても成立する」。
[Ax2]は、「分配則が成立する」。
[Ax3]は、「対偶は真である」。
ってことかな、と思っています。全部覚えていないと、証明を導くのが大変。*

:point_up: **恒真式の証明方法**
<details><summary>$\def\a{\phi} \def\b{\psi} \def\c{\rho} \def\r{\rightarrow} \a \r \a$の証明</summary>
[1. Ax1] $\a \r (\a \r \a)$
[2. Ax1] $\a \r ((\a \r \a)\r \a)$
[3. Ax2] $(\a \r ((\a \r \a)\r \a)) \r ((\a \r (\a \r \a)) \r (\a \r \a))$
[4. MP(2.3.)] $ (\a \r (\a \r \a)) \r (\a \r \a) $
[5. MP(1.4.)] $ \a \r \a $
</details>
<details><summary>$(\a \r (\b \r \c)) \r (\b \r (\a \r \c))$の証明</summary>
[1. Ax2] $(\a \r (\b \r \c)) \r ((\a \r \b)\r(\a \r \c))$
[2. Ax1] $((\a \r \b) \r (\a \r \c)) \r ( \b \r ((\a \r \b) \r (\a \r \c)))$
ここで、$A \equiv (\a \r (\b \r \c)), B \equiv ((\a \r \b)\r(\a \r \c)), C \equiv ( \b \r ((\a \r \b) \r (\a \r \c)))$
とすると、[1.] $ A \r B $、[2.] $B \r C$である。
[3. Ax1] $ (B \r C) \r ( A\r (B \r C) ) $
[4. MP(2.3.)] $ A \r (B \r C) $
[5. Ax2] $ (A \r(B \r C)) \r ( (A\r B) \r  (A \r C) ) $
[6. MP(4.5.)] $ A \r C$
[7. Ax2] $ ( \b \r ((\a \r \b) \r (\a \r \c))) \r ( ( \b \r (\a \r \b)) \r ( \b \r (\a \r \c) ) ) $
ここで、$D \equiv ( ( \b \r (\a \r \b)) \r ( \b \r (\a \r \c) ) )$
とすると、[7.] $ C \r D $である。
[8. Ax1] $ (C  \r D) \r ( A \r (C \r D)) $
[9. MP(7.8.)] $ A \r (C \r D) $
[10. Ax2] $ (A \r (C \r D)) \r ((A \r C)\r (A \r D)) $
[11. MP(9.10.)] $(A \r C)\r (A \r D)$
[12. MP(6.11.)] $ A \r D $
[13. Ax2] $ (A \r ( ( \b \r (\a \r \b)) \r ( \b \r (\a \r \c) ) )) \r ((A \r ( \b \r (\a \r \b)))\r(A \r ( \b \r (\a \r \c) )))$
$D$を展開して、
[14. MP(12.13.)] $ (A \r ( \b \r (\a \r \b)))\r(A \r ( \b \r (\a \r \c) ))$
[15. Ax1] $ \b \r (\a \r \b) $
[16. Ax1] $ (\b \r (\a \r \b)) \r (A \r (\b \r (\a \r \b))) $
[17. MP(15.16.)] $ A \r (\b \r (\a \r \b)) $
$A$を展開して、
[18. MP(14.17.)] $ (\a \r (\b \r \c)) \r ( \b \r (\a \r \c) ) $
*演繹定理（後述）を使うと簡単に解ける（本書参照）けど、使わない証明はすごく大変:sob:*
</details>
<details><summary>$ (\a \r \b) \r ((\b \r \c)\r(\a \r \c))$の証明</summary>
[1. Ax2] $ (\a \r (\b \r \c))\r ((\a \r \b) \r (\a \r \c)) $
$A \equiv ((\a \r \b) \r (\a \r \c))$とする。[1.] $ (\a \r (\b \r \c))\r A $
[2. Ax1] $ (\b \r \c) \r (\a \r (\b \r \c)) $
[3. Ax1] $ ((\a \r (\b \r \c))\r A) \r ( (\b \r \c) \r ((\a \r (\b \r \c))\r A)) $
[4. MP(1.3.)] $ (\b \r \c) \r ((\a \r (\b \r \c))\r A) $
[5. Ax2] $ ((\b \r \c) \r ((\a \r (\b \r \c))\r A)) \r (( (\b \r \c)\r (\a \r (\b \r \c))) \r ((\b \r \c) \r A)) $
[6. MP(4.5.)] $ ( (\b \r \c)\r (\a \r (\b \r \c))) \r ((\b \r \c) \r A) $
[7. MP(2.6.)] $ (\b \r \c) \r A $
[8. Ax2] $ ((\b \r \c) \r ((\a \r \b) \r (\a \r \c))) \r (((\b \r \c) \r (\a \r \b)) \r ((\b \r \c)\r(\a \r \c))) $
$A$を展開して、
[9. MP(7.8.)] $ ((\b \r \c) \r (\a \r \b)) \r ((\b \r \c)\r(\a \r \c)) $
$B\equiv ((\b \r \c)\r(\a \r \c))$とする。[9.] $ ((\b \r \c) \r (\a \r \b)) \r B $
[10. Ax1] $ (((\b \r \c) \r (\a \r \b)) \r B) \r ( (\a \r \b) \r (((\b \r \c) \r (\a \r \b)) \r B)) $
[11. MP(9.10.)] $  (\a \r \b) \r (((\b \r \c) \r (\a \r \b)) \r B) $
[12. Ax2] $ ((\a \r \b) \r (((\b \r \c) \r (\a \r \b)) \r B)) \r (((\a \r \b) \r ((\b \r \c) \r (\a \r \b))) \r ((\a \r \b) \r B)) $
[13. MP(11.12.)] $ (((\a \r \b) \r ((\b \r \c) \r (\a \r \b))) \r ((\a \r \b) \r B) $
[14. Ax1] $ ((\a \r \b) \r ((\b \r \c) \r (\a \r \b)) $
$B$を展開して、
[15. MP(13.14.)] $ (\a \r \b) \r ((\b \r \c)\r(\a \r \c)) $
*いわゆる、三段論法ですね！*
</details>
<details><summary>$ \neg\neg\a \r \a$の証明</summary>
[1. Ax3] $ (\neg\neg\neg\neg\a \r \neg\neg\a)\r (\neg\a \r \neg\neg\neg\a) $
[2. Ax3] $ (\neg\a \r \neg\neg\neg\a) \r (\neg\neg\a \r \a) $
[3. 前述の定理] $ ((\neg\neg\neg\neg\a \r \neg\neg\a)\r (\neg\a \r \neg\neg\neg\a)) \r (((\neg\a \r \neg\neg\neg\a) \r (\neg\neg\a \r \a))\r((\neg\neg\neg\neg\a \r \neg\neg\a) \r (\neg\neg\a \r \a))) $
[4. MP(1.3.)] $ ((\neg\a \r \neg\neg\neg\a) \r (\neg\neg\a \r \a))\r((\neg\neg\neg\neg\a \r \neg\neg\a) \r (\neg\neg\a \r \a)) $
[5. MP(2.4.)] $ (\neg\neg\neg\neg\a \r \neg\neg\a) \r (\neg\neg\a \r \a) $
[6. Ax1] $ ((\neg\neg\neg\neg\a \r \neg\neg\a) \r (\neg\neg\a \r \a)) \r ( \neg\neg\a \r ((\neg\neg\neg\neg\a \r \neg\neg\a) \r (\neg\neg\a \r \a))) $
[7. MP(5.6.)]  $ \neg\neg\a \r ((\neg\neg\neg\neg\a \r \neg\neg\a) \r (\neg\neg\a \r \a)) $
[8. Ax2] $ (\neg\neg\a \r ((\neg\neg\neg\neg\a \r \neg\neg\a) \r (\neg\neg\a \r \a))) \r ((\neg\neg\a \r (\neg\neg\neg\neg\a \r \neg\neg\a))\r(\neg\neg\a \r (\neg\neg\a \r \a))) $
[9. MP(7.8.)] $ (\neg\neg\a \r (\neg\neg\neg\neg\a \r \neg\neg\a))\r(\neg\neg\a \r (\neg\neg\a \r \a)) $
[10. Ax1] $ \neg\neg\a \r (\neg\neg\neg\neg\a \r \neg\neg\a) $
[11. MP(9.10.)] $\neg\neg\a \r (\neg\neg\a \r \a)$
[12. Ax2] $(\neg\neg\a \r (\neg\neg\a \r \a)) \r ( (\neg\neg\a\r\neg\neg\a)\r (\neg\neg\a\r\a))$ 
[13. MP(11.12.)] $ (\neg\neg\a\r\neg\neg\a)\r (\neg\neg\a\r\a) $
[14. 前述の定理] $ \neg\neg\a\r\neg\neg\a $
[15. MP(13.14.)] $ \neg\neg\a\r\a $
*二重否定の消去。逆は、本定理とひとつのAx3を使えば、容易に示せる。*
</details>
*ここでいう証明とは、真理値表を書いて「成り立つね！」って示すことではなく、あくまで論理式の有限列として恒真式を導出すること。*

:point_up: **演繹定理**

## 無矛盾性

## 完全性定理

## コンパクト性定理