出版書誌データベース

---------
ある島にはAさんとBさんの二人の住人がいます。
一方が正直者であり，他方は嘘つきです。
ここで，Aさんは次のように言いました。
「Bさんと私の少なくとも一人は嘘つきだ。」
---------
さて，Aさんは正直者ですか，またBさんはどうでしょうか？

次のパズルは，ジョージ・ルーカスが製作総指揮した映画（Labyrinth）で使われた問題です。
---------
ここに左右二つの扉があり，それぞれに門番がついています。
一方は正直者であり，他方は嘘つきです。
左右の扉のうち一つだけが城に通じています。
門番一人に一つの質問をして，どの扉が城に至るのかを聞き出してください。
映画の主人公サラは，一人の門番にある質問を尋ねました。
どのような質問でしょうか？
---------
質問に対する回答を確認後，”前とは違って賢くなったみたい”と話しながら，サラは一つの扉を開けます。

形式的ではない論理的思考のための題材として，スマリヤンの論理学の本にはこのようなパズルが収められています。そこでは，社会学と論理学に興味を持っている人類学者アバクロンビーの冒険が続くことになります。しかしこのような問題を真面目に自然言語で考えていると，目が回りそうになります。私は実際に目がまわってしまいました ^^;　

そう言えば中学生の時に，リンゴやミカンの個数を求める問題で，変数を使って式をたてました。そして，式を計算して解くことで個数を求めました。これと同じ様に式を使って表現して，これらのパズルの答えを求めることはできないでしょうか？

本書で言っている記号化・形式化とは，このような式（論理式）を使って物事を表現することを意味しています。この種のパズルの解法では，大まかには二つの方法が考えられます。

一つは，推論規則を使って答えを導出する方法です（証明論的手法）。もう一つは，真理値と呼ばれる式の値を計算する方法です（意味論的手法）。全く異なるこれら二つの手法の関係を理解することが本書の大きな目標です（ゲーデルの完全性定理）。

さらに，証明も同様に式（ラムダ式）として表現されることを学びます。これによって，証明をプログラムと考えることができて，論理式をプログラムの型（タイプ）と解釈することができます。このような考え方に基づくと，高校で勉強した数学的帰納法の証明から再帰的プログラムが得られることになります。論理とプログラミング言語の親密な関係（カリー・ハワード同型）についても習得することができます。

1.　準備
言葉づかいについて：集合，順序と同値関係，写像と関数
2.　命題論理
2.1　日常的推論と記号化
2.2　数理パズルと記号化
2.2.1　スマリヤン流のパズル
2.2.2　不思議の国のパズル
2.2.3　スマリヤン流パズル再考
2.2.4　パズルランドのアリス
2.2.5　同値式の代数的性質
2.2.6　映画Labyrinthのパズル
2.2.7　ジョージ・ブーロスの最強のパズル
2.3　命題論理の言語：論理式
2.4　命題論理の意味論
2.4.1　論理式の値：真理値
2.4.2　恒真（トートロジー），充足可能，充足不可能
2.4.3　意味論的同値関係
2.4.4　意味論的帰結Γ|=A
2.5　ブール代数
2.6　ブール関数
2.7　命題論理の形式的体系
2.7.1　自然演繹の体系NJとNK
2.7.2　古典論理と直観主義論理：埋め込み
2.8　形式的体系の健全性と完全性
2.8.1　NKの健全性
2.8.2　NKの完全性
3.　述語論理
3.1　数理パズルと述語論理による記号化
3.1.1　だれがヒゲを剃るか？
3.1.2　スマリヤン流パズル述語論理版
3.1.3　TiffanyDuneau:SolvinglogicalpuzzlesinDisCoCircにおけるスマリヤン流パズル
3.1.4　関数の連続性の定義
3.1.5　言葉づかいについての復習
3.2　述語論理の言語
3.3　述語論理の形式的体系
3.3.1　自然演繹の体系NKとNJ
3.3.2　述語論理におけるグリベンコの定理：埋め込み
3.4　述語論理の意味論
3.4.1　構造と解釈
3.4.2　NKの健全性
3.4.3　NKの完全性：シーケントの分解と反例の構成
4.　証明の形式化とラムダ計算
4.1　証明図の簡約
4.2　証明の記号化・形式化
4.2.1　ラムダ記法：関数と値の区別
4.2.2　ラムダ項（ラムダ式）
4.2.3　ベータ変換
4.2.4　チャーチ・ロッサーの定理
4.2.5　型付きラムダ計算：型推論
4.2.6　型付きラムダ項とベータ変換
4.3　カリー・ハワード同型
4.3.1　論理式と型
4.3.2　証明図の簡約とベータ変換，CPS変換と埋め込み
4.3.3　古典論理の証明項：ラムダ・ミュー計算
引用・参考文献
索引