数理論理学 I：学習計画

目的

数学のコースはどれも証明することを求め、哲学のコースはどれも論証することを求める。ところが、そのどれも推論そのものを対象とはせず、結論が前提から導かれるとはどういうことかを、わかりきったこととして扱う。このコースは、まさにその問いを主題とする。その目的は、論理学の最も単純な言語について、推論を対象とする最初の完全な数学的理論を、四つの部分がすべて見える形で構成することである。すなわち、論理式を認識でき曖昧さなく読める言語、記号の意味を顧みずに演繹を生み出す計算体系、各論理式にその変数の各付値のもとでの真理値を割り当てる意味、そして計算体系と意味が一致することの証明である。

そうであれば、このコースは記号を操作する規則の寄せ集めではなく、完全性定理という中心的な結果をもつ理論であり、それまでのすべてがその準備となる。論理式の集合 $\Gamma$ と論理式 $\varphi$ について、導出可能性 $\Gamma \vdash \varphi$ は、公理と規則によって構成され $\varphi$ で終わる論理式の有限列が存在することを述べる。意味論的帰結 $\Gamma \models \varphi$ は、$\Gamma$ の論理式を真にするどの付値も $\varphi$ を真にすることを述べる。二つの関係は相反する考えから生まれる。一方は構文的で存在的、他方は意味論的で全称的である。それにもかかわらず、このコースは $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$ を証明する。このことから、ある前提から何が導かれるかという問いには、どれも、より易しい側から答えられることが従う。演繹を示すこと、表をたどること、あるいは最後の内容の課が教えるように、融合法によって反駁することである。

対象者と前提知識

このコースは、数学、情報科学、哲学の学習を始める人、そして教育のどの段階にあっても、証明とは何か、なぜそれを信頼できるのかを正確に知りたい人を対象とする。大学の数学に入って証明につまずく学生、回路、プログラム、充足可能性問題の論理を必要とする情報科学の学生、論証の論理からその理論へと進みたい哲学の学生である。

これはレベル 1 のコースで、前提となるコースはなく、それだけで完結している。論理学を学んだこと、集合論を知っていること、定理を証明したことがあることを前提としない。集合（所属、包含、和集合、論理式の集合）、関数（付値は変数から $\{0, 1\}$ への関数である）、記号列、帰納法について用いることは、必要になる場所で教える。集合と記号列は第 1 単元の言語についての課で、帰納法はその次の課で、使う前に教える。前提とするのは二つのことだけである。注意深く読むこと（形式言語では、記号を一つ加えたり落としたりすると記号列が変わるからである）と、自然数の初歩的な算術である。自然数は、このコースでもサイトのほかの部分と同じく、$1$ から始まる。

このコースの行き先

以上のことから、サイトにおけるこのコースの位置が決まる。前提となるコースはなく、数学、情報科学、哲学の三つの課程の目標となっている。この三つのいずれにおいても、推論は道具であると同時に対象だからである。補完的なコースが三つあり、前でも並行でも後でも、どの順序でも学ぶことができる。アリストテレス論理学は名辞の論理と三段論法を学ぶ。三段論法の妥当性は、このコースが扱わない「すべての」や「ある」といった語に依存する。また、どのような伝統から計算体系に至ったかを示す。代数と幾何 Iはペアノの公理から演繹の体系を築き上げ、このコースが対象として研究する公理的方法と帰納法を、数について実地に用いる。その計画は、このコースを先に学ぶか並行して学ぶことを勧めている。最後に、C++ プログラミング Iは、ここで理論であるものを実践に移す。記号列が整論理式かどうかを判定すること、真理値表をたどること、標準形を計算すること、反駁を探すことは、どれもプログラムとして書ける手続きである。

ただし、このコースは表現力の問いを残したままにする。その言語は「すべての」も「ある」も言えず、日本語で述べられた論証の形式化は、第 1 単元から量化子を失う。したがって、予定されている続編は数理論理学 II であり、述語論理を扱う。そこでは同じ道を、量化子と対象を動く変数とともにたどる。健全性、完全性、コンパクト性は保たれ、その方法はこのコースが先取りしているが、意味論的帰結はもはや決定可能ではなくなる。

