「まえがき」から引用する：
数理論理学は数学のひとつの分野で論理，特に数学における論理を研究対象としています． 本書は数理論理学の基本結果であるゲーデルの完全性定理，ゲーデルの不完全性定理，ゲンツェンの LK のカット除去定理， 直観主義論理のクリプキモデルに対する完全性定理などをわかりやすくかつ正確に説明することを目指した入門書です．（後略）
要再読である。
第１章は「証明を対象にするとは」という表題である。p.12 以降では導出図の実例について解説されている。まず、証明の実例を pp.1-2 にしたがってみてみよう。 15 年前の 10 月 10 日の朝に雨が降っていなかったことの証明である。この証明を（ア）とする。
その日は運動会が実行された（日付け入りの記念品が証拠として残っている）． ところで運動会は「当日の朝に雨が降っていたら中止」という条件で企画されていた（運動会実施要項が証拠書類として残っている）． したがってその日の朝には雨が降っていなかった．
さて、自然演繹の方法で一定の形式で証明を写し取ったものを導出図と呼ぶ。この証明の導出図は次のとおりである。
\[\Infer{}{\Infer{(ここで仮定①を解消)}{⑥\ \lnot \B}{⑤\ \bot} }{\Infer{}{③\ \lnot \A}{②\ \B \ra \lnot \A \AND ①\ \B (一時的な仮定)} \AND ④\ \A }\]
この導出図を（ア#）とする。どのようにして、導出図（ア#）は、文章による証明（ア）を写し取ったのか。pp.12-13 を見て整理する。
ここで、\( \A \) は、「その日に運動会が実行された」という命題であり、\( \B \) は「その日の朝に雨が降っていた」という命題である。 これらの命題を導出図に従って読むと次のようになる。
①その日の朝に雨が降っていたと仮定する． すると②「雨が降っていたら運動会は中止」という前提と合わせて， ③「運動会は中止」ということになる． これは④「運動会は実行された」という前提と合わせると，⑤矛盾する． したがって仮定が偽であった，すなわち ⑥「その日の朝に雨が降っていなかった」と結論付けられる（①～⑥は導出図中の対応する場所を示している）．
導出図は、MathJax の（というより LaTeX の）連分数の書式を使えば、本書のレイアウトと同じようにできる。
第２章は「自然演繹」である。p.29 には図 2.2 では自然演繹の推論規則一覧がある。
\[ \Infer{[\land 導入]}{ \varphi \land \psi}{\varphi \AND \psi} \]\[ \Infer{[\land 除去]}{ \varphi }{\varphi \land \psi} \]\[ \Infer{[\land 除去]}{ \psi }{\varphi \land \psi} \]\[ \Infer{[\lor 導入]}{ \varphi \lor \psi}{\varphi} \]\[ \Infer{[\lor 導入]}{ \varphi \lor \psi}{\psi} \]\[ \Infer{[\lor 除去] \mathcal{A} 中に仮定 \varphi や \mathcal{B} 中に仮定 \psi があればここで解消．}{\rho}{{\begin{matrix} {} \\ \varphi \land \psi \end{matrix}} \AND {\begin{matrix} \vdots & (\mathcal{A}) \\ \rho & \end{matrix}} \AND {\begin{matrix} \vdots & (\mathcal{B}) \\ \rho & \end{matrix}}} \]\[ \Infer{[\ra 導入] \mathcal{A} 中に仮定 \varphi があればここで解消．}{\varphi \ra \psi}{{\begin{matrix} \vdots & (\mathcal{A}) \\ \psi & \end{matrix}}} \]\[ \Infer{[\ra 除去]}{ \phi}{\varphi \ra \psi \AND \varphi} \]\[ \Infer{[\lnot 導入] \mathcal{A} 中にある仮定 \varphi をここで解消．}{\lnot \varphi}{{\begin{matrix} \vdots & (\mathcal{A}) \\ \bot & \end{matrix}}} \]\[ \Infer{[\lnot 除去]}{ \bot}{\lnot \varphi \AND \varphi} \]\[ \Infer{[背理法] \mathcal{A} 中にある仮定 \lnot \varphi をここで解消．}{\varphi}{{\begin{matrix} \vdots & (\mathcal{A}) \\ \bot & \end{matrix}}} \]\[ \Infer{[矛盾]}{ \varphi }{\bot} \]\[ \Infer{[ \forall 導入] （注 1）}{\forall x \varphi}{ \varphi[y/x]} \]\[ \Infer{[ \forall 除去] （注 2）}{\varphi[t/x]}{ \forall x \varphi} \]\[ \Infer{[ \exists 導入] （注 2）}{\exists x \varphi}{ \varphi[t/x]} \]\[ \Infer{[\exists 除去] \mathcal{A} 中に仮定 \varphi[y/x] があればここで解消．(注 3)}{\psi}{{\begin{matrix} {} \\ \exists x \varphi \end{matrix}} \AND {\begin{matrix} \vdots & (\mathcal{A}) \\ \psi & \end{matrix}} } \]\[ \Infer{[等号公理] (注 4)}{t = t}{} \]\[ \Infer{[統合規則](注 5)}{ \varphi[s/x] }{\varphi[t/x] \AND t=s} \]（注１） \( x \) は変数記号．\( y \) は \( \mathcal{A} \) 中の解消されていない仮定の中にも \(\forall x \varphi \)の中にも自由出現しない変数記号で，\(\varphi\) 中の \(x\) に代入可能なもの．
（注２）\( x \) は変数記号．\( t \) は \( \varphi \) 中の \( x \) に代入可能な項．
（注３）\( x \) は変数記号．\( y \) は \( \mathcal{A} \) 中の \(\varphi[y/x]\) 以外の解消されていない仮定の中にも \(\exists x \varphi \) や \(\psi\) の中にも自由出現しない変数記号で，\(\varphi\) 中の \(x\) に代入可能なもの．
（注４）\( t \) は項．
（注５）\( x \) は変数記号．\( t, s \) は \( \varphi \) 中の \( x \) に代入可能な項．
なかなか難しい。
このページの数式は MathJax4 で記述している。
| 書名 | 数理論理学 |
| 著者 | 鹿島亮 |
| 発行日 | 2009 年 10 月 25 日（初版第１刷） |
| 発行元 | 朝倉書店 |
| 定価 | 3300 円（本体） |
| サイズ | A5版 ページ |
| ISBN | 978-4-254-11765-3 |
| その他 | 川口市立図書館にて借りて読む |
まりんきょ学問所 ＞ 数学の部屋 ＞ 数学の本 ＞ 鹿島亮：数理論理学
