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

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

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

［参照用 記事］

互換な演繹システムとシーケント、そして矢印記号

雑記／備忘

論理で使う“「ならば」っぽい記号”、“矢印的な記号”については過去に述べたことがあります。

何が主たる問題かというと、地の文で使うメタな記号表現と、演繹システムが処理するデータである形式的表現〈形式化された表現 | 形式表現〉の区別がイイカゲンなことです。イイカゲンには幾つかの意味があります。

  1. 使い分け／書き分けのルールを決めてない。
  2. ルールは決めてあるが、守っていない。
  3. ルールが人により場合によりバラバラである。

僕もヒトのことをどうこう言える立場ではなくて、このブログ内での一貫したルールは決めてません。ひとつの記事内ではなるべく統一的に書くようにはしてますが、記事ごとにルールが違います。バランバランです。

特に意味と使用法が安定しない記号は、“矢印っぽい”記号 '→', '⇒', '|-' です。「証明の“お膳立て”」シリーズなどでは、人間を演繹システムに見立てて、シーケントの区切り記号に '|-' を使ったりしています。今後も、意味と使用法は安定しそうにありません。

この記事では、複数の演繹システムが連携している状況における、何種類かの表現（形式化された表現とメタな表現）について説明します。この記事で使う記号の約束は、ヤッパリここだけのもので、グローバルな約束ではありません。

内容：

論理式を扱うシステムとシーケントを扱うシステム

ゲンツェンのNK/NJシステムの論理式と、同じくゲンツェンのLK/LJシステムのシーケントの関係を説明するために、「さまざまな「ならば」達」で '||-' というメタ記号を使いました。ここでも '||-' を使います。このメタ記号 '||-' と、よりポピュラーなメタ記号 '|-' について説明しましょう。

論理式（もちろん形式化されている）を A, B などのラテン文字大文字で表します。論理式のリストは Γ, Δ などのギリシャ文字大文字で表すのが習慣ですが、ここでは下線を引いたラテン文字大文字にします。A, B などです。つまり、次のようです。

  • リスト A の長さは n として、A = (A1, ..., An) 。ここで、A1, ..., An は論理式。

S0 は、論理式をデータとする演繹システムだとして、|-S0 A は次の意味です。

  • 論理式 A は、演繹システム S0 により証明可能である。

同じことですが、

  • 演繹システム S0 は、論理式 A を証明できる／できた。

ターンスタイル記号 '|-S0' の左側にリストを置いてもかまいません。A |-S0 B は次の意味です。

  • 論理式 B は、リスト A に含まれる論理式を前提とすれば、演繹システム S0 により証明可能である。

同じことですが、

  • 演繹システム S0 は、リスト A に含まれる論理式を前提として、論理式 B を証明できる／できた。

さて、もうひとつの演繹システム S1 があって、こっちはシーケントをデータとして扱うとします。シーケントは、A→B の形に書くと約束します。A, B はリストだったので、A1, ..., An→B1, ..., Bm のように書いても同じです（リストを囲む丸括弧は省略しています）。話を簡単にするために、シーケントの右辺〈結論部分〉はひとつの論理式だとしましょう。つまり、A1, ..., An→B の形だけを扱います。

メタな表現 ||-S1 A→B は次の意味です。

  • シーケント A→B は、演繹システム S1 により証明可能である。

同じことですが、

  • 演繹システム S1 は、シーケント A→B を証明できる／できた。

'|-' も '||-' も、意味は証明可能なので、同じ記号でもいいのですが、あえて二種類のメタ記号を導入したのは、「論理式をデータとするシステムの証明可能性」と「シーケントをデータとするシステムの証明可能性」を区別するためです。メタ記号 '|-' は、「論理式をデータとするシステムの証明可能性」を表し、メタ記号 '||-' は、「シーケントをデータとするシステムの証明可能性」を表します*2。

シーケントを、α, β などのギリシャ文字小文字で表し、シーケントのリストは α, β などの下線付きギリシャ文字小文字で表すことにします。シーケント A→B を一文字 α で表すと、メタな表現 ||-S1 A→B は、||-S1 α と書けます。

シーケントのリスト α とシーケント β に関して、α ||-S1 β は次の意味です。

  • シーケント β は、リスト α に含まれるシーケントを前提とすれば、演繹システム S1 により証明可能である。

同じことですが、

  • 演繹システム S1 は、リスト α に含まれるシーケントを前提として、シーケント β を証明できる／できた。

演繹定理

演繹定理〈deduction theorem〉は、定理と呼ばれてはいますが、演繹システムに要求される性質です。S0 が論理式をデータとする演繹システムの場合、S0 が演繹定理は満たすとは、次の2つの条件が成り立つことです。形式化された記号 '⊃' は含意記号です。

  • A1, ..., An |-S0 B ならば、A1, ..., An-1 |-S0 An⊃B
  • A1, ..., An-1 |-S0 A⊃B ならば、A1, ..., An-1, A |-S0 B