全体的な学習目標

以下の目標は、コースを修了した人ができるようになるべきことを記述する。各目標は観察可能な行為として定式化されており、具体的な課題で確かめることができる。内容の各課もまた、それぞれ固有の目標を掲げ、それらは一つまたは複数の全体目標に仕える。締めくくりの課は、各目標がどの単元とどの課で取り組まれるかを示す。七つの目標には、引用できるよう番号を付ける。

1. 目標 1. 対象言語とメタ言語を区別し、記号列が論理式であるかどうかを形成規則によって判定する。
2. 目標 2. 自然言語の言明と論証を形式化し、形式化が何を保ち何を失うかを指摘する。
3. 目標 3. コースの体系（ウカシェヴィチの公理、modus ponens、二重否定の置換）において、公理、原始規則、派生規則を組み合わせて演繹を構成する。
4. 目標 4. 自然数、論理式の複雑さ、演繹の長さに関する帰納法によってメタ定理を証明する。
5. 目標 5. 妥当性、充足可能性、意味論的帰結、意味論的同値を、真理値表と同値式によって判定する。
6. 目標 6. 論理式を標準形に変形し、それによって真理関数と回路を表す。
7. 目標 7. 健全性、完全性、コンパクト性を説明して適用し、充足不能性を融合法によって判定する。

目標 3 と目標 7 はそれぞれ自分の単元、すなわち演繹とメタ理論をもつ。目標 5 と目標 6 は意味論の単元を分け合い、前者はその前半、後者は後半にある。目標 2 には専用の課、すなわち形式化の課があり、その後も問題が言葉で述べられるたびに練習される。これに対して目標 1 と目標 4 は横断的である。言語の内部で言われることと言語について言われることの区別は四つの単元を貫き、帰納法は、論理式の一意読み取り可能性から体系の健全性とカルマーの補題に至るまで、コースの重要な証明すべての形である。このことから、その達成を一つの課に帰することはできず、コース全体を通じて養うのがよいことが従う。

コースの体系とその決定

命題論理のコースはさまざまな仕方で組み立てることができ、通常の教科書は、言語、原始結合子、演繹体系において互いに異なる。このコースは三つの決定を下しており、それらは初めから知っておくとよい。一見すると奇妙に見えるかもしれないことを説明してくれるからである。

白丸と黒丸の言語

コースの言語のアルファベットは、白丸 $\sigO$ と黒丸 $\sigI$ の二つの記号だけからなる。$n$ 番目の変数は $n$ 個の白丸に黒丸が一つ続く記号列 $v_{n} = \sigO^{n}\sigI$ であり、したがって $v_{1} = \sigO\sigI$、$v_{2} = \sigO\sigO\sigI$ である。形成規則は一つだけである。$\varphi$ と $\psi$ が論理式ならば、$\sigI\varphi\psi$ も論理式であり、これを $(\varphi \downarrow \psi)$ と略記して「$\varphi$ でも $\psi$ でもない」と読む。したがって否定論理和 $\downarrow$ が唯一の原始結合子であり、ほかの結合子はすべて一度だけ定義される略記である。$\neg\varphi$ は $(\varphi \downarrow \varphi)$ であり、選言 $(\varphi \vee \psi)$ は $\neg(\varphi \downarrow \psi)$ であり、これらから連言、含意、双条件、排他的選言が定義される。それらのほかの書き方はどれも証明される定理であって、定義ではない。

この選択には読みやすさという代償があり、コースはそれをメタ言語で支払う。白丸と黒丸の記号列を日常的に書く人はおらず、書くのはその略記名であり、それはいつでも、それが指す記号列にまで展開できる。ところが、この代償は何倍にもなって返ってくる。二つの記号で無限に多くの変数をまかなえるので、どの論理式も二つの要素からなるアルファベット上の有限の記号列である。結合子は引数の前に書かれるので、括弧は要らない。一意読み取り可能性は重みの議論で証明される。これは各変数に $+1$ を、結合子の黒丸それぞれに $-1$ を割り当てる。そして複合的な論理式はどれも否定論理和なので、複雑さに関する帰納法による証明はどれも複合の場合を一つしかもたず、これが後続の単元の証明をすべて短くする。一つの結合子でほかのどの結合子も表せることは前提とされない。意味論の単元がそれを証明する。

