『数理論理学』1 | 宇宙とブラックホールのQ&A (ameblo.jp)
『数理論理学』5 | 宇宙とブラックホールのQ&A (ameblo.jp)
----------------------------------
次は、ゲンツェン流シーケント計算の古典論理体系 LK です。
定義 ￢φ と φ←→ψ の定義は、HM と同じ。
LK の公理
(ID) (⊥⇒)
φ ⇒ φ ⊥ ⇒
以下、 Γ，Σ，Δ，Π は、いずれも 0 個以上の論理式の列。
LK の構造規則 (CUT) Γ ⇒ Π, φ φ, Σ ⇒ Δ
Γ, Σ ⇒ Π, Δ
(w⇒) Γ ⇒ Δ (e⇒) Γ, φ, ψ, Σ ⇒ Π (c⇒) φ, φ, Γ⇒ Π
φ, Γ ⇒ Δ Γ, ψ, φ, Σ ⇒ Π φ, Γ⇒ Π
(⇒w) Γ ⇒ Δ (⇒e) Γ, Σ ⇒ Π, φ, ψ (⇒c)Γ⇒ Π, φ, φ
Γ ⇒ Δ, φ Γ, Σ ⇒ Π, ψ, φ Γ⇒ Π, φ
ここで、w, e, c は次の頭文字です。
ｗ：弱化(Weakening)
ｅ：交換(Exchange)
ｃ：縮約(Contraction)
LK の論理規則
(→⇒)Γ ⇒ Π, φ ψ, Σ ⇒ Δ (⇒→) φ, Γ ⇒ Δ, ψ
Γ, φ→ψ, Σ ⇒ Π，Δ Γ⇒ Π, φ→ψ
(∧⇒) φi, Γ ⇒ Δ (⇒∧) Γ ⇒ Δ, φ Γ ⇒ Δ, ψ
φ1∧φ2, Γ⇒ Δ Γ ⇒ Δ, φ∧ψ
(∨⇒) φ, Γ ⇒ Δ ψ, Γ ⇒ Δ (⇒∨) Γ ⇒ Δ, φi
φ∨ψ, Γ ⇒ Δ Γ⇒ Δ, φ1∨φ2
(∀⇒) φ[τ/ξ], Γ⇒ Δ (⇒∀) Γ⇒ Δ, φ[ζ/ξ]
∀ξφ, Γ ⇒ Δ Γ ⇒ Δ, ∀ξφ
ただし、ζはΓ，Δ，∀ξφに含まれないとする。
(∃⇒) φ[ζ/ξ], Γ⇒ Δ (⇒∃) Γ⇒ Δ, φ[τ/ξ]
∃ξφ, Γ ⇒ Δ Γ ⇒ Δ, ∃ξφ
ただし、ζはΓ，Δ，∃ξφに含まれないとする。
ゲンツェン流直観主義論理 LJ は、 LK においてシーケントの右辺の長さを高々 1 に制限した体系です。
すなわち、Γ⇒Δ において、 |Δ|≦1 。ただし、|Δ| はΔに含まれる論理式の数。
さらに、ゲンツェン流最小論理 LM は、 LJ から (⇒w) と (⊥⇒) を除いた体系です。
証明の具体例は、別途紹介することにして、今回は省略します。
「第11章 カット除去定理」
ゲンツェン流シーケント計算のカット除去定理(cut elimination theorem)とは、ゲンツェンによって1934年に発見され、別名、基本定理(fundamental theorem)とも呼ばれるきわめて重要な定理です。
（ｋ：と書いてあり、私も昔から知っていますが、実はその重要性が全然ピンと来ません。最初からカットを使わないで証明すればいいだけじゃん、と思ってしまいます。頭のどこかの血管が詰まっているのかな(^^:）
定義11.1（ゲンツェン流シーケント計算Ｋ のカット除去定理） Ｋ の任意のシーケントＳについて、Ｓを終式とするＫ の証明図Ｄ が存在するならば、Ｓを終式とする Ｋ －CUT の証明図が存在する。ただし、Ｄに現れる自由変項は、Ｄ において束縛変項としては現れないものとする。
Ｋ －CUT は、シーケント計算Ｋ から CUT を除いたものです。
定理11.2 LK，LJ，LM において、カット除去定理が成り立つ。
定理自体の証明は後回しです。
この定理の応用として無矛盾性と公理の独立性の証明の例が出てきます。
定理11.5（LK，LJ の無矛盾性） |－/LK ⊥， |－/LJ ⊥．
記号「|－/」は、本来は「|－」の右側の横棒に斜め線/が掛かっています。
定理11.8（LJと(LEM)の独立性） |－/LK φ∨￢φ．
LEM は、排中律(law of Excluded Middle)のことです。
定理11.9（LJと(DNE)の独立性） ￢￢φ |－/LK φ．
DNE は、二重否定除去律(Double Negation Elimination)のことです。
この後、カット除去定理の証明が十数ページ続きますが、省略します。
「第12章 タブロー式シーケント計算」は、第 I 部で出てきたタブローをシーケント計算にしたもので、TAB で表されます。
TAB は、それまでに出てきた古典論理の体系と同等です。
次の章の主役になるので本書での位置付けは重要なのですが、あまり面白いものでもないので(^^;、ここでは省略します。
最終章「第13章 健全性と完全性」は重要なので、ある程度丁寧に見ていきます。
この書評では省略しましたが、前章までで次の関係が得られています。
Γ |－HK φ ⇐＝⇒ Γ |－NK φ ⇐＝⇒ Γ |－LK φ
⇐＝⇒ Γ |－LK－CUT φ ⇐＝⇒ Γ |－TAB φ．
（本章には関わりませんが、
Γ |－HJ φ ⇐＝⇒ Γ |－NJ φ ⇐＝⇒ Γ |－LJ φ．
Γ |－HM φ ⇐＝⇒ Γ |－NM φ ⇐＝⇒ Γ |－LM φ．
という関係も得られています。）
しかし、これら古典論理の体系の妥当性は保証されていません。
定義13.1（証明体系の健全性(soundness)） 任意の論理式の列 Γ，Δ について以下が成り立つとき、証明体系Ｋ は健全(sound)である、という。
Γ |－Ｋ Δ ＝⇒ Γ |＝ Δ
健全性とは、証明できる推論は意味論的に妥当であり、妥当でない推論が証明されることはない、ということです。
定義13.2（証明体系の完全性(completeness)） 任意の論理式列 Γ，Δ について以下が成り立つとき、証明体系K は完全(complete)である、という。
Γ |＝ Δ ＝⇒ Γ |－Ｋ Δ
完全性とは、意味論的に妥当な推論は証明することができ、妥当であるのに証明できないような推論はない、ということです。
HK などの5つの体系はいずれも同等であることが証明されているので、どれか1つについて健全性と完全性を証明すればよいわけです。
本章では、TAB について証明が行われます。
次に、演繹の定義を、無限個の前提・帰結の場合も含むように拡張します。
定義13.4 Γ，Δが無限個の論理式を含む場合、Γ |－Ｋ Δ を 「Γ’⊂Γ，Δ’⊂Δ（ただし |Γ’|，|Δ’| は有限）を満たす Γ’，Δ’ が存在して、Γ’ |－Ｋ Δ’ が成り立つ」 と定義する。
定義13.6（推論の意味論的妥当性：一般の場合） Γ，Δ を論理式列とする。
Γ |＝ Δ ＝： ￢Δ, Γ が充足不能である
この後、まず TAB の健全性の証明があります。
定理13.10（TAB の健全性） 任意の論理式の列 Γ，Δ について以下が成り立つ。
Γ |－TAB Δ ＝⇒ Γ |＝ Δ
完全性定理の証明には、ヘンキンの定理を経由します。
定理13.12（ヘンキンの定理） 任意の論理式の列Γについて以下が成り立つ。
Γ |－/TAB ＝⇒ Γは可算領域で充足可能
ただし、Γは可算領域(countable domain)で充足可能とは、高々可算の領域 DM が存在して、Γを同時に充足するような解釈 M＝<DM, FM> が存在する、ということである。
定理13.13（完全性定理(completeness theorem)） 任意の論理式φについて、以下が成り立つ。
|= φ ＝⇒ |－TAB φ
定理13.14（強い完全性定理(strong completeness theorem)） 任意の論理式列 Γ，Δ について以下が成り立つ。
Γ |= Δ ＝⇒ Γ |－TAB Δ
ヘンキンの定理から次の2つの定理が証明されます。
定理13.23（レーベンハイム・スコーレムの定理(Löwenheim-Skolem’s theorem: LST)）
Γが充足可能 ＝⇒ Γは可算領域で充足可能
LSTは、一階の理論では可算ではない無限集合を扱う理論であっても、可算領域で解釈可能であることを示しています。
このことは、スコーレムのパラドクス(Skolem’s paradox)として知られています。
数理哲学のネタの一つですね。
定理5.109（コンパクト定理） すべてのΓ’⊂Γ（ただし |Γ’| は有限）について、
Γ’が充足可能である ＝⇒ Γが充足可能である
最後のページで、次のような考え方を紹介しています。
証明体系が論理体系（たとえば一階命題論理や一階述語論理）の意味論とは異なるやり方で、別の意味論を独立に与えている、というものです。
このような考え方を証明論的意味論(proof-theoretic semantics)というとしています。
（意味論という分野がすでにあるのだから、別の「意味論」を持ってくるのは混乱を招くように思うのですが。なお、この場合の「証明論的」の代わりに「構文論的」と言っても同じです。P.41欄外注*12参照）
今回の書評はこれで終わりです。
私が苦手としていた意味論の部分を載せられたのが、一番の収穫です。
省略した部分は、別の形で取り上げたいと思っています。
論理学関係の書評としては、次に様相論理の入門書を取り上げるつもりです。
まあ、いつもながら予定は未定なので、どうなるかは分かりませんが。
★ 本日、将棋順位戦B級1組第13局(最終局)が行われており、藤井聡太竜王は佐々木勇気七段と対局中です。持時間6時間の最長棋戦なので、終局は深夜になる可能性があります。藤井竜王にとってはA級昇級がかかった重要な対局です。結果は明日の記事でまとめる予定です。
★★ 今日のロジバン 潔白 .u’ucu’i
.u’u cu’i mi zukte no da 「ウフシュヒ ミ ズㇰテ ノ ダ」
無実だ、私は何もしていない。
.u’ucu’i ： 潔白。既成のそれについて自分は潔白だと思う気持「私のせいではない」。心態詞(純粋感情)UI*1類 <-u’u 後悔
zukte ： 行為/実行する，x1は x2(行動内容)を x3(目的/目標)のために。-zuk-, -zu’e-
no は数詞 0 なので、{ zukte no da } で 「0個の行為をした」 つまり 「何もしていない」 となります。
出典は、