論理学をつくる 第3部-論理をもう一つの目で見る 読書メモ

論理学をつくる 第3部-論理をもう一つの目で見る 読書メモ

論理学は、人間が考える方法や議論の方法について研究する学問分野であり、特に、命題や推論に関する基本的な概念を扱うものとなる。

論理学の基本的な概念として、命題や命題論理、論理学の記号体系などがある。命題とは、真偽が決まる文句であり、真か偽かが確定するものとなる。命題論理は、命題を扱う論理学の分野であり、論理的な関係を表すための論理演算子が用いられる。論理学の記号体系は、論理的な演算を表すための記号を定めた体系であり、命題論理においては「否定」「論理積」「論理和」などの論理演算子が用いられる。

論理学には、命題論理以外にも、一階述語論理や高階論理などの分野もある。一階述語論理は、命題論理に述語や変数を導入することで、より複雑な論理的な関係を表現することができるものとなる。高階論理は、集合や関数などの数学的概念を含む論理を扱うものとなる。

論理学には、命題の真偽を決定する方法や、正しい推論を行うための方法についても研究されている。例えば、命題の真偽を決定する方法として、真理値表や証明という方法がある。真理値表は、命題に対して全ての可能な真偽の組み合わせを試して、命題の真偽を決定する方法となる。証明は、命題が正しいことを示すための論理的な手順であり、公理や推論規則を用いて、命題の真偽を導き出す。

論理学は、哲学や数学、人工知能などの分野にも深く関わっている。哲学においては、論理学の概念を用いて論理的な議論を行い、数学においては、論理学を用いて数学的な命題を導出するための基礎的な体系を構築する。人工知能においては推論技術や知識情報処理技術のベースとなっている。

論理学のベースとなっている数学的理論としては、”集合論の概要と参考図書“に記載している集合論、”構造とアルゴリズムと関数“で述べている代数学、”形式言語と数理論理学“で述べている形式言語学や意味論等があり、そちらも参照のこと。

今回は数理論理学の著名な教科書である「論理学をつくる」より、読書メモを示す。

前回の第2部論理学を拡げるに続き、今回は第3部論理学をもう一つの目で見るの読書メモについて述べる。

第Ⅲ部　論理をもう1つの目で見る

第9章　自然演繹法を使いこなそう
9.1　自然演繹法をつくる

9.1.1 evaluationからconstructionへ
はじめに
「P→Q、Q→R、したがって、(R→S)→(P→S)」と言う論証は正しい
タブローを使って証明できる
タブローや真理表という手法は
あらかじめ与えられている論証について
それが妥当かどうかを判定するための 「評価手続き(evaluation procedure)」
ではP→Q、Q→Rから(R→S)→(P→S)を出すことはできるのか?
前提から結論を一歩一歩引き出して見せる
本章では、与えられた前提から、結論を実際に導くための手続きを作る
ゲンツェン(Gerhart Gentzen)が定式化し、フィッチ(Frederic B Fitch)が使いやすく整理した
手かがり
(1) P→Qとする(前提)
(2) Q→Rとする(前提)
(3) さて、いま仮にR→Sだとする(仮定)
(4) さらに、Pであるとする(仮定)
(5) (4)と(1)によりQである
(6) (2)と(5)によりRである
(7) (3)と(6)によりSである
(8) したがって、(4)のPという仮定のもとでSが導けたから、P→S
(9) したがって、(3)のR→Sという仮定の元でP→Sが導けたから、(R→S)→(P→S)である
(10) 以上より、P→QとQ→Rを前提として(R→S)→(P→S)を導くことができる
演繹という手続きを反省してみよう
(5)で(4)と(1)からQを導く
PとP→QからQが論理的に出てくる
P→Q、Q→R ⊨ (R→S)→(P→S)と言う事実と同レベルの事実
演繹という手続きは
すぐには論理的帰結関係がわからない式の間を もっと簡単で自明な論理的帰結関係で橋渡ししてやること
演繹の手続きが満たすべき条件
(a)その正当性が見てすぐわかる程度に自明であること
(b)やって良い移り行きと許されない移り行きとが明確に区別されていること
(c)できる限り許される移り行きのレパートリーが少数であること
演繹を行う際に、演繹を行う側がさらに仮定を増やしている
(3)と(4)
演繹の都合上こちらが勝手に追加した仮定は、演繹が終わるまでにどこかでキャンセルしないといけない
(8)と(9)
9.1.2 形式化への第一歩
演繹規則をきちんと定め、演繹全体を形式化して自然演繹法を作り上げる
導出線と前提棒
演繹を作る時には
それぞれの式がどの仮定のもとで出てきているのかを明確に示すような書き方を工夫しないといけない
一つの記述方法
(1) P→Q (前提) (2) Q→R (前提) (3) R→S (仮定) (1),(2) (4) P (仮定) (1),(2),(3) (5) Q (4)と(1)より　(1),(2),(3),(4) (6) R (2)と(5)より　(1),(2),(3),(4) (7) S (3)と(6)より　(1),(2),(3),(4) (8) P→S (4)と(7)より　(1),(2),(3) (9) (R→S)→(P→S) (3)と(8)より　(1),(2)
上述のグラフィカルな表現
垂直線を導出線(derivation line)
導出線によってなされる式の変形
(1),(2)を仮定しての導出
(1),(2),(3)を仮定しての導出
(1),(“),(3),(4)を仮定しての導出
それぞれの導出に対して新たに仮定がおかれている
R→SからP→Sを導く左から2本目の導出線
PからSを導く一番右の導出
より左側の導出でおいた仮定は、右の導出でも有効
表示方法の手直し
導出の依存関係と導出において生きている仮定
定義
導出Dが別の導出D’に依存している
⇔
Dの導出線から左に行く水平線がD’の導出線に交わる
例
D1はD2とD3に依存しており、D2はD3に依存している
D3から見て
D2,D1を「下位導出(sub derivation)」
D2を「一次下位導出」
D1を2次下位導出
定義
導出Dにおいて生きている仮定とは、以下のいずれか
(1)Dの全堤防の上に置かれている仮定
(2)Dが依存しているあらゆる導出の前提棒の上に書かれている仮定
9.1.3 演繹規則をたてる
演繹を行うために従うべき規則を明文化する
自然演繹法でのこうした規則
前提規則(premiss rule: Prem)
(1)導出を始める時導出線を書いてその前提棒の上にいくらでも論理式を書いて良い
(2)演繹の途中で新しい導出を始める時、導出線を書いてその前提棒の上に一つだけ論理式を書いて良い
繰り返し規則と復活規則
繰り返し規則(rule of repetition : Rep)
導出において、その導出の前提棒の上にある式を繰り返し書いて良い
復活規則(Rule of reiteration : Reit)
導出Dでは、それが依存している導出しておいた仮定(Dにおいて生きている仮定)を自由に使って良い
Dよりも左にある導出線上に並んでいる式を持ってきてDの中で使って良い
導出Dのどこにおいても、Dが依存している導出にすでに生じているいかなる論理式を書いても良い
復活規則を間違って適用するとえらいことになる
例
QからPを導いている部分は、PからPを導く導出に依存していないので
そこから出てくるPを復活させることはできない
9.1.4 →導入規則と→除去規則
→除去規則(→elimination : → elim)
例
4行目と5行目から6行目が出てくる
6行目と7行目から8行目が出てくる
8行目と9行目から10行目が出てくる
3ケ所の「?」で行われていることをどのような規則で書けば良いか?
→除去規則(→ elim)
A→BとAが同じ導出に出てきたら、Bをその導出の中に書き加えて良い
→導入規則(→ introduction : → intro)
「??」の箇所はどうか?
Pを仮定したらSが出てきたので、Pと言う仮定なしにP→Sと言って良い
→導入規則(→intro)
導出Dがその一部に前提AからBへの導出(Dの一次下位導出)を含んでいるならば
A→Bをその導出の次の項として加えても良い
BはAという仮定のもとで導出されているが
A→BはAと言う仮定なしに導出されている
Aを仮定してBが導けるなら、仮定AをキャンセルしてA→Bを導いても良い
最終的に
9.1.5 演繹の攻略法
タブローは規則を当てはめていけばいつでも結果が出る機械的方法
タブローが大きくなることを厭わなければ完全に機械的にできる
自然演繹は「〜から…を導け」と言う具合に出発点と終点が指定され、その間をつないでいかねばならない
どの式にどの規則をどういう順番に当てはめるか
どのような過程を新たに立てるのか
上記の選択を誤ると目的の式にたどり着くことはできない
自然演繹法による演繹の構成をかなり「誰にでもできる方法」に近づけることはできる
例
「P→(Q→R)からQ→(P→R)を導け」
攻略法:演繹の枠組みをまずつくれ
A1,..,AnからBの演繹が欲しいなら、 まずA1,…,Anを前提棒の上に縦に書き並べ、 導出線の一番下にBを書け
攻略法:→を目指すには
A→Bに達したいとき、 Aを前提とし、一番下にBが出てくるような導出を構成し、 →introによってA→Bを得るようにすると良い
1
2
攻略法: 復活はいつでもOK
ある論理式に達したいなら、 他の攻略法を試した後で、 それに役立ちそうな論理式をとにかく復活させて見ると良い
攻略法:除去はいつでもOK
除去規則が使えそうなときはとにかく使うべし
9.1.6 演繹・定理・証明
定義
(1)A1,…,AnからBの導出があって、 それが他のいかなる導出にも依存していないとき
それをA1,…,AnからのBの演繹(deduction of B from A1,…,An )という
(2) 練習問題64のように、一番左の導出線に前提棒のない演繹がある
これはP→(Q→P)がいかなる前提をもおかずに演繹できたことを示している
こうした前提のない演繹がある式をtheorem(定理)と言い、その演繹をproof(証明)という
Proof:ある規則(つまり推論規則)に従って並んでいる論理式の列
Theorem:その列の最後に並んでいる論理式
これに対して「メタ定理(metatheorem)」がある
論理式の集まり、論理式と論理式との関係等について現に成り立っているある事実を、メタ言語の日本語で述べたもの
その正しさをメタ言語の日本語といくつかの補助的な記号(⇔とか⊨⫤とか)を使って示したものが証明

