Language, Proof and Logic（言語・証明・論理）

引用

Barker-Plummer, D., Barwise, J., & Etchemendy, J. (2011). Language, Proof and Logic (2nd ed.). CSLI Publications.

章の要約

Language, Proof and Logic（LPL）は、ソフトウェアと一体になった教科書である。Tarski's World は一階の言語とその意味論を教え、Fitch は証明を組み立てて検査する自然演繹の環境、Boole は真理表を扱い、Submit は演習ファイルを自動採点のオンラインサービス Grade Grinder に送る。序論の後に3部19章が続き、多くの節には「（optional）」と明記されている。巻末には形式的証明規則のまとめ、用語集、ファイル・演習・一般の各索引がある。出版社によれば、第2版は初版を大幅に拡充・改訂したもので、数学的帰納法の扱いが拡大され（ペアノ帰納法と累積帰納法のソフトウェア対応も追加）、素朴集合論とツェルメロ＝フレンケル集合論の記述も改善された。

序論

合理的探究における論理学の特別な役割、なぜ人工言語を学ぶのか、帰結と証明についての節がある。続いて、目次で「必読」とされている宿題演習についての指示と、教員向けの注記が置かれている。

第I部：命題論理

第1〜2章：原子文、原子文の論理

第1章は個体定項、述語記号、原子文を導入し、関数記号、集合論と算術の一階言語、別の記法についての選択的な節を含む。第2章は妥当な論証と健全な論証を定義し、証明の方法と形式的証明を導入し、Fitch で証明を組み立てる方法と、帰結でないことを示す方法を説明する。

第3〜4章：ブール結合子、ブール結合子の論理

第3章は否定、連言、選言、文を評価するためのゲーム、曖昧さと括弧、同じことの言い換え、翻訳を扱う。第4章はトートロジーと論理的真理、トートロジー的同値・帰結と論理的同値・帰結を区別し、トートロジー的帰結を Fitch で扱う。否定を内側へ移す操作と、連言標準形・選言標準形についての選択的な節もある。

第5〜6章：ブール論理の証明法、形式的証明とブール論理

まず非形式的な証明として、妥当な推論ステップ、場合分けによる証明、背理法を扱う。第6章では、連言・選言・否定の導入規則と除去規則、下位証明の正しい使い方、証明を見つけるための戦略と戦術を示す。

第7〜8章：条件法、条件法の論理

実質条件法と双条件法、会話の含意、そして選択的に真理関数的完全性を扱う。第8章では、条件法についての非形式的・形式的な証明法、健全性と完全性についての選択的な節、第I部の復習演習が加わる。

第II部：量化子

第9〜11章：量化入門、量化子の論理、多重量化

第9章は変項、量化子記号、論理式と文、量化子の意味論、四つのアリストテレス的形式を導入し、複雑な名詞句の翻訳を練習する。第10章は一階の妥当性と帰結、ド・モルガンの法則を含む量化子の同値、公理的方法についての選択的な節、そして補題を扱う。第11章は量化子の混在、段階的な翻訳法、英語の言い換え、曖昧さと文脈依存性、冠頭標準形を扱う。

第12〜13章：量化子の証明法、形式的証明と量化子

まず非形式的な方法として、妥当な量化子ステップ、存在例化、一般条件証明、量化子が混在する証明を扱う。続いて Fitch における全称・存在の形式的規則、戦略と戦術、健全性と完全性についての選択的な節が来る。

第14章：量化についてさらに

数量的量化と数量的主張の証明、「the」「both」「neither」、一階論理への他の限定詞の追加、一般化量化子の論理、一階論理の表現力の限界を扱う。

第III部：応用とメタ理論

第15〜16章：一階集合論、数学的帰納法

第15章は素朴集合論を展開する。空集合、部分集合、共通部分と和集合、順序対、関係、関数を扱い、選択的な節としてべき集合、ラッセルのパラドックス、ツェルメロ＝フレンケル集合論がある。第16章は帰納的定義と帰納的証明、自然数上の帰納法、Fitch での帰納法を示し、自然数の公理化と強い帰納法についての選択的な節を含む。

第17〜19章：命題論理の発展的話題、一階論理の発展的話題、完全性と不完全性

第17章は命題論理の完全性を証明し、ホーン文と導出原理についての選択的な節を含む。第18章は一階の構造を定義し、真理と充足を見直し、一階論理の健全性を証明する。スコーレム化、単一化、導出原理についての選択的な節もある。第19章はヘンキン構成によって完全性定理を証明し、レーヴェンハイム＝スコーレムの定理とコンパクト性定理を扱い、ゲーデルの不完全性定理で締めくくる。

主要概念

第I部：命題論理

• 妥当性と健全性：論証は結論が前提から帰結するとき妥当であり、さらに前提が真であるとき健全である。
• トートロジー的帰結と論理的帰結：真理関数的結合子だけによる帰結と、より一般に意味による帰結との対比。
• フィッチ式自然演繹：導入規則と除去規則から組み立てられ、一時的な仮定のために下位証明を用いる形式的証明。
• 真理関数的完全性：ある結合子の集合がすべての真理関数を表現できるかどうか。

