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
と表記する。

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

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

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


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