第二の原始規則

演繹体系はヤン・ウカシェヴィチの体系から出発する。否定と含意で書かれた三つの公理図式と、唯一の規則としての modus ponens である。これらの図式は、否定と含意を原始結合子とする言語のために定式化された。白丸と黒丸の言語では、$(v_{1} \downarrow v_{2})$ のような論理式は否定でも含意でもなく、公理にとっては不透明である。演繹の単元の最初の課は、すべての公理がもち、modus ponens が保ち、この論理式がもたない標識によって、ウカシェヴィチの体系が $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$ を演繹しないことを証明する。

そうであれば、体系を補わなければならない。自然な対処は二重否定 $\varphi \dashv\vdash \neg\neg\varphi$ を証明することに見える。二番目の課はこれを三つの図式から演繹する。標識は、それでは足りないことを示す。二重否定の定理は標識を保ち、それにもかかわらず、それらを使っても否定論理和の内部で $v_{1}$ を $\neg\neg v_{1}$ に置き換えることはできない。したがって二番目の課は、二重否定を証明したあとで、第二の原始規則、二重否定の置換を加える。論理式 $\chi$ から、その中の部分論理式 $\theta$ の一つの出現を $\neg\neg\theta$ に、あるいは $\neg\neg\theta$ の一つの出現を $\theta$ に置き換えて得られる論理式を推論する。こうして、コースの体系はウカシェヴィチの三つの図式、modus ponens、そしてこの規則からなる。

否定論理和のためのほかの体系は、それに合わせて作った公理図式で同じことを達成する。このコースが規則を選ぶ理由は二つある。modus ponens よりもさらに単純であること（一行だけをとり、一つの出現だけを変える）、そして人工的なところが何もないこと（二重否定がすでに述べていること、すなわち $\theta$ と $\neg\neg\theta$ が入れ替え可能であることを、論理式のあらゆる場所に広げたものを表している）である。そのうえ、この規則は健全である。各行の真理値を保つからである。また、証明に場合が一つ増えるだけで、演繹定理を保つ。この規則があれば演繹されるべきものがすべて演繹できるということが、最後の単元の完全性定理である。

強完全性の前にコンパクト性を

完全性には三つの段階がある。弱完全性は、すべてのトートロジーが定理であることを述べる。有限前提集合についての完全性は、有限の前提集合の意味論的帰結がどれもその集合から演繹されることを述べる。強完全性は、同じことが任意の集合、無限の集合についても成り立つことを述べる。コースの方法であるカルマーの補題は、論理式の有限個の変数と有限の前提を扱うので、最初の二つの段階には達するが、三つ目には達しない。そこに達するには、$\Gamma \models \varphi$ であるとき、ある有限の部分 $\Gamma_{0}$ で $\Gamma$ に含まれるものがすでに $\Gamma_{0} \models \varphi$ を満たせば十分である。ところが、それこそがコンパクト性定理の主張することである。

多くの教科書は、まず別の方法で強完全性を証明し、そこからコンパクト性を導く。これに対してこのコースでは、強完全性こそが求めるものであり、そこからコンパクト性を得るのは循環になる。そこで順序が逆になる。コンパクト性の課は、意味論の内部で、いかなる演繹にも触れずに、$v_{1}, v_{2}, \ldots$ の値を一つずつ固定してそれを証明し、そのあとで初めて、三行で強完全性、すなわち $\Gamma \models \varphi \Rightarrow \Gamma \vdash \varphi$ がすべての集合 $\Gamma$ について成り立つことを得る。

内容