S1 がシーケントをデータとする演繹システムの場合は、演繹定理の記述は少し複雑化します。最初に、シーケントの左辺を空（からっぽ）に変換できることを見ておきます*3。一般的なアルゴリズムを述べるのは面倒なので、一例で察してください。「因数分解できれば2次方程式は解ける」を意味するシーケント (a, b∈R), (x∈R), (x - a)(x - b) = 0 → x = a ∨ x = b を例にします。

  1. 与えられたシーケント：
    (a, b∈R), (x∈R), (x - a)(x - b) = 0 → x = a ∨ x = b
  2. 左辺の論理式を含意の前件にして右辺に移動する：
    (a, b∈R), (x∈R) → (x - a)(x - b) = 0 ⊃ x = a ∨ x = b
  3. 自由変数の型宣言を全称限量子にして右辺に移動する：
    (a, b∈R) → ∀x∈R.( (x - a)(x - b) = 0 ⊃ x = a ∨ x = b )
  4. さらに、自由変数の型宣言を全称限量子にして右辺に移動する：
    → ∀a, b∈R.( ∀x∈R.( (x - a)(x - b) = 0 ⊃ x = a ∨ x = b ) )

こうしてできたシーケントを右片側シーケント〈right one-sided sequent〉と呼びます。シーケント α から作った右片側シーケントを →RHS(α) と書くことにします。RHS は Right Hand Side の略記です。今の例では、RHS は次のようです。

  • RHS("(a, b∈R), (x∈R), (x - a)(x - b) = 0 → x = a ∨ x = b") = "∀a, b∈R.( ∀x∈R.( (x - a)(x - b) = 0 ⊃ x = a ∨ x = b ) )"

では、RHS を使って、シーケントをデータとする演繹システム S1 に関する演繹定理を述べましょう。S1 が演繹定理は満たすとは、次の2つの条件が成り立つことです。

  • α1, ..., αn ||-S1 B1, ..., Bm→C ならば、α1, ..., αn-1 ||-S1 RHS(αn), B1, ..., Bm→C
  • α1, ..., αn-1 ||-S1 A, B1, ..., Bm→C ならば、α1, ..., αn-1, →A ||-S1 B1, ..., Bm→C

互換な2つの演繹システム

S0 と S1 は、前節で述べたような演繹システムで、どちらも演繹定理を満たすとします。さらに、S0 と S1 が次の2つの条件を満たすとき、S0 と S1 は互換〈compatible〉であるということにします*4。

  • A1, ..., An |-S0 B ならば、||-S1 A1, ..., An→B
  • ||-S1 A1, ..., An→B ならば、A1, ..., An |-S0 B

ゲンツェンのシステムに限らず、自然演繹風システムとシーケント計算風システムが互換になる例は色々と作れます。互換な演繹システム S0, S1 があると、証明可能性に関するメタな記述が色々な形に言い換えられます。次の7つのメタな表現は、メタな命題として同値です。

  1. |-S0 (A∧B)⊃C
  2. |-S0 A⊃(B⊃C)
  3. A |-S0 B⊃C
  4. A, B |-S0 C
  5. ||-S1 A, B → C
  6. →A ||-S1 B → C
  7. →A, →B ||-S1 → C

こうした状況を背景にして、（ほんとはやってはいけないのですが）形式化された記号とメタ記号をゴッチャにして使うことがあります。

演繹システム S0, S1 は了解されているとして省略すれば：

  1. |- (A∧B)⊃C
  2. |- A⊃(B⊃C)
  3. A |- B⊃C
  4. A, B |- C
  5. ||- A, B → C
  6. →A ||- B → C
  7. →A, →B ||- → C

'|-' の代わりに '→'、'||-' の代わりに '⇒' を使うと：

  1. → (A∧B)⊃C
  2. → A⊃(B⊃C)
  3. A → B⊃C
  4. A, B → C
  5. ⇒ A, B → C
  6. →A ⇒ B → C
  7. →A, →B ⇒ → C

ここらへんまでは、なんとか推測して（メタな意味で）判読可能ですが、含意記号 '⊃' にも '⇒' を使うと：

  1. → (A∧B) ⇒ C
  2. → A ⇒ (B ⇒ C)
  3. A → B ⇒ C
  4. A, B → C
  5. ⇒ A, B → C
  6. →A ⇒ B → C
  7. →A, →B ⇒ → C

これら7つの表現の意味や違いを正しく判読するのは困難になります。これはワザと作った悪例ですが、程度の差はあれ、判読困難なレベルでイイカゲンな書き方はあるので注意してください。

最後にもう一度繰り返しますが、次のような“矢印っぽい”記号の意味と使用法はまったく安定してないので、毎回定義を確認する必要があります。

  • '→'
  • '⇒'
  • '|-'

この注意は、檜山のこのブログにも適用されます。これら3つの矢印は、どれもシーケントの区切り記号に使ったことがあります。'⇒' は、形式化された含意記号にも、メタな意味的帰結〈semantic consequence〉にも使ったことがあります。記事の内容・目的やそのときの気分で変わってしまうんですわ、あしからず。

*1:「伴意」の読み方に関しては「伴意は「ばんい」じゃなくて「はんい」と読む」に書いてあります。「はんい」と読む人がいますが、結局僕は「ばんい」と読んでいます。

*2:ひとつの演繹システムが、論理式モードとシーケントモードを持っているような状況も考えられますが、そのときは、'|-' と '||-' がそれぞれのモードでの証明可能性を表します。

*3:左辺を空にしたシーケントを同値とみなすことが、演繹定理の内容を含んでいます。

*4:論理のモデルをデカルト閉圏 C に取ると、S1 のシーケントは C を射を記述し、S0 の推論図／証明図が終対象からの射を記述していることになります。