このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

論理とはなにか？ (2)

雑記／備忘

「論理とはなにか？」の続き。論理それ自体の知識をできるだけ仮定しないで、論理の一般論のエッセンスを解説しましょう（そう試みてはみるよ）。

内容：

前置き

ストラスバーガーは、「論理とはプレ順序集合だ」と言っているわけですが、この主張が、既存の様々な論理的システムにうまく適用できるかどうかを調べたいと思います。とはいえ、既存の様々な論理システムに関する博物学的な知識が要求されるのではたまらないので、命題論理（に相当する日常論理）、中学レベルの連立方程式を素材にします。

記号列、記号的図形の集合を外から眺める、という発想は必要かも知れません。このへんのことは、「論理を身に付けるには」の前半を参照してください。

フツーっぽい命題証明系

Sは論理的文（命題）の集合だとします。さらに、なんらかの証明手続きが在るとします。その手続きがコンピュータ・プログラムとして実現されていると考えるといいですね。証明手続き＝プログラムをPとします。使い方はこんな感じ：

Prover p = new P();
p.addAssumption(a);
boolean result = p.prove(b);
// 無限走行の可能性あり
if (result) echo("b is proved.");

上のコードが示しているように、文aを仮定して文bがプログラムPで証明できるとき、a |- b と書きます。特に何も仮定しなくてもbが証明できるなら |- b （左側は空っぽ）と書きます。実は、a |- b かどうかの判定は人間には困難です。プログラムP（上の例ならp.prove(b)の実行）がなかなか終わらないとき、いつまで待てばいいか分かりませんからね。で、判定は神様にやってもらいます（神頼みについては、「論理を身に付けるには」の後半を参照）。

“証明手続き＝プログラムP”がまともに作られているなら：

  1. a∈Sに対して、a |- a
  2. a, b, c∈Sに対して、a |- b かつ b |- c ならば a |- c

は成立していると期待していいので、証明可能を表す記号‘|-’を不等号‘≦’に置き換えた次も成立します。

  1. a∈Sに対して、a≦a
  2. a, b, c∈Sに対して、a≦b かつ b≦c ならば a≦c

よって、(S, ≦）はプレ順序集合となります。これが、論理的システムをプレ順序集合とみなす考え方の原型／典型例です。

「仮定なし」と「複数の仮定」への対処

仮定なしの証明可能性 |- a を不等号‘≦’で書こうとすると、左辺がないので困ってしまいます。また、複数の仮定からの証明可能性 a, b |- c とかも不等号ではうまく書けません。

「真」を表す定数記号Tと、アンド結合（連言、合接、conjunction）∧があれば、この問題は解決します。|- a は、T |- a のことだとみなして、不等式 T≦a で表現します。a, b |- c は (a∧b)≦c です。

「xを仮定する」とは「仮に、xを真だとする」ことですから、「Tを仮定する」は「仮に、真を真だとする」こと。「仮に」じゃなくて真はいつだって問答無用に真ですから、T |- a は「仮定なしでaを証明できる」ことですね。

同様に、「x, yを仮定する」とは「仮に、xを真、yも真だとする」こと。これは「x∧y（‘xアンドy’という一つの文）を真だとする」と同じことですから、a, b |- c を (a∧b)≦c と表現してもいいでしょう。

まとめると、「真」を表す定数記号と「アンド」を表す演算記号（論理結合子）があるなら、“仮定なしの証明可能性”も“複数の仮定からの証明可能性”も‘≦’を使った不等式表現に直せるってことです。

一次方程式の証明系

多くの論理的システムがTと∧を備えていますが、いつでもTと∧があるとは限りません。いま、中学で習う 2x - 3y = 0 とか -y + 5 = 10x のような一次方程式を考えます。変数x, yを含むかもしれない一次方程式を“文”とみなして、その全体をSとします。一次方程式のことをA, Bなどの大文字（メタ変数）で表します（x∈S などと書くと、さすがに混乱するでしょうから）。

足し算／掛け算の法則と等式の変形規則を形式化して（つまり、コンピュータの記号処理で扱えるように定義して）、一次方程式Aから一次方程式Bが証明（導出）されることを A |- B と書きます。例えば、‘-y + 5 = 10x’ |- ‘y = -10x + 5’。

Sは一次方程式だけの集合なので、Tも∧も入ってません。しかし、|- A も、A, B |- C も意味を持ちます。例えば：

  • |- ‘x = x’
  • ‘2x + 3y = 0’, ‘y = 4’ |- ‘x = -6’

この問題の対処は、中学校で習っています。単一方程式の代わりに連立方程式を考えます。連立方程式とは、方程式の有限集合です。特別な連立方程式（方程式の有限集合）として、空の連立方程式{}も許します。連立方程式を使って今までの例を書き換えれば：

  • {-y + 5 = 10x} |- {y = -10x + 5}
  • {} |- {x = x}
  • {2x + 3y = 0, y = 4} |- {x = -6}

一般的な手法としての有限ベキ構成

単一方程式から連立方程式への発展を、一般的に記述しましょう。Sが最初に与えられた文の集合だとして、Pow(S)はXのベキ集合（power set）、つまりSの部分集合全体の集合です。Powf(S)は、Sの有限部分集合だけを寄せ集めた集合だとします（'f'はfiniteから）。

さて、A1, ..., An, B ∈S に対して、A1, ..., An |- B の意味は既に決まっているとします。そのとき、{A1, ..., An} |- {B1, ..., Bm} とは、

  • A1, ..., An |- B1 であり、
  • A1, ..., An |- B2 であり、
  • …（同様）…
  • A1, ..., An |- Bm である。

とします。{A1, ..., An} |- {B1, ..., Bm} の代わりに {A1, ..., An}≦{B1, ..., Bm} と書いてみると、いま新しく定義した‘≦’はPowf(S)の上の関係です。

Powf(S)をS'と書いて、S'のメンバー（Sのメンバーの有限集合）をΓ、Δなどと書くことにしましょう（だんだん記号が足りなくて苦しくなっている）。証明系(S, |-)が、証明系と呼べるシロモノなら、(S', ≦）は次を満たすはずです。

  • Γ∈S' に対して、Γ≦Γ
  • Γ, Δ, Σ∈S' に対して*1、Γ≦Δ かつ Δ≦Σ ならば Γ≦Σ

これで、次の処方箋が得られました； 証明系(S, |-)から直接にプレ順序集合(S, ≦)が定義しにくいときは、S'=Powf(S)として、プレ順序集合(S', ≦)を作ってみる。

今回のまとめと次の話題

Sは論理的文の集合、記号‘|-’は証明可能性を意味するとして、A1, ..., An |- B が（神様から見て）判定可能な証明系があるとき、

  1. 真Tとアンド∧があるなら、‘|-’をそのまま‘≦’に置き換えるだけでプレ順序集合(S, ≦)が得られる。
  2. S'=Powf(S)として、{A1, ..., An} |- {B1, ..., Bm} を適切に定義した上で、新しく定義した‘|-’を‘≦’に置き換えれば、プレ順序集合(S', ≦)が得られる。

続き物にするつもりはなかったのだけど、ハナシが長引いてしまったな。あと1回は書く予定。証明可能性‘|-’ではなくて、定理集合や閉包演算子により論理的システムを定義する方法もあるので、それらの流儀でもやっぱりプレ順序集合が作れることは確認したいので。

*1:このΣは総和の意味ではなくて、単にσの大文字。