コースは六つの単元からなる。この紹介、四つの内容の単元、そして締めくくりである。内容の各単元は導入の課で始まる。導入の課は単元の各課、コースにおける単元の位置、前提とする知識、単元が解決する問題を示し、導入テストから始まる。単元はまとめの課で閉じる。まとめの課は単元の演繹の連鎖を再構成し、それをコースのほかの部分と結びつけ、導入テストで問うた技能をまとめテストで繰り返し、各課の問題よりも難しい六つの挑戦課題を出す。

第 0 単元 コースの紹介

この課だけからなり、コースの目的、全体目標、決定、内容、学習量、設計を定める。

第 1 単元 言語

その目的は、コースが研究する言語を構成し、各論理式がただ一通りに読まれることを証明し、それを日本語の論証と結びつけることである。

1. 言語：導入。
2. 数理論理学とは何か：真理に対する妥当性、反例、パラドックス、対象言語とメタ言語の区別。
3. 命題論理の言語：集合と記号列、白丸と黒丸の言語、その形成規則と略記。
4. 自然数と論理式に関する帰納法：通常の帰納法、累積帰納法、構造帰納法、重みの補題、一意読み取り可能性、再帰的定義。
5. 自然言語の形式化：辞書、言明と論証の翻訳、実質含意が失うもの。
6. 言語：まとめと挑戦課題。

第 2 単元 演繹

その目的は、言語に計算体系、すなわちコースの体系を与え、その中で、数学が名前を付けずに使っている推論の形式を、それぞれ一度ずつ導くことである。

1. 演繹：導入。
2. 形式的演繹体系：ウカシェヴィチの体系、前提からの演繹、演繹定理、その限界を示す標識。
3. 四つの演繹技法：仮言三段論法、前提の交換、二重否定、対偶、二重否定の置換。
4. 結合子の対称性：否定論理和の基本補題、同値なものの置換、結合子の別の形、その五つの対称性。
5. 古典論理の技法：各結合子の規則、排中律、場合分けによる証明、背理法（いずれも前提つき）。
6. ド・モルガンの法則と分配法則：両方向の証明と、ほかの論理式の内部での同値なものの置換。
7. 演繹：まとめと挑戦課題。

第 3 単元 意味論

その目的は、論理式に意味を与え、それによって妥当性と意味論的帰結を判定し、すべての論理式を標準形に帰着させることである。

1. 意味論：導入。
2. 命題論理の意味論：付値とその再帰による拡張、一致補題、真理値表、妥当性と充足可能性。
3. 意味論的帰結と同値：集合からの意味論的帰結、意味論的演繹定理、置換と一様代入。
4. 一般化されたド・モルガンの法則と分配法則：$n$ 項の連言と選言とその法則を、帰納法によって。
5. 関数的完全性：どの真理関数にも論理式があること、否定論理和だけで足りること、十分な結合子の集合。
6. 標準形：リテラル、節、選言標準形と連言標準形、その双対性と存在。
7. 標準形のアルゴリズムとその応用：正しく必ず停止するアルゴリズムと、スイッチ回路の設計と簡単化。
8. 意味論：まとめと挑戦課題。

第 4 単元 メタ理論

その目的は、演繹と意味論的帰結が一致することを、まず有限の前提について、次に任意の前提について証明し、それらを判定する第三の方法を示すことである。

1. メタ理論：導入。
2. 健全性と完全性：行に関する帰納法による健全性、無矛盾性、カルマーの補題、弱完全性と有限前提集合についての完全性。
3. コンパクト性定理：その意味論的証明、同値な形、そこから従う強完全性、組合せ論への応用。
4. 融合法：節形式、融合規則、その健全性と反駁完全性、その計算量。
5. メタ理論：まとめと挑戦課題。

第 5 単元 コースのまとめ

課数理論理学 I：最終総括だけからなる。この課は七つの全体目標を振り返り、各目標がどの単元とどの課で取り組まれるかを図で示し、まとめテストの最初の解答を目標ごとに集め、学習がどこへ続くかを示す。

学習量と単位