9.2　他の結合子のための推論規則

9.2.1 Λの導入と除去
Λの除去規則(Λ elim)
AΛBが導出の一項目として現れているなら、 A、Bいずれもその同じ導出の項目として書き足して良い
Λの導入規則(Λ intro)
AとBいずれも同じ導出の項目として現れているなら AΛBをその導出の一項目として書き足して良い
攻略法:Λを目指すには
AΛBに至りたかったら、AとBそれぞれ別個に得るようにし、その後にΛintroを用いると良い
攻略法だけで演繹できちゃう?
(P→Q)Λ(R→S)から(PΛR)→(QΛS)への演繹
(1)まず演繹の枠組みを作れ
(2)→を目指すには
(PΛR)→(QΛS)を導くために、PΛRを仮定してQΛSを導く
(3)Λを目指すには
QΛSを導くためにはQとSをそれぞれ導けば良い
(4)復活はいつでもOK
QとSのどちらかを導くだが
「復活はいつでもOK」を使ってこれらを導く材料を手に入れる必要がある
ところが復活させることができるのは(P→Q)Λ(R→S)の一つだけ
それを復活させる
(5)除去はいつでもOK
Λを除去、PΛRからもΛを除去
(6)もう一度、除去は鉄でもOK
P→QとR→Sの→を除去
ちょっとは頭を使うべし
(PΛQ)→RからP→(Q→R)を導け
演繹の枠組みを作れ、→を目指すには
Rが出てくるためには、(PΛQ)→Rを使う そうするとPΛQが出てくれば→elimでRが出てくる
問題はPΛQをどうやって持ってくるか 前提にPもQもあるからこれを復活させてΛを導入すれば良い
9.2.2 ↔︎の導入と除去
↔︎導入規則(↔︎intro)
A→BとB→Aが一つの導出に一項目として現れていたら、
その導出にA↔︎Bを書き加えても良い
↔︎除去規則(↔︎elim)
A↔︎BとA(あるいはB)が導出に一項目として現れていたら、
その導出にもう片方B(あるいはA)を書き加えても良い
9.2.3 ¬の導入と除去
¬除去規則(¬elim)
¬¬Aが一つの導出に一項目として現れてきていたら
その導出にAを書き加えても良い
要するに2重否定は外しても良い
¬導入規則(¬intro)
導出DがAからの矛盾の導出を一項目として含んでいたら
¬AをDの一項目として書き加えて良い
つまり
Aと仮定すると矛盾が生じることがわかったら、Aでないと主張して良い
Aからの矛盾の導出
Aを仮定して始まる導出の中に、ある論理式とその否定の両方が出てくるようなもの
攻略法:¬を目指すには
¬Aに至るためには、Aから何らかの矛盾を導くようにせよ
例
P→Qから¬(PΛQ¬)を演繹せよ
(1)演繹の枠組みをまず作れ
(2)→を目指すには
PΛ¬Qを仮定して
何らかの矛盾(contradiction!)を導いて
¬導入規則により¬(PΛ¬Q)を得れば良い
(3)どんな矛盾を導くのか(復活と除去規則の利用)
矛盾の作り方についての攻略法
例
¬(PΛQ)を¬(P→Q)から演繹する
(1)従来の攻略法
(2)復活で出てきた¬(P↔︎Q)に対して P↔︎Qが得られれば矛盾が得られる
P↔︎Qを導く
(3)それぞれの下位導出で QとPをそれぞれ導出するために PΛQを復活させる
攻略法:矛盾の見つけ方
Aの仮定のもとで、矛盾を見つけたいが見つけられないとき
Aの周りにある論理式を見よ
もしそこに¬Bの形があったら、Bを得るよえにせよ
9.2.4 連言は簡単だったのに選言はややこしい
Ⅴ導入規則(Ⅴintro)
何が言えていればAⅤBを言って良いか
AかBがすでに言えているならAⅤBと言っても良い
AかBが同じ導出において以前に一項目として出てきているなら、AⅤBを書き加えても良い
攻略法:Ⅴを目指すには
AⅤBに到るためには、AかBのどちらかに達すれば良い
例
P→QからP→(Q→R)を演繹せよ
(1)演繹の枠組みをまず作れ
(2)→を目指すには
(3)
Ⅴ除去規則
問題なのはⅤの除去規則
AⅤBからⅤを除去してAやBを引き出すことはできない
なぜか
AⅤBは選言肢のうちどちらが成り立っているかということについて全く何も述べていない
結合子のⅤ除去規則は、AⅤBが言えているとして、そこからさらにどのようなことが言えるかを述べたもの
AⅤBだけからはこれ以上AとBについて何も出てこない
他の論理式の助けを借りる
Ⅴ除去規則(Ⅴelim)
AⅤB、A→C、B→Cがすでに同じ導出に出てきているなら、Cをその導出に書き加えて良い
AとBの2つの場合で、場合分けが尽くされていることがわかっており
どちらの場合をとってもCということが演繹できるものだったら
場合わけなしに常にCと言ってよい
この規則に対する攻略法
攻略法:Ⅴからスタートしたいなら
AⅤBという選言からCに至るためには
まずA→CとB→Cという2つの式を導け
例
P→QとR→Sから(PⅤR)→(QⅤS)を演繹せよ
(1)演繹の枠組みを作れ
(2) →を目指すには
(3)Ⅴからスタートしたなら
9.2.5 最後の手段としての間接証明
これまでの攻略法でうまくいかない場合の対応
攻略法:最後の手段は間接照明
Aに至りたいのに、その他の方法が全てダメだった時
まず¬Aを仮定において矛盾を導き
¬introで¬¬Aを得て
¬elimで2重否定を除去してAを得るという方法を試みよ
例
対偶法則の演繹
P→Qと¬Q→¬Pが互いに演繹できることを提示
(1)
(2)
(3)
(4)
排中律のproof
排中律PⅤ¬Pは間接証明を用いないとProofが作れない
(1)演繹の枠組みを作れ、最後の手段は間接証明
¬(PⅤ¬P)を仮定して、矛盾を導くことで¬¬(PⅤ¬P)を導いて、2重否定をおとす
(2) 矛盾の作り方
¬(PⅤ¬P)があるからPⅤ¬Pを出せば矛盾を導ける
(3) Ⅴを目指すには
PⅤ¬Pを出すには、「Ⅴを目指すには」を用いてPか¬Pを出せばよい
とりあえず¬Pを出すことにする
(4) ¬を目指すには
¬Pを出すには、「¬を目指すには」を用いて、Pを仮定して矛盾を導けばよい
(5) 矛盾の作り方
前提棒の下に¬(PⅤ¬P)があるから、PⅤ¬Pを出すことにする
前提にPがあるので、ⅤintroでPⅤ¬Pはすぐに手に入る

