ストラスバーガーの論文を紹介、その第3回。
前回の最後で：
あと1回は書く予定。証明可能性‘|-’ではなくて、定理集合や閉包演算子により論理的システムを定義する方法もあるので、それらの流儀でもやっぱりプレ順序集合が作れることは確認したいので。
と書いたので、そこらへんの話題です。
内容：
前置き
ストラスバーガーの原論文は解説的なものですが、一般向けの記事ではないので、少ない予備知識で紹介しようとすると文章の量が増えますね。もとの一文が一段落に、もとの一段落が一記事に、という感じ。でも、僕は翻訳ではなくて噛み砕いた説明を提供したいので、いたしかたないでしょう。
さて、以下、記号「⇒」、「⇔」は“地の文”で内容的に使います。つまり、「…ならば…」、「…と…は同値」という日本語表現の略記に過ぎません。一方、「⊃」（含意）、「∧」（連言）、「T」（真）などは、論理的システム内部の記号として使います。さらに、「|-」、「|⇒」は論理的システムに関する主張に使う記号で、日本語表現の「仮定から、または仮定なしで証明できる（証明論的に帰結する）」、「伴意する（モデル論的に帰結する）」の略記です。
必要なら、次を参照してみてください。
定理集合またはセオリー
なんらかの論理的システムにおける論理文（logical statement/sentence）をすべてかき集めた集合をSとします。そして、Sの部分集合K（K⊆S）が天下りに与えられている状況を考えます。Kに属する文は“正しい命題”だと解釈することにして、Kを定理集合（a set of theorems）とかセオリー（a theory）と呼びます。
「セオリー」はもちろん「理論＜りろん＞」という意味ですが、漢字で「理論」と書くと、かなり混乱した印象を与える（例えば、理論の理論とか）ので、「セオリー」とカタカナ書きしましょう（「形式的理論」と呼ぶ方法もある）。
セオリーが指定された文集合 (S, K) からプレ順序集合を作るには、もとの論理（論理的システム）に含意が備わっている必要があります。A, Bが文（つまり、A, B∈S）のとき、A⊃B という記号的図形も文だとします（‘A⊃B’∈S ）。そして、
- A∈Sに対して、A⊃A はKに属する。
- A⊃B と B⊃C がKに属するなら、A⊃C もKに属する。
と仮定しましょう。この条件を満たすときに、Kはセオリーと呼ぶにふさわしいのです。*1上の2つの条件は、後でプレ順序を作るために、ご都合主義で導入したみたいに思えますが、含意を持つ（あるいは、含意を定義できる）論理における“正しい命題”の全体が上の条件を満たすことは、経験的に正当化できると思います。
セオリーからプレ順序
(S, K) がセオリーKが指定された文の集合だとします。セオリーの条件から：
- ‘A⊃A’∈K
- ‘A⊃B’, ‘B⊃C’∈K ⇒‘A⊃C’∈K
です。関係≦を、A≦B ⇔ ‘A⊃B’∈K で定義すると：
- A≦A
- A≦B, B≦C ⇒ A≦C
なので、これでプレ順序集合 (S, ≦) が作れました。
さて、Sの部分集合Kをいきなりセオリーとしてドカンと指定してしまう方法はなかなか便利なのですが、Kの由来にはまったく触れないので気持ち悪いですよね。通常、セオリーKは次のようにして作られます。
- なんらかの証明系があって、A∈K ⇔ |- A 。つまり、Kは仮定なしで証明できる命題の全体。適当な仮定からの証明可能性を使ってもよい。
- なんらかのモデルの世界Uがあって、A∈K ⇔ Uに属するどんなモデルMに対しても M |= A 。つまり、Kはモデルの世界において普遍的に妥当な命題の全体。
演繹定理
現存する多くの証明系において、その証明系を外から眺めると次が成立しています。
- A |- B ⇔ |- A⊃B
これは演繹定理と呼ばれる性質です。証明系をコンピュータで実行されるプログラムと考えると、次の2つのコードがいつでも同じ結果となることを演繹定理は主張しています。
/* a |- b */
Prover p = new P();
p.addAssumption(a);
boolean result = p.prove(b);
// 無限走行の可能性あり
if (result) echo("assuming a, then b is proved.");
/* |- a⊃b */
Prover p = new P();
Sentence c = Sentence.implication(a, b);
boolean result = p.prove(c);
// 無限走行の可能性あり
if (result) echo("a⊃b is proved.");
ところで、A∈K ⇔ |- A として定義した集合Kがセオリーとなるには、
- ‘A⊃A’∈K。つまり、|- A⊃A
- ‘A⊃B’, ‘B⊃C’∈K ⇒‘A⊃C’∈K。つまり、|- A⊃B かつ |- B⊃C ⇒ |- A⊃C
これらセオリーの条件を、演繹定理を使って書き換えれば：
- A |- A
- A |- B かつ B |- C ⇒ A |- C
あれれ、これは、文の集合Sで定義された関係 |- がそのままプレ順序関係であることを意味しますね。ということは、演繹定理が成立するような証明系では、次の2つの性質が同じだということです。
- 証明できる文全体の集合Kがセオリーである。
- 証明可能性 |- をS上の関係だと考えてプレ順序になる。
演繹定理が成り立たない（含意が存在しなければ、そもそも演繹定理が無意味）証明系では、上の2つの条件を結びつけることはできません。その意味で、演繹定理は“とり扱いやすい証明系”を特徴付けていると言えるでしょう。
まだ続くのかな
僕が好きな論理の定義として、閉包作用素を使う定義があります。これについて説明するかも知れません（しないかも知れません）。それと、ストラスバーガーの意図としては、論理をプレ順序と考えるのは中間ステップであり、論理を圏として捉えるのが目的なので、「論理は圏だよ」という結論にたどり着かないと心残りかも知れません（でも、忘れるかも知れません）。
*1:ただし、セオリーの定義はいくつか在るので注意してください。