コースの学習量は講義時間では測らない。非同期のコースには講義時間がないからである。測るのは学ぶ人の作業の総量、すなわち読むこと、証明と演繹をたどること、問題を解くこと、復習することである。見積もりは、サイトのすべてのコースで同じ方法による。各課の本文を一分あたり百語で読む時間（論理式は一つを一語と数える）、例題一題につき二十分、演習問題一題につき三十五分、挑戦課題一題につき四十五分、導入テストまたはまとめテスト一回につき十二分を数え、復習のために一割の余裕を加える。

結果

コースの各課は全体で、例題 $90$ 題、演習問題 $90$ 題、挑戦課題 $24$ 題を含み、そのほかに単元テストが八回ある。単元ごとの見積もり学習量は、時間単位に丸めると次のとおりである。

• 第 0 単元、コースの紹介：$1$ 時間未満。
• 第 1 単元、言語：$30$ 時間。
• 第 2 単元、演繹：$36$ 時間。
• 第 3 単元、意味論：$43$ 時間。
• 第 4 単元、メタ理論：$25$ 時間。
• 第 5 単元、コースのまとめ：$1$ 時間未満。

合計はおよそ $137$ 時間の学習である。この数字は、あるがままに読むべきである。すなわち、すべての証明を学び、すべての問題と挑戦課題を解く人についての見積もりである。すでに論理学を学んだ人や、挑戦課題に取り組まず演習問題にとどめる人は、かなり少ない時間で済む。定理を一度も証明したことのない人は、より多くの時間を要するかもしれない。特に演繹と意味論の単元で、これらは最も分量の多い単元でもある。

ただし、この数字は名目上のものである。コースの単位はこの数字で決まり、一定の速さで読むこと、挑戦課題一題に四十五分をかけることを前提とする。実際の受講者で測定されるまでは、現実的な幅を添えておくのがよい。各演繹を紙と鉛筆で書き写し、白丸と黒丸の記号列を一つずつ手で分解するときのように読む速さが想定の半分になり、挑戦課題一題に四十五分ではなく七十五分かかるとすれば、同じ方法でおよそ $174$ 時間になる。したがって、見込まれる学習量はおよそ $137$ 時間からおよそ $174$ 時間の間にある。上限は慎重な見積もりであって測定値ではない。この幅は、受講者が実際にかける時間がわかった時点で修正し、それまでは名目上の数字で単位を計算する。

推奨するペース

ペースを呼び分けるため、この計画はサイトのほかの計画と同じ基準を使う。フルタイムとは $60$ 単位の学年、すなわちおよそ四十週にわたるおよそ $1650$ 時間、つまり週におよそ $40$ 時間であり、パートタイムはその半分、週におよそ $20$ 時間である。ここから、推奨するペースは十六週の一学期で、週におよそ $8$ 時間か $9$ 時間、フルタイムの五分の一をやや上回る。現実的な幅をとれば、週 $9$ 時間から $11$ 時間である。この学期は代数と幾何 Iと分け合うことができる。そのコースの証明は、演繹がすでになじみの対象になっているときのほうが読みやすい。

集中的なペース、週におよそ $20$ 時間、つまりパートタイムでは、七週でコースを終えることができる。よりゆったりしたペース、週におよそ $4$ 時間か $5$ 時間では、二学期にわたり、それはほぼ半分ずつに分かれる。第 0 単元から第 2 単元、すなわち言語と演繹がおよそ $67$ 時間、第 3 単元から第 5 単元、すなわち意味論、メタ理論、まとめがおよそ $69$ 時間を占める。

互換単位への換算

互換単位の制度は、コースを対面授業の時間ではなく、コースが受講者に求める作業の総量で測る。ある機関で修めた学業を別の機関で認定できるようにするためである。欧州単位互換累積制度は、ボローニャ宣言を受けて欧州の大学が採用したもので、フルタイムの一学年に $60$ 単位を割り当て、一単位を $25$ 時間から $30$ 時間の学習と定める。チリの互換単位制度は、チリの大学が同様の設計で採用したもので、やはり一学年に $60$ 単位を割り当て、一単位を $24$ 時間から $31$ 時間の学習と定める。

さて、見積もった $137$ 時間をそれぞれの区間の両端で割ると、コースはおよそ $5$ 欧州単位（4.6 から 5.5）、$4$ から $6$ のチリ互換単位（4.4 から 5.7）に相当する。両区間の中央値である一単位あたり 27.5 時間を基準にとると、どちらの制度でも同じ数 4.98 が得られ、これを丸めて 5 とする。欧州単位については、単位数 $C$ は次のように挟まれる。

したがって、このコースには欧州単位 $5$ 単位とチリ互換単位 $5$ 単位を割り当てることを推奨する。これはフルタイムの一学年の十二分の一であり、通常の六単位の一学期科目をやや下回る。

コースの設計

形態

コースは非同期、オンライン、自分のペースで進めるものである。日程もライブ授業も締め切りもなく、受講者はそれぞれの準備と時間が許す速さで進む。コースはサイトの十四の言語で提供され、どの言語でも論理は同じである。論理式、演繹、証明の各段階はどの版でも同一で、訳されるのは本文だけである。各課は、先に学んでおくとよいほかの課を示すので、推奨される順序は明示されている。

一つの課の構成

内容を扱う課はすべて同じ構成をとる。まず概要と、観察可能な行為として定式化した固有の学習目標の一覧がある。続いて理論があり、定義、正確に述べられた結果とその証明、そして例からなる。証明はステップ再生器として示される。各ステップは一行を書き、変わる部分を強調し、先の結果に依拠するときはその結果に立ち返る。体系の演繹は番号付きの行で書かれ、各行の根拠が右側に記される（公理、前提、使う行を添えた modus ponens、または派生規則）。進むにつれて、引用された行が強調される。課の最後には、段階を追った解答付きの例題が五題と、演習問題が五題ある。演習問題にはそれぞれ折りたたまれたヒントがあり、そのあとに最終的な答えが示される。証明を求める演習問題には、答えのあとに折りたたまれた詳しい解答が加わる。これは自分の解答を書き上げてから開くのがよい。

さらに、各課はサイトの読み上げ機能で音声として聞くことができる。読み上げ機能は論理式の記号を言葉で発音し、白丸、黒丸、演繹と意味論的帰結の記号も読む。

評価

このコースは採点しない。その評価は形成的なもので、自己評価に基づく。演習問題によって各課の目標の達成を、挑戦課題によって各単元の目標の達成を確かめることができる。これに単元テストが加わる。導入テストは導入の課の初めにあり、出発点を十一問から十五問で測る。単元の問いに、単元が前提とする知識についての問いをいくつか加えるからである。まとめテストはまとめの課で挑戦課題の前にあり、達成したことを十二問で測り、導入テストと比較される。どちらもブラウザの中で採点され、各解答に説明と、復習するとよい課への案内が付く。その結果は解答した人のブラウザにだけ保存され、最終総括は各まとめテストの最初の解答を、全体目標ごとの概観にまとめる。

このコースの学び方

コースは順に学ぶように作られている。各単元はそれより前の単元を前提とする。演繹は最初の単元の言語で書かれ、意味論はその論理式に値を与え、メタ理論は二番目の単元と三番目の単元を比べる。課を一つ飛ばすと、遅かれ早かれそこへ戻らざるをえなくなる。

各課では、まず概要と目標を読むのがよい。次に紙と鉛筆で理論を学び、白丸と黒丸の記号列を書き写し、その変数と黒丸を区切り、再生器が書く前に演繹の各行を予想する。例題は解答を見る前に試み、演習問題は助けを借りずに解き、ヒントは試みが尽きたときにだけ開く。試みる前に答えを見てしまった問題は、解いたのではなく、読んだのである。

最後に、各主張がどの水準のものかを常に区別するのがよい。言語の内部で何かを述べているのか（論理式のように）、それとも言語について何かを述べているのか（$\Gamma \vdash \varphi$ や $\Gamma \models \varphi$ のように）。この区別はコースの目標の第一であり、またコースの中心的な結果を理解することを可能にするものでもある。その結果はメタ言語でしか述べることができない。