命題論理をやることにする。

やはり、この本を読むには命題論理までの素朴な部分を済ませておく必要があると思う。
悩んだが、そこをしっかりやるところまで一旦撤退することにする。
ほんとは、途中で別の本にいくのはよくないんだけど、今回はやってみる。

いくつか吟味した結果、戸田山和久さんの「論理学をつくる」をやることにした。

「論理学をつくる」を読む

2 一階述語論理の演繹体系 (続き2)

理解する、ということはどういうことだっけ? という感覚がすこしずつ戻ってきた。
最終的には正しく使える、ということだ。Duck typing。
それには、慣れと、筋のよい概念構築、抽象と具象の自由な往来、が必要。

今回は慣れを得るために問をやる。

ひとつめ。
帰納法が必要かな、と思ったが、いらんかった。

ふたつめ。
¬右：論理式の変形。
¬左：論理式の変形。
∧右：真偽表。これの論理式の変形がおもいつかず。
∧左：シーケントの定義まんま。
∨右：シーケントの定義まんま。
∨左：既出の規則から導出。
⊃右：既出の規則から導出。
⊃左：既出の規則から導出。

みっつめ。
読んでみた。なるほど。そう読んで違和感はない。

よっつめ。
問題なし。

いつつめ。
シーケント計算って、なんというか、四則演算を簡易にやるための筆算式のようなものなんですね。
それがなくても同等のことは可能。だけどそれがあると簡易にできる。
そして、そのやり方自身がそれなりのルールをもっている。

むっつめ。
ここ、概念的にひっかかるところがどうも気になってしまう。
演繹体系が完全であることの意味の説明がどうもわからない。
「正し論理式はすべて定理として証明可能」というが、論理式の正しさはセマンティクスに属しているんじゃなかったっけ?
命題論理のストラクチャーがでてくるけど、これがわからない。命題論理を理解していることが本書の予備知識として求められてはいるのだが。。。
命題論理をきっちりやった方がいいんだろうな。それは別途やろう。
今は、慣れることに重点をおく。
駄目だ。飛ばす。

ななつめ。
飛ばす。。。

やっつめ。
((P∧Q)∨(P∧R))⊃(P∧(Q∨R))：証明できた。
¬(P∧Q)⊃(¬P∨¬Q)：証明できた。
(¬P∨¬Q)⊃¬(P∧Q)：証明できた。
(¬P∨Q)⊃(P⊃Q)：証明できた。
(P⊃Q)⊃(¬P∨Q)：証明できた。
P⊃¬¬P：証明できた。
¬¬P⊃P：証明できた。
((P⊃Q)⊃P)⊃P：証明できた。
((P1∧P2)∨(Q1∧Q2))⊃((P1∨Q1)∧(P2∨Q2))：証明できた。

ここのつめ。
やった。

とお。
Qが真でPが偽。
P1,Q1を真、P2を偽。

これで、命題論理のシーケント計算に少し慣れた。
今日はここまで。

2 一階述語論理の演繹体系 (続き)

再チャレンジ。
スタート時点から、かなり仕事で疲れきった状態。。。

全体の流れ。

シーケント定義
命題論理のシーケント計算
　推論規則
　完全性
　ワングのアルゴリズム
一階述語論理のシーケント計算
　推論規則

これ以降は次章。次章ではエルブランの定理と完全性。

少し読んでみて、手を動かしてみて、アタリは掴めてくる。
だけど、やっぱり自分が何をやっているのかが不明瞭になってくる。

そこで、いったんやろうとしていることの整理。
用語の確認から。

演繹体系とは？
公理と推論規則の組。

推論規則とは？
いくつかの命題を前提として、新たな命題を結論として導くための規則。

シーケント
論理式の簡略表記法のひとつ。
A1,…,Am→B1,…,Bn
は、
∀x1…∀xk(A1∧…∧Am⊃B1∨…∨Bn)
の略記。

恒真シーケント
Γ→Δが恒真ということは、どのようなストラクチャーをもってきても
Γの中のどれかが偽になるか、Δの中のどれかが真になる。
A1∧…∧Am⊃B1∨…∨Bn
が恒真論理式であるということ。

命題論理のシーケント計算
まず、シーケント計算とは、シーケントからシーケントへの一連の変形についてまとめて、それぞれに名前を付けたものである。
一連の変形というのは、複数のシーケントからあるシーケントに変形するときに、前者が恒真シーケントであれば、後者も恒真シーケントであるようなものである。

その記法は、
前提1 … 前提n
------------(変形の名前)
結論
とする。

命題論理の場合、次のものがある。
並べ替え
¬右
¬左
∧右
∧左
∨右
∨左
⊃右
⊃左

おどろいたのは、これらの変形をシーケント計算の記法で書くと、そこそこ綺麗に書けることである。

具体的な推論規則
これがわからない。。。
シーケント計算の推論規則は、命題論理全般に当てはまるものだと思う。恒真だから。
だったら具体的もへったくれもないような。
恒真ということは、もってくるストラクチャーによらない、ということ。いや、今、命題論理だからストラクチャーはいらんか。そうじゃなくて、命題AiやBjの真偽によらず成りたつということ。いや、それは違う。P∨¬Pというのはそうなのだが、シーケントが恒真(またはトートロジー)というのは、また違うことではないか。
具体的な推論規則、については先送りとする。

イニシャル・シーケント
シーケントの両辺に同じ論理式があるとき、それをイニシャル・シーケントと呼ぶ。
イニシャル・シーケントは恒真シーケントである。

証明可能
イニシャル・シーケントに対して推論規則(シーケント計算)を有限回適用して得られるシーケントを証明可能であるという。

証明(証明図もしくは証明木)
シーケント計算を段積みにして、その一番上のシーケントが全てイニシャル・シーケントのものを証明と呼ぶ。

定理
論理式Aについて、→Aというシーケントが証明可能であるとき、論理式Aが証明可能である、という。
証明可能な論理式を定理と呼び、
├A
と表記する。

命題論理のシーケント計算の完全性
ある演繹体系によって、命題論理のなかの任意の恒真論理式が証明可能であるとき、その演繹体系を完全であるという。
命題論理のシーケント計算は、完全である。

恒真かどうかの判定
シーケントまたは論理式が与えられたとき、シーケント計算をつかって、それらが恒真であるかないかを判定(決定)することができる。
そのときに使うアルゴリズムを、ワングのアルゴリズムという。

シーケントを偽にするストラクチャー
命題論理のストラクチャーって定義されていたっけ。。。
字句通りに理解すると、ワングのアルゴリズムである論理式が恒真でないことが判定できたとすると、ワングのアルゴリズムで作成した証明木の葉にイニシャル・シーケンスでないものが含まれており、そのシーケンスを実現するストラクチャーがそれである。


以上で、流れは掴めたような気がする。
詳細を追う&疑問点を確認するのは次回としよう。。。