第II部：量化子

• 一階の妥当性と帰結：トートロジー的帰結を超えて、量化子と同一性の意味だけから帰結するもの。
• 翻訳：複雑な名詞句や量化子の混在を含む英語の文を、段階的に一階論理へ書き換えること。
• 存在例化と一般条件証明：形式的な量化子規則が写し取っている非形式的な推論パターン。
• 一般化量化子：「most」や「both」のような限定詞と、一階論理で表現できることの限界。

第III部：応用とメタ理論

• 数学的帰納法：自然数を含む、帰納的に定義された集合についての証明。
• 健全性と完全性：証明体系が妥当な帰結だけを、そしてそのすべてを証明できること。
• コンパクト性とレーヴェンハイム＝スコーレム：無限の文の集合とモデルの大きさについての、完全性から導かれる帰結。
• ゲーデルの不完全性定理：無矛盾な形式体系では算術のすべての真理を証明できないという限界。

批判的分析

長所

• 学習にソフトウェアが組み込まれている。 出版社によれば、パッケージのプログラムで学生は世界、真理表、証明を作ることができ、Grade Grinder が数百のコンピュータ演習をほぼ即座に採点する。学生はすぐにフィードバックを得られ、教員は機械的な採点作業から解放される。
• 非形式から形式へ。 目次では、各論理分野について、非形式的な証明法の章が形式的証明の章の前に置かれている（第5〜6章と第12〜13章）。学生は形式体系の中だけでなく、通常の数学的な文章で推論することも学ぶ。
• 選択的な内容が明示されている。 選択的な節は目次で明記されているので、授業では第I部と第II部の中核を進み、追加の内容を選ぶことができる。
• 初学者からメタ理論まで。 出版社は、論理学の予備知識を前提とせず、入門と二つ目の授業の両方に適していると述べている。Openproof のサイトは、第III部が完全性、コンパクト性、ゲーデルの定理にまで達するため、学部の最初の論理学の授業から大学院最初の授業まで使えるとしている。
• 翻訳と自然言語。 翻訳、英語の言い換え、会話の含意、一般化量化子にまとまった節が割かれており、証明だけでなく言語への著者たちの関心がうかがえる。

短所

• ソフトウェア・パッケージと結びついている。 本書の利点を十分に生かすには、パッケージに付属する登録IDが必要である。出版社は、登録IDは一度有効化すると譲渡できないとしているため、中古本ではウェブアプリや採点を利用できないことがある。
• 長く、密度が高い。 本書はおよそ600ページあり、第III部は最初の授業に必要な範囲を大きく超える。
• 一階論理のみ。 目次には様相論理、多値論理などの非古典論理は含まれていない。第14章で一階論理の表現力の限界は論じられるが、哲学の学生は様相論理のために別の教科書が必要になる。

コースにおける位置づけ

論理学のコースの中で、LPL はフィッチ式自然演繹を用いた形式論理入門の二冊のうちの一冊である。forall x: Calgary は、真理関数的論理と一階論理を同様の証明体系で扱う、無料でオープンライセンスの教科書である。より短く、ソフトウェアも不要なので、軽めに一通り学びたい学生に向いている。コピの Introduction to Logic は非形式的推論、三段論法、記号論理、帰納を一冊で扱うので、クリティカル・リーズニングの授業には LPL よりも適している。

LPL の後には、セオドア・サイダーの Logic for Philosophy が二つ目の授業として、命題論理と述語論理をより厳密に扱い、LPL が扱わない様相論理を加えてくれる。ブーロス、バージェス、ジェフリーの Computability and Logic は計算可能性と限界定理の完全な証明を展開する。出版社によればゲーデルの定理の概略で終わる LPL の第19章は、そこへの橋渡しとして役立つ。

本書の使い方

本書は論理学の予備知識を前提としない。演習に取りかかる前に、序論の宿題についての指示を読むこと。ソフトウェアと Grade Grinder は、演習の解き方と提出の方法の一部になっているからである。最初の授業では通常、第I部と第II部（第1〜14章）を扱う。このパッケージをもとに著者たちが作ったオンライン講座も、ちょうどこの最初の二つの部を14章で扱い、おおよそ週に1章のペースを勧めている。最初は、担当教員の指示がない限り選択的な節を飛ばしてよい。

非形式的な方法の章を、それに対応する形式的な章より先に学ぶこと。Fitch での証明に進む前に、Tarski's World を使って翻訳を具体的な世界に照らして確認するとよい。第III部は、二つ目の授業や、数学やコンピュータ科学に進む学生に向いている。集合論と帰納法を扱う第15〜16章は証明中心の数学全般へのよい準備となり、第17〜19章はメタ理論へと導く。演習の際は、巻末の形式的証明規則のまとめと用語集を参照資料として使うとよい。