9.3　矛盾記号を導入した方がよいかも

9.3.1 超絶技巧の演繹?
ドモルガンの法則の半分、¬PΛ¬Qから¬(PΛQ)への演繹にチャレンジ
(1)
方針を立てる
(2)
PⅤQから矛盾を導く、「Vからスタートしたなら」に従う
(3)
Contradiction!はAと¬Aが同時に出てくることを表す
→introの規則を当てはめてP→contradictionを作ることはできない
(4)
Contradictionの部分を何らかの矛盾式にする必要がある
(5)
9.3.2 矛盾記号の導入
Contradiction!を一つの式のようにして扱って演繹をする
¬introの代わりに
¬intro*
¬elim*
上記の演繹の書き直し

9.4　述語論理への拡張

9.4.1 ∀除去規則と∃除去規則
述語論理にも自然演繹を拡張する
∀除去規則(∀elim)
| ∀𝛏A | | A[α/𝛏] ∃導入規則(∃intro)
| A[α/𝛏] | | ∃𝛏A
(1)∀xPxからPaΛPbの演繹
(2)Raaaから∃xRaxaの演繹
(3)∀x(Px→Qx)と∀x(Qx→Rx)からPa→Raの演繹
枠組み作りと→を目指すには
9.4.2 ∀導入規則
∀ 導入規則(∀ intro)
| A[α/𝛏] | | ∀𝛏A
いつでも使えるほけではない
但し書きが必要
∀は次のことを言っている
全てのものの代表として任意に選んだαについて
A[α/𝛏]であることがわかっているなら
全てのものについてそれを主張してよい
但し書きをどうすればよいか
どのような条件を∀導入規則に課したらよいのか
aがPであることと、全てのPがQであることから、アリとあらゆるものがQであるということは出てこない
(1)上記の演繹は禁止されなければならない
2行目のaは、∀x(Px→Qx)を満たす全てのものの代表として導入された任意のものではない
aはPを満たしている特定のもの
4行目のQaは、特定のaについてQaが成り立つと言っているに過ぎない
よって再び一般化はできない
(2)上記は良い
全てのものについて、Pということと、PならばQということが成り立つ
全てのものの代表として、任意にaを選んで3行目と4行目を導き
ここからQaが導出される
Qaのaは全てのものの代表として任意に選ばれたものの性格を失っていない
Aがどのようなものについてのそれ以上の情報が何もない
最後に一般化して∀xQxにできる
上記の違いはどこからくるか
∀を導入する段階で
(1)ではaがキャンセルされていない前提(premがついている式)の中に現れている
(2)ではaがキャンセルされていない前提の中には現れていない
∀introへの但し書き
ただし、αは規則を適用する段階までまだキャンセルされていない前提には現れないものとする
(3)正しい演繹
5行目で前提の中にaが現れている
この前提は最後の行でキャンセルされているので但し書に違反しない
(4)間違った演繹
キャンセルされない前提に現れる固定定項を一般化してしまう
10行目で∀を導入することが但し書きに違反している
もう一つの但し書き
∀導入規則にはもう一つ但し書きが必要
上記のような間違った演繹を防ぐため
「全ての人は自分を愛している」 から、 「全ての人がジョディーを愛している」ということは出てこない
上記の但し書きには違反していない
aはキャンセルされなていない前提に出てくるものではない
問題は3行目でLaaのaを一般化するときに一つだけ残したことにある
∀導入規則(∀intro)
| A[α/𝛏9] | | A𝛏A
ただし
(1) αは規則を適用する段階ではまだキャンセルされていない前提には現れないものとする
(2) αは∀𝛏Aの中に残ってはいけない
∀規則で一般化できる個体定項は、「任意のものについて然然のことが言えますよ」という情報だけ伝えて
その「任意のもの」を「全てのもの」に置き換えた(つまりそれが∀導入ということ)暁には、表舞台から全て消えるダミーである
攻略法:∀を目指すには
∀𝛏Aに至るためには、
A[α/𝛏]を導き、それに∀導入規則を適用せよ
ただし
Αは∀𝛏Aの中にある個体定項と、 ∀𝛏Aが得られる導出においてキャンセルされていない前提に出てくる個体定項以外の個体定項から 選ばなくてはいけない
9.4.3 ∃除去規則はさらに面倒
AVBという不特定の情報からはAとBについて確定的な情報はもう引き出せない
どれかわからないがとにかくしかじかなものがあるという不特定の情報から
それ以上何かの情報は引き出せない気がする
Ⅴの除去法則のアプローチ
AⅤBであるとき
AとBのどちらが成り立っているかわからないにしても
もし、 AであれBであれいずれにせよCということが言えるのだったら
Cという確定的なことを主張しても良い
同様に∃に対しても
Pなものがあるという
どれがそのPであるかわからないにしても
「どれがそのPであろうがなかろうがいずれにせよC」ということが言えるのなら
Cだと主張しても構わない
∃除去規則(∃elim)
使用例
7行目の∃xQxはあくまでもPaという前提のもとでだけ導出されたもの
8行目の∃xQxはPaを前提しないで導出されている
∃除去規則とは
Aなものがあるということがわかっているとする
このときAなものを仮にαと名付けて推論をしていったら、Cという事柄が導出されたとする
このときAなものをαと名付けたことを忘れて
Aなものがあるという情報からCという情報を引き出しても良い
例
どうもここの水を飲んだ人がいるらしい
その人を仮にヤストモとする
水銀汚染された水を飲んだ人は皆髪の毛から水銀が出てくるはず
ヤストモの頭髪から水銀が出てくるはず
髪の毛から水銀が検出される人が少なくとも一人はいるはず
但し書きを考えよう
上記の導入される名前「ヤストモ」(あるいは個体定項α)は 次の2つの性質を持っている
(1)それは∀導入の場合と似た 「任意のもの」である
ただし、∀導入の際の個体定項は文字通り任意のものであるが
∃除去の場合はAである限りにおいて任意のものである
(2)その個体定項はCという結論を引き出すための 仲立ちの働きをする替え玉に過ぎない
結論Cに伝わるのは「なんであれAなものがある」という情報だけ
そのAなものがどれであるかという情報は結論のCにおいて残ってはいけない
上記により個体定項αについていくつかの条件があることがわかる
まず(1)から次のことが言える
(a)αは「Aであるなにか」 という以上の情報を担ってはならない
だからαは∃除去の際にキャンセルされずに残っている前提の中に現れてはいけない
これは∀introと同様
(b)さらにαは∃𝛏Aの中にも現れてはならない
(c)αについての情報が結論Cの中に残ってはいけない
従ってαはCの中に現れてはいけない
(a)(b)(c)に違反すると上記のような間違いをする
∃除去規則の使用例
∃xPxから∃x(PxⅤQx)を演繹してみる
(1)建て付け
(2)
(3)
攻略法:∃からスタートしたなら
存在量化された式からスタートして目標となる式を導くにあたり
いったんその存在量化子を外さなければいけないと思われるとき
その目標となる式をゴールとするような下位導出を作って∃除去規則を適用することを試みよ
この攻略法の使用例
(1)上記のような演繹を行う
(2)
(3)
(4)
9.4.4 ド・モルガンの法則に挑む
∃x¬Pxから¬∀xPxを演繹する
∃x¬Pxから¬∀xPxを導く
(1)「∃からスタートしたなら」を適用して∃除去規則で目的の式を出す
(2) ¬∀xPxを導出するために、「¬を目指すには」を適用して∀xPxを仮定して矛盾を導く
(3) 復活させることのできる式を復活させる
¬∀xPxから∃x¬Pxを演繹する
(1)「演繹の枠組みを作れ」に従う
前提の¬∀で始まる式に直接当ては目ることのできる規則がない
(2)間接証明を導入する
(3)矛盾を作るために、復活できるものは復活させる
なんとかして∀xPxを導けば良い
(4) ∀xPxを導くために「∀を目指すには」により、任意の個体定項aについてPaを導いて、それに∀導入規則を当てはめる
(5)間接証明を利用(¬Paを仮定して毛潤を導く)
攻略法:¬∀、¬∃からスタートしたいなら
¬∀A、¬∃Aという形の式を直接に変形するような推論規則はない
従って、∀A、∃Aを導いてそれと矛盾させるという具合にこれらの式を丸ごと利用することを考えよ
そうなると、演繹が完成証明の形になる

9.5　同一性記号を含む自然演繹

=除去規則(=elim)
A(α/β)は式Aの中の個体定項βを (すべての箇所だけでなくても良い) 何箇所かで個体定項αに置き換えた式を表す
=導入規則(=intro)
α=αの形との式は演繹のどこの段階でもいかなる前提なしでもおいて構わない
こんな規則がなんの役に立つのか?
∀x(x=x)のproof
(1)
a=aをAと見立てて、そのうちの左側のaのところにa=bを代入している
(2)

第10章　シンタクスの視点から論理学のゴールに迫る
10.1　公理系という発想

10.1.1 論理的真理をすべてかぞえあげる
セマンティクスの立場では論理的真理を トートロジー(述語論理では妥当式)として捉えた
与えられた式がトートロジーであるかどうかは
真理表やタブローによって確かめられた
上式は一つ一つの式に対する確かめに過ぎない
「トートロジーはこれだけです」という具合に トートロジーの全体を把握することはできないのか?
トートロジーは無限にある
帰納的定義を用いて、無限のトートロジーを定義
そのための方法 「公理系(axiomatic system)
(1)出発点となる代表的なトートロジーをいくつか選ぶ
出発点となる式を「公理(axiom)」
(2)出発点に選んだトートロジーの代表から、 残りのトートロジーを全て作り出すための規則を立てる
規則を推論規則(rule 0f inference) あるいは変形規則(rule of transformation)
(3)以上の手続きによって得られる論理式は全てトートロジーであり しかもトートロジーは全て手続きよって尽くされていることを証明する
証明を「完全証明」
10.1.2 命題論理の公理系
命題論理の範囲内で 全てのトートロジーを捉えようとして考案されたもの
A1 P→(Q→P) A2 (P→(Q→R)→((P→Q)→(P→R)) A3 (P→(Q→R))→(Q→(P→R)) A4 (P→Q)→(¬Q→¬P) A5 ¬¬P→P A6 P→¬¬P R! AとA→BとからBを引き出して良い (分離規則:modus pones, 略してMP) R2 P1,…,Pnが原始式であるとする。このとき一つの式に出てくるP1,..,Pnを一斉に倫理式B1,…,Bnに置き換えて良い (代入則、置き換え則:rule of substition,略してRS)
フレーゲの公理系ではⅤ等の論理定項はなく限定されている
どうするのか?
D1 AΛB=df¬(A→¬B) D2 AⅤB=df¬A→B D3 A↔︎B=df(A→B)Λ(B→A)
PⅤ¬Pは¬P→¬Pの別の書き方になる
公理系APL(axiomatic system for propositional logic)
A1 A→(B→A) A2 (A→(B→C))→((A→B)→(A→C)) A3 (¬B→¬A)→((¬B→A)→B) R1 MP
ここにない論理定項は定義D1〜D3で導入されるものとする
公理そのものがA,Bなどの図式文字を使って書かれている
A1は一つの論理式ではなく、P→(Q→P)、(P→Q)→(R→(P→Q))などA→(B→A)の形をした無数の論理式を一括している
A1は「しかじかの形をした任意の論理式を公理とする」ということを言っている
A1からA3は公理図式(axiom schema)と呼ばれることもある
代入規則が入らなくなる
P→Pはトートロジーの一つだがAPLの小売には含まれていない
APLのいずれかの公理から推論規則を用いて適用して導かれる
(1) P→(P→P)→P) ….. A1 (2) (P→((P→P)→P))→((P→(P→P))→(P→P)) ……. A2 (3) (P→(P→P)) →(P→P) …….. (1)(2)からM`により (4) P→(P→P) ……. A1 (5) P→P ……. (3)(4)からMP
10.1.3 公理系に関して定義される諸概念
theoremとproof
公理系APLに対して、APLでのtheorem,proofということを次のように定義する
定義
(1) 以下の条件を満たす、論理式の有限個の列B1,B2,…,Bn (この最後のBnがCであるとする)を、CのAPLにおけるproof(証明)という
条件
Bi(ただし1≤I≤n)は、次のいずれかである
(a) APLの公理である
(b) 先行するBj,Bkから推論規則MPによって引き出された式である
(2) Cのproofが存在するとき、CはAPLのtheorem(定理)である。 またCはAPLにおいてprovable(証明可能)であるという
ここで定義したproofはある条件を満たす「論理式の列」のこと
Theoremはその列の最後にある「論理式そのもの」のこと
これまでの「定理25」とかその証明のような、「論理式の性質についてある事実を日本語で述べたもの」「その正しさを示すこととしての定理や証明」とは全く異なる
よって「theorem」とか{proof」とか表現する
公理からのproofの例
前述のP→Pの導出は、APLにおけるproofの条件を満たしている
APLのtheorem
(1) (P→(Q→R))→((P→Q)→(P→Q)) ………. A2 (2) ((P→(Q→R))→((P→Q)→(P→R)))→((Q→R)→((P→(Q→R))→((P→Q)→(P→R)))) …… A1 (3) (Q→R)→((P→(Q→R))→((P→Q)→(P→R))) ……… (1)(2)からMP (4) 以下省略
これから出てくる(P→Q)→((Q→R)→(P→R))はAPLのtheorem
公理系の健全性と完全性
公理系を作った狙いは全てのトートロジーを数え上げることにある
以下の2つが成り立たないといけない
(1)どんなトートロジーも上記の3つの形をした公理のククつかを出発点においてMPによって変形していくと出てくる
(2)そのようにして出てくる論理式はどれもトートロジーになっている
論理式AガAPLのトートロジーになっている ⇔ Aはトートロジーである
定義
論理式Aが公理系Kのtheoremである ⇒ Aはト-トロジーである が成り立つとき、公理系Kは「健全(sound)」であるという 逆に 論理式Aがトートロジーである ⇒ Aは公理系Kのtheoremである が成り立つとき、公理系Kは「完全(complete)」であるという
公理系が健全で完全であることをひっくるめて完全であるということもある
10.1.4 仮定からの演繹
いじってたら出た!
公理系は論理的帰結の概念のこれまでとは違った捉え方も与えてくれる
例:数学の問題
Sinθ+cosθ=√2とする。このときsin2θを求めよ
両辺をとにかく二乗する
sin2θ + 2sinθcosθ + cos2θ = 2
そういえば「sin2θ + cos2θ = 1」
代入する
1 + 2sinθcosθ = 2
2sinθcosθ=1
そういえば「2sinθcosθ = sin2θ」
代入する
sin2θ=1
答えは1
式の意味はわからないが
闇雲に変形していたら目指す答えが出た
ここでP→Pのproofを見直す
式の形だけを見ていてもproofは構成できる
「→」が「ならば」とか「A→B」の心理条件についての考慮はproofの構成には関係ない
Proofは、全く意味・真理無視の立場、つまりシンタックスの立場に立っている
仮定からの演繹
先ほどの数学の例
(1)出発点のsinθ+cosθ=√2 は問題で与えられた仮定となる式
この問題だけで成り立つと仮定される式
(2)その他のsin2θ+cos2θ=1と2sinθcosθ=sin2θはいわゆる「公式」
いつでも成り立つ式
どんな問題でも使って良い式
我々が普通「証明問題を解く」と呼んでいるものは
問題に与えられた特定の式(これを仮定と呼ぶ)から、目標となる式を導くということ
その時に、公式と呼ばれるいつでも使って良い式を導入して、目標となる式を導いている
与えられた特定の仮定から出発して目標となる式に たどりつく過程としての「証明」を公理系という道具を用いて捉え直す
これを「proof」ではなく「deduction(演繹)」と呼ぶ
先ほどの例
sinθ+cosθ=√2からsin2θ=1への演繹
この途中で2つの公式を使う(論理学では公理)
定義
(1)Γを論理式の集合とする、 この時以下の条件を満たす、論理式の有限個の列B1,B2,…,Bn(BnはCである)を、 公理系APLにおける仮定ΓからCへのdeduction(演繹)という
条件
Bi(ただし1≤I≤n)は次のいずれかである
(1) APLの公理である
(2)Γの要素である
(3)先行するBj,Bkから推論規則MPによって引き起こされた式である
(2)ΓからCへの演繹が存在する時、 CはΓからdeduceされる。 またはdeducible(演繹可能)といい、 Γ⊢Cと書く
⊢:ターンスタイル
「ΓからCが論理的に出てくる」という概念を論理学的に緻密化して捉えたもの
2重ターンスタイル「⊨」と似ているが、両者は全く異なる
Deductionもある条件を満たした論理式の列に他ならない
仮定からのdeductionの例
P→Q、P→(Q→R) ⊢ P→Rであることを示す
(1) P→Q …….. 仮定 (2) P→(Q→R) ……. 仮定 (3) (P→(Q→R))→((P→Q)→(P→R)) ……. A2 (4) (P→Q)→(P→R) ……. (2)(3)MP (5) P→R …… (1)(4)MP
P→Q、O→R、P⊢Rであることを示す
(1) P→Q ….. 仮定 (2) P ……. 仮定 (3) Q ……. (1)(2)MP (4) Q→R …… 仮定 (5) R …… (3)(4)仮定
proofはdeductionの特殊ケースである
両者の違い
Deductionでは小売以外に幾つかの式を仮定としておいてスタートする
Proofでは公理だけが使われる
Proofは0個の仮定から出発したdeductionの特殊ケース
Γ⊢CにおいてΓが空集合の時がproof
よって
Cがtheoremであることを「⊢C」と書く
deductionの持つ性質
Γからのdeductionに対して以下のことが成り立つ
定理37
(1) A∈Γ ⇒　Γ⊢A (2) Γ⊢AかつΓ⊆Δ ⇒ Δ⊢A (3) Γ⊢A ⇒ Γ’⊆Γとなる適当な有限集合Γ’があって、Γ’⊢A (4) ⊢A ⇒　Γ⊢A (5) Γ⊢AかつΓ⊢A→B ⇒ Γ⊢B (6) {Γ⊢AかつΓに含まれる全ての論理式BについてΔ⊢B} ⇒ Δ⊢A (7) {Γ⊢AかつΔ,A⊢B} ⇒ Γ,A⊢B
10.1.5 演繹定理
以上で定義された「⊢」については、次の事実が成り立つ
定理38:演繹定理(deduction theorem)
Γ,A⊢C ⇔ Γ⊢A→C
演繹定理は便利
推移律(P→Q)→((Q→R)→(P→R))のproofを作るのは大変
演繹定理を繰り返して使うと
⊢(P→Q)→((Q→R)→(P→R))
P→Q⊢(Q→R)→(P→R)
P→Q, Q→R⊢P→R
P→Q, Q→R, P⊢R
P→Q, Q→R,Pを仮定したRへのdeductionが あることを示しておけば
(P→Q)→((Q→R)→(P→R))のproofが存在することが言える
演繹定理の証明
Γ,A⊢C ⇒ Γ⊢A→Cの方向を証明する
10.1.6 deduction中でのtheoremの利用と派生規則
一度proofの存在を示したtheoremは図式として使おう
例
2重否定則(⊢¬¬P→P)を示す
演繹定理により
¬¬P⊢Pを示せば良い
(1) ¬¬P ……. 仮定 (2) (¬P→¬¬P)→((¬P→¬P)→P) ……… A3 (3) ¬¬P→(¬P→¬¬P) …….. A1 (4) ¬P→¬¬P …… (1)(3)MP (5) (¬P→¬¬P)→P ……… (2)(4)MP (6) ¬P→((¬P→¬P)→¬P) …… A1 (7) (¬P→((¬P→¬P)→¬P))→((¬P→(¬P→¬P))→(¬P→¬P)) …… A2 (8) (¬P→(¬P→¬P))→(¬P→¬P) ……. (6)(7)MP (9) ¬P→(¬P→¬P) …… A1 (10) ¬P→¬P …… (8)(9)MP (11) P …….. (5)(10)MP
(6)から(10)はP→PのproofのPのところを¬Pに置き換えてもう一度繰り返している
Proofがあることがわかっているtheoremは公理と同じように、deductionやproofで自由に使って良いとする
さらに
P→Pのproofが一旦されているなら
そのproofで「P」が出ているところを「(Q→¬R)」に置き換えると(Q→¬R)→(Q→¬R)のproofとして使える
¬¬P→Pにproofがある
一度proofされているものは「図式」として使って良いとする
(1) ¬¬P (2) (¬P→¬¬P)→((¬P→¬P)→P) ……. A3 (3) ¬¬P→(¬P→¬¬P) …….. A1 (4) ¬P→¬¬P …….. (1)(3)MP (5) (¬P→¬P)→P ……. (2)(4)MP (6) ¬P→¬P ……… theorem1 (7) P …… (5)(6)MP
¬P→¬Pのproofを端折る
派生規則
例
P→Q, Q→R, P⊢Rであることがわかったとする
このdeductionをDと呼ぶ
他のdeductionをする時に、論理式の列の中にP→Q, Q→R, Pの3つの式が現れているなら
その列に続けてRを書き込んでもちゃんとしたdeductionw@あるための条件には違反しない
とすると
P→Q, Q→R, P⊢Rであることがわかったなら
Deductionの途中で「P→Q, Q→R,PならばRを引出しても良い」 という規則をあたかもMPに類する推論規則として扱っても良い
さらにP,Q,Rという原始指揮を一斉に別の論理式に変えても良い
ということは
「A→B、B→C、AからはCを引出しても良い」という推論規則を手に入れたと考えても良い
これらは公理系APLから導き出された規則
これまで導き出された派生規則
D1 A→B、A→(B→C) から A→Cを引出しても良い (254ページ) D2 A→B、B→C、A から Cを引出しても良い (254ページ) D3 A から B→Aを引出しても良い (練習問題77の(1)) D4 A から (A→B)→Bを引出しても良い (練習問題す77の(2)) D5 A→B から (B→C)→(A→C)を引出しても良い (256ページ) D6 A→B、B→C から A→Cを引出しても良い (256ページ) D7 A→(B→C)、B、A から Cを引出しても良い (練習問題78の(2)(a)) D8 A→(A→B)、A からBを引出しても良い　(練習問題78の(2)(b)) D9 ¬B→¬A、A から Bを引出しても良い (練習問題78の(2)(c)) D10 ¬B→¬A から A→Bを引出しても良い (練習問題78の(2)(c)) D11 ¬¬A からAわ引出しても良い　(258ページ)
10.1.7 自然演繹も公理系の一種である
公理系もいろいろある
命題論理の公理系はたくさんある
APLと違う公理系の例
メレディス(Meredith)の公理系M
A1 (((P→Q)→(¬R→¬S))→R)→T)→((T→P)→(S→P)) R1 MP R2 RS
どの公理系か区別する必要がある
⊢APLBとか⊢MB
自然演繹も公理系の一つである
メレディスの公理系を一歩進めて、公理が一つもない公理系
自然演繹
公理を置かず、推論規則だけで作られたもの

10.2　シンタクスとセマンティクス

10.2.1 論理的帰結の2通りの考え方
論理学の目標
論理の正しさとは何か、(論理的に出てくるとはどういうことか)を調べることを目標にしていた
それらに対して2つの仕方で答えを出す
意味論的帰結
一つは「セマンティクスを道具として捉えた論理的帰結の概念」
論理式A1,A2,…,AnからCが論理的に出てくるということは
A1,A2,…,Anが全て真になるような真理値割り当て/モデルの元でCも必ず真になる
この考えの元では、Cが論理的に真になるということは
Cがどのような真理値割り当て/モデルの元でも必ず真になるということ
(言い換えれば)「Cがトートロジー/妥当式である」ということとして捉えられる
こうした論理的帰結や論理的真理の捉え方は
記号にどのような解釈を割り当てるかという観点に立っている
記号にどのような意味を割り当てるかということと そこから派生する様々な事柄を担当する部門
真理表の話やモデルの話はセマンティクスに属する
トートロジーや妥当式、論理的同値といった概念はみんな真偽に関係するので セマンティクスに属する概念
「⊨」によって表示される論理的帰結の概念
この路線は、論理的帰結の概念は「論理定項の意味」によって明らかになるはずだという直観を突き詰めていったもの
構文論的帰結という考え方
上記とは異なる論理的帰結概念の捉え方
論理的に出てくるかどうかは「式の形だけの問題」だという直観を突き詰めたもの
この考えの元では
論理式A1,A2,…,AnからCが論理的に出てくるということは
「公理系APL(あるいはND)において、A1,A2,…,Anを仮定とするCのdeductionが存在する」ということ
A1,A2,…AnとAPLの公理系を出発点として推論規則を順序よく当てはめて置き換えるとCにたどり着く
論理式Cが論理的真理であるということ
仮定を置かないCのdeductionがあるということ
(言い換えると)Cがtheoremであるということ
Deductionを構成するプロセスでは
意味や真理条件についての考慮は全く必要ない
例
推論規則のMP「AとA→BからBを引出しても良い」
「AとA→Bが真だから、AとA→BがあればBも書いても良い」ということではなく
「AとA→Bという形をした式がdeductionに出てきたならば、Bという部分を取り出して次に書いても良い」という規則を言っているに尽きる
言語を純粋に図形の連なりに捉えて、 記号がどんな形をしてどのように並んでいるかだけに注目して論理を考える立場
なぜAPLで「P→P」のproofをするのか?
シンタクスとセマンティクスを区別して考える必要がある
シンタクスの観点
P→Pは図形の列
意味はないので自明も何もない
「proof」はある条件を満たした式の列のことに他ならない
P→Pのproofを作ることによりわかること
P→Pが真であるとかトートロジーであるということではなく
公理から規則に従って式を変形していくことにより、P→Pという記号列に到達することができる
「APLに与えられた公理から形式的な記号の書き換えだけで出てくるかどうか」はわかり切ったことではない
セマンティクスの観点
P→Pが真であることはわかり切っている
なぜシンタクスの立場が成立してきたのか
現代の論理学が数学のなかで生じてきたことが関係している
数学では数や集合などを対象に証明や演繹をしている
数学が証明自信を対象にして調べたくなったにどうするのか?
証明そのものを数学でとらえるしかない
厳密な規則に従って作られる図形の連なりとして証明をとらえる
10.2.2 シンタクスにおいて捕らえた矛盾の概念
論理学は3つの研究対象を持っている
(1)論理的帰結の概念
(2)論理的真理の概念
(3)論理的矛盾の概念
これらに対する2 つのアプローチ
論理定項の意味に注目するセマンティクス
意味は無視して論理の図形変形ゲーム的な側面に注目するシンタクス
研究対象のうち(1)と(2)は上述で述べられている
残りの(3)論理的矛盾の概念について
セマンティクスの立場
定義
式の集合Γがセマンティクス(意味論)的に矛盾している(Γ⊨と書く)
⇔
Γに属する式を一斉に真にする真理値割り当て/モデルが存在しない
Γが意味論的に矛盾していない時、Γは充足可能または整合的であるという
シンタクスの立場
定義
式の集合Γがシンタクス(構文論)的に矛盾している(Γ⊢と書く)
⇔
Γ⊢A、Γ⊢¬Aとなるような論理式Aが存在する
Γが構文論的に矛盾していない時、Γは無矛盾であると言う
これらの定義からはよく似た結果が導かれる
定理39
(1) Γが意味論的に矛盾している ⇒ 任意の式Bについて、Γ⊨B
(2)Γが構文論的に矛盾している ⇒ 任意の式Bについて、Γ⊢B
Γが構文論的に、無矛盾であることを証明したい場合
Γからdeductionできない論理式が一つでもあれば良い
構文論的無矛盾性
式集合の構文論的無矛盾性と同様に公理系に対しても構文論的無矛盾性を定義できる
定理
公理系Kが構文論的に無矛盾である
⇔
Kには⊢Aかつ⊢¬Aとなるような論理式Aが存在しない
定理41
APLは無矛盾である
10.2.3 完全性がなぜ重要なのか
シンタクスとセマンティクスアプローチのまとめ
セマンティクスとシンタクスの論理的帰結が重なることはあるのか?
APL、NDに関しては成り立つ
完全証明がうまくいくと
「論理的に出てくる」を意味論的にとらえる仕方と構文論的にとらえる仕方が重なる
「重なる」は意味論的帰結の概念と構文論的帰結の概念が同じ概念になることではない
お互いの集合が広がりにおいて一致すると言うこと

10.3　命題論理の公理系の完全性証明

10.3.1 完全性定理とヘンキンによる証明の利点
完全低定理の証明
強い完全性定理
公理系のtheoremの集合とトートロジーの集合がぴったり一致することを主張するもの
前述は上記の特殊ケース
セマンティクスで捉えた論理的帰納の概念とシンタくすで捉えたそれが外延的に一致する
完全性定理は「シンタクスとセマンティクスの架け橋の役割をする定理」
これから証明するのはさらにちょっとだけ強い結果
定理42
強い完全性定理 (strong completeness theorem)
なぜ強いのか?
Γが無限集合でも良い
Γ⊢Bは
過程が全てΓの要素であるようなBのdeductionがある
BのdeductionにΓの要素が全て使われることは要求していない
Γ⊨B ⇐ Γ⊢B
の証明
B1が小売りである時、APLの公理は全てトートロジーである
B1がΓの要素であるとき、仮定によりVはΓを充足するような真理値割り当てであったから、B1はVの元で真である
MPの元でB1から導かれるCも真である
Γ⊨B ⇒ Γ⊢B
完全性の証明法
レオン・ヘンキン (Leon Henkin)の証明
以下の2つの点で優れている
(1)
Γ⊢Bは仮説ΓからBへのdeductionだが
deductionはどの公理系のdeductionかを抜きにして意味がない
本来は全ての公理系で完全性を証明する必要がある
ここの公理系の特殊事情に左右される箇所ができるだけ少ないような証明であることが望ましい
(2)
ヘンキンの照明は拡張性に富んでいる
様々な論理(様相論理など)の公理系に適用可能
10.3.2 ヘンキンの証明のアウトライン
ヘンキンの定理
まずAPLの完全性を証明
少しの手直しでNDにも書き換え可能
定理43
いかなる論理式の集合Γと論理式Aについても、次が成り立つ
Γ⊨A ⇔ Γ⋃{¬A}は充足可能ではない(意味論的に矛盾する)
定理40
いかなる論理式の集合Γと論理式Aについても、次が成り立つ
Γ⊢A ⇔ Γ⋃{¬A}は構文論的に矛盾する
定理44:ヘンキンの定理
論理式の集合Γが構文論的に無矛盾 ⇒ Γは充足可能
構文論的に無矛盾な論理式の集合は 必ずそれに含まれる全ての論理式を一斉に真にするような真理値の割り当てがある ことを証明すれば良い
ヘンキンの定理をどのように証明するのか
ヘンキンの定理を証明すれば強い完全性が証明されたことになる
この証明方針は以下のとおり
(1)ヘンキンの定理を証明するには、
構文的に無矛盾な集合Γに含まれる論理式を 全て真にすることのできるような真理値割り当てがあることを示せば良い
一番ストレートなやり方は
Γに応じてそのような真理値割り当てを作る手順を与えること
(2)ところが、「構文的に無矛盾です」と言うだけでは
Γについての情報が乏しすぎて、
Γから直接そうした真理値割り当てを構成することができない
(3) そこで、あるやり方Γを拡大して
Γをすっぽり含んだ証明上都合の良い集合Γ*を作る
(4) Γ*はその作り方からして
そこに含まれる全ての論理式を真にする真理値割り当てを容易に作ることができる
と言うことを示す
(5) Γ*はΓを含んでいるから
(4)で作った真理値割り当てはΓの全ての式を真にする
極大無矛盾集合
Γをすっぽり含んだ証明上都合の良い集合Γ*
Γを部分集合としてすっぽり含んでいて、
無矛盾で
しかもある意味でそれ以上大きな集まりはないようなギリギリの集合
定義
論理式の集合Δが極大無矛盾である
⇔
Δは構文論的に無矛盾であり、 Δの要素ではない全ての論理式Aに対しΔ⋃{A}は構文論的に矛盾している
自分に含まれていない式をそれ以上一つでも付け加えると、 途端に矛盾してしまう
Γそれ自体を相手にしていると
それに含まれる式全てを真にする真理値割り当てを構成する方法が見当たらない
Γを極大無矛盾集合Γ*にまで拡大すると
Γ*に含まれる式をすべて真にする真理値割り当てはいつでも同じ手順で簡単に手に入る
Γ⊆Γ*ゆえ
この真理値割り当てはΓの全ての式を真にするから
Γは充足可能であることがわかる
タブローの方法が信頼できることを証明するため
開放経路をヒンティッカ集合へ拡大したのと同じようなことをやる
2つの補助定理
ヘンキンの定理を章目雨するために次の2つの補助定理を証明すれば良い
補助定理44-1 : リンデンバウムの補助定理 (Lindenbaum’s lemma)
Γが構文論的に無矛盾な式の集合である時、
Γを部分集合とするような極大無矛盾集合Γ*が少なくとも一つ存在する
補助定理44-2 : 極大無矛盾集合の充足可能性補助定理
極大無矛盾集合Γ*が与えられると
Γ*に含まれる全ての式を真にする首尾一貫した真理値割り当てが決まる
つまり、極大無矛盾集合は充足可能である
10.3.3 補助定理44-1の証明
2段階の証明を行う
(1)任意の無矛盾な式集合Γが与えられた時にそれをΓ*にまで拡大するための手順を与える
(2)その手順に従ってΓを拡大したΓ*が本当に極大無矛盾集合になっていることを示す
ΓをΓ*にまで拡張する手順
全ての論理式の集合は列挙可能である
全ての論理式を自然数の番号をつけて1列に並べることができる
全ての論理式を列挙した列が一つ与えられているとする
無矛盾なΓから始めて、そこにこの列から論理式を順にとってきて
もしそれをΓに付け加えても矛盾しないのなら付け加える
以上の操作を繰り返してΓを膨らませる
この操作により極大無矛盾集合Γ*に至る
具体的な手順
(1) Γ0=Γとする
(2) Aが論理式の列挙においてi番目に現れる論理式だとする
その時
Γi⋃{Ai}が構文論的に無矛盾であるなら、それをΓi+1とする
Γi⋃{Ai}が構文論的に矛盾するなら、Γi+1=Γiとする
Γ*が極大無矛盾であることの証明
(1) Γ*が無矛盾であることの証明
(2)Γ*が極大であることの証明
10.3.4 補助定理44-2の証明
2つの補助定理
補助定理44-2の証明
10.3.5 完全定理からすぐに導かれること
定理45
APLにAPLでprovableでないどんな論理式を公理図式として付け加えても構文論的に矛盾してしまう
コンパクト性定理の別証明
コンパクト性証明
Γの全ての有限部分集合が充足可能である
⇔
Γは充足可能である
上記は完全性定理の副産物として証明できる
証明
Γのあらゆる有限部分集合が充足可能
⇒ Γのあらゆる有限部分集合が無矛盾(適合性による)
⇒ Γが無矛盾(deductionの有限性による)
⇒ Γは充足可能(完全性定理による)

第Ⅲ部のまとめ

次回は第4部-論理学はここから先が面白い 非古典論理の読書メモについて述べる。