演繹システムの論理パート

我々の演繹システムは、論理パートと分野固有パートに分かれる。分野固有パートは色々と取り替えるが、論理パートは分野に関わらず同じモノを使う。ここでは、共通に使う論理パートを定義する。

TBD (To Be Described/Determined/Defined) の部分は、追加予定。

演繹システムの論理パートはどのようにして定義されるのか

論理パートは、組み込み〈基本 | プリミティブ〉推論の集合と、組み込み〈基本 | プリミティブ〉リーズニングの集合により定義される。

16個の組み込み推論（16 = 1 + 1 + 7×2）
9個の組み込みリーズニング（9 = 3 + 6）
置き換えの操作を伴う組み込み推論 TBD

16個の組み込み推論のうち9個は可逆で、6個は逆方向にして形が変わるので、方向を分けて勘定すると22個の組み込み推論になる。

9個の組み込みリーズニングのうち3個は暗黙に仮定されることが多く、6個を意識的に使うことになる。 9個の組み込みリーズニングのうち5個は可逆で、4個は逆方向にして形が変わるので、方向を分けて勘定すると13個の組み込みリーズニングになる。

組み込み推論と組み込みリーズニングを最小にすることは意図してない。現存するほとんどの演繹システムは冗長（頑張ればもっと小さく出来るように）に作られている。冗長性を排除すると、（ときに実用に耐えないほどに）使いにくくなる。したがって、組み込み推論と組み込みリーズニングが何個あるかは、あまり気にするポイントではない。

組み込み推論の概要

何もしない自明な推論 1つ
モーダスポネンス 1つ
連言系統の推論 7つ
選言系統の推論 7つ

推論の名称に使用する文字の謂れ

番号	記号	由来	備考
1	!	たぶん唯一性から ∃! と同じ由来	これだけギリシャ文字ではない
	θ	0に似てるから	使わない、*!と書く
2,3	π	projectionのp
	ι	injectionのi	使わない、*πと書く
4	Δ	diagonalのd、それと形状の類似
	λ	leftのl	使わない、導出できる
5	ρ	rightのr（rh）
	α	associativeのa	使わない、導出できる
6	σ	symmetryのs, symmetry = permutation
7	γ	conjunctionとconstructorのc、だが注記参照
	δ	distributiveのd	使わない、導出できる
-	ε	evalのe

※注記： γはcには対応しない。gに対応。だが、三番目に登場するのでcの代わりにγが使われることがある。

自明な推論と最も有名な推論

組み込み推論は、命題総称な〈命題パラメータを持つ〉シーケントとして記述する。命題総称の命題パラメータは山形括弧内に入れる。命題パラメータを持つ推論は推論規則とか推論パターンとも呼ばれる。

推論規則〈命題総称な推論 | 推論パターン〉の命題パラメータは、任意の論理式を代入して具体化してよい。推論規則の正しさは、次のように検証または保証される。

命題パラメータにどんな論理式を代入したシーケントも、スコット・ブラケットによる解釈で正しい。

id<A>:A ↔ A （自明な推論、↔は可逆なことを示す）
ε<A, B>:A, A⇒B → B （モーダスポネンス）

あるいは、

A -(id<A>)→ A （可逆）
A, A⇒B -(ε<A, B>)→ B

あるいは、

1.
   A
  ----↑ id<A> （上向き矢印は可逆なことを示す）
   A

2.
   A  A⇒B
  --------- ε<A, B>
      B

あるいはノード・ワイヤー図（描いてない TBD）。

自明な推論は、組み込み推論のなかで、おそらく最も解釈が容易な推論（命題総称な推論）である。
自明な推論は、あまりに当たり前なので、組み込み推論としてカウントしないことがある。
モーダスポネンスは、組み込み推論のなかで、おそらく最も解釈が困難な推論（命題総称な推論）である。とはいえ、我々は当たり前だと思っている。

連言に関わる推論

「↔」で書いてある推論は両方向に適用できる。4, 5, 7は逆方向にすると形が変わる。

!<A>:A → T
π[1]<A, B>:A∧B → A
π[2]<A, B>:A∧B → B
Δ<A>:A ↔ A, A
ρ:A, T ↔ A
σ<A, B>:A, B ↔ B, A
γ<A, B>:A, B ↔ A∧B

これらの組み込み推論の意味を一言で表現すれば：

1. どんな命題からも、真命題は出る。
2, 3. 2つの命題の連言から、その片方は出る。
1. 命題を、連言的に複製しても（縮約しても）よい。
1. 真命題は、連言的に挿入・削除してよい。
1. 連言的なリストの、順番を変えてもよい。
1. 連言的なリストから、連言命題を作っても（その逆をしても）よい。

横棒記法で書けば（可逆なものは↑でマークしている）：

1. !:A → T

    A
   ---- !<A>
    T

2. π[1]:A, B → A

    A  B
   ------π[1]<A, B>
     A

3. π[2]:A, B → B

    A  B
   ------ π[2]<A, B>
     B

4. Δ:A → A, A

     A
   -----↑ Δ<A>
   A  A

5. ρ:A, T → A

   A  T
  ------↑ ρ<A>
    A

6. σ:A, B → B, A

    A   B
   -------↑ σ<A, B>
    B   A

7. γ:A, B → A∧B

    A   B
   -------↑ γ<A, B>
     A∧B

Δ<A> の逆 Δ'<A>:A, A → A だけは論理固有で、他の推論規則は、関数型プログラミングの組み込み総称関数として使える。例えばγは、型Aと型Bの2つのデータを受け取って、それらのペア（型はA×B）を返す型総称関数となる。

問題：集合Xに対するベキ集合Pow(X)内で、上記の7つの推論を、∩と⊆に関する法則として解釈せよ。

選言に関わる推論

矢印の向きを逆にして、T←→⊥、∧←→∨、,←→| を入れ替えた形を双対な推論と呼び、もとの推論の名前に'*'を前置して示すことにする。

*!<A>:⊥ → A
*π[1]<A, B>:A → A∨B
*π[2]<A, B>:B → A∧B
*Δ<A>:A | A ↔ A
*ρ:A ↔ A | T
*σ<A, B>:A | B ↔ B | A
*γ<A, B>:A∨B ↔ A | B

これらの組み込み推論の意味を一言で表現すれば：

1. 偽命題からは、どんな命題も出る。
2, 3. 1つの命題から、その命題を含む選言は出る。
1. 選言的に重複した命題を、縮約しても（逆に複製しても）よい。
1. 偽命題は、選言的に挿入・削除してよい。
1. 選言的なリストの、順番を変えてもよい。
1. 選言命題から、選言的リスを作っても（その逆をしても）よい。

*Δ<A> の逆 *Δ'<A>:A → A | A だけは論理固有で、他の推論規則は、関数型プログラミングの組み込み総称関数として使える。ただし、（タグ付きユニオン型とは別に）選言的リストに相当する概念（選言的引数リスト、選言的多値戻り値）を実装しているプログラミング言語が（たぶん）ない。

問題：集合Xに対するベキ集合Pow(X)内で、上記の7つの推論を、∪と⊆に関する法則として解釈せよ。

導出できる推論

次の推論は、最初からシステム組み込みにしてもいいが、入れなくても導出できる。導出は、他の組み込み推論から始めてリーズニングを行う。

λ:T, A ↔ A
*λ: A ↔ ⊥ | A
δ:A, B∨C ↔ A∧B | A∧C
*δ:A∨B, A∨C ↔ A | B∧C
α:(A∧B)∧C ↔ A∧(B∧C)
*α:A∨(B∨C) ↔ (A∨B)∨C

組み込みとしているπ[1]も、実際は導出できる。

   A         B
  ---id<A>  ---!<B>
   A         T
 =========+======= Conj
       A  B              A  T
      ------            ------ρ<A>
       A  T               A
     ==============+=============== Comp
                A  B
               ------ 導出されたπ[1]<A, B>
                 A

π[1]は伝統的に有名な推論なので、組み込みとしている。推論を組み込みとして採用するかどうかの判断は、使い勝手とシステム設計者の好み〈趣味嗜好〉による。

置き換えを伴う組み込み推論

TBD

組み込みリーズニングの概要

暗黙に仮定される場合が多いリーズニング：

名称	キーワード	別名
恒等リーズニング	Id	自明{な}?リーズニング
複製リーズニング	Dup
破棄リーズニング	Dis

※ Dis は discard〈破棄する〉、dispose〈処分する〉から。

これらの暗黙的リーズニングの使い方は後で述べる。

明示的・意図的に使われるリーズニングは次の6つと、逆が3つである。

番号	名称	演算子記号	キーワード	別名
1	結合リーズニング	;	Comp	フルカット
2	連言リーズニング	⊗	Conj	連言的併置
3	選言リーズニング	⊕	Disj	選言的併置
4	ダイアモンド・リーズニング	◇	Diam	右連言導入, 右全称導入
5	スクエア・リーズニング	□	Squr	左選言導入, 左存在導入
6	ラムダ・リーズニング	Λ	Lamb	右含意導入
	ダイアモンド・リーズニングの逆	◇'	Diam'	右連言除去, 右全称除去
	スクエア・リーズニングの逆	□'	Squr'	右選言除去, 右存在除去
	ラムダ・リーズニングの逆	Λ'	Lamb'	右含意除去

組み込みリーズニングの記述

リーズニング規則（推論総称なリーズニング）を、横書き1行のテキストで表現するのは困難であるが、次の約束のもとでテキスト表現してみる。

Γ, Δ, Σ, Π は命題のリストを表す。連言的リストであるか、選言的リストであるかは場合による。
-○→ は、そこに何らかの推論図があることを示す。ただし、-○→ の出現ごとに、その内容は変わるかもしれない。
単なる矢印 → はケーブルの存在（空ケーブルかも知れない）を示すだけで、そこに推論図が在るわけではない。
(x∈X| … ) は、コンテキスト・ボックスを示す。
一番外側のコンテキスト・ボックスは省略して書かない。
リーズニングの名前は、=(名前)▷ の形で書く。

以上の約束で記述するが、なにかと無理があること（テキスト表現は破綻していること）は承知しておいてくださいな。

Γ-○→Δ　 Δ-○→Σ =(Comp)▷ Γ-○→Σ
Γ-○→Δ　 Σ-○→Π =(Conj)▷ Γ, Σ -○→ Δ, Π
Γ-○→Δ　 Σ-○→Π =(Disj)▷ Γ | Σ -○→ Δ | Π
Γ→(x∈X| A -○→ B[x]) =(Diam)▷ Γ, A-○→∀x∈X.B[x] （可逆）
Γ→(x∈X| A[x] -○→ B) =(Squa)▷ Γ, ∃x∈X.A[x] -○→ B （可逆）
A, Γ -○→ B | Δ =(Lamb)▷ Γ -○→ A⇒B | Δ （可逆）

よく使われる簡略な形：

4の簡略形： Γ→(x∈X| -○→ B[x]) =(Diam)▷ Γ -○→∀x∈X.B[x] （可逆）
6の簡略形： A, Γ -○→ B =(Lamb)▷ Γ -○→ A⇒B （可逆）

横棒記法で書けば（可逆なものは△でマークしている）：

1. フルカット

  Γ   Δ
  --   --
  ○   ○
  --   --
  Δ   Σ
 ====+==== Comp
    Γ
    --
    ○
    --
    Σ

2. 連言的併置

  Γ    Σ
  --    --
  ○    ○
  --    --
  Δ    Π
 =====+==== Conj
   Γ Σ
  -------
    ○
  -------
   Δ Π

3. 選言的併置

  Γ   Σ
  --   --
  ○   ○
  --   --
  Δ   Π
 ====+==== Disj
  Γ | Σ
  ---|---
    ○
  ---|---
  Δ | Π

4. 右(下側)全称導入

   Γ
  +-(x∈X)--
     A
    ---
     ○
    ----
    B[x]
  +--------
 ===============△ Diam
     Γ  A
     -------
       ○
   -----------
   ∀x∈X.B[x]

4s. 簡略形 右(下側)全称導入

   Γ
  +-(x∈X)--
     ○
    ----
    B[x]
  +--------
 ==============△ Diam
      Γ
    -------
      ○
  ------------
   ∀x∈X.B[x]

5. 左(上側)存在導入

  Γ
  +-(x∈X)---
    A[x]
    -----
     ○
    ----
     B
  +---------
 ================== △ Squa
  Γ ∃x∈X.A[x]
  --------------
     ○
    -----
     B

6. 右(下側)含意導入

   A  Γ
   ------
    ○
   ------
   B | Δ
 =========△ Lamb
    Γ
   ----
    ○
  ---------
  A⇒B | Δ


6s. 簡略形 右(下側)含意導入

   A  Γ
   -----
    ○
   ----
    B
 =========△ Lamb
    Γ
   ----
    ○
   -----
   A⇒B

リーズニングによって構成される推論式を添えればより明確になる。

リーズニング規則〈推論総称なリーズニング〉の推論パラメータは、《》のなかに記す。
空白は、単なる余白と、推論の区切りと、連言的リストの連接演算、連言的リスト内の区切り、の意味がある。
推論図を代表する名前（推論変数）は、プロファイル込みである。プロファイルを切り離した推論という概念はない。
<X> は、◇の内部にXのこと。
[X] は、□の内部にXのこと。

繰り返し言うが、テキスト表現では限界があり、色々と問題もあることを承知しておいてくださいな。

1. フルカット

  Γ   Δ
  --   --
  F    G
  --   --
  Δ   Σ
 ====+==== Comp《F:Γ→Δ, G:Δ→Σ》
    Γ
    --
   F;G
    --
    Σ

2. 連言的併置

  Γ    Σ
  --    --
  F     G
  --    --
  Δ    Π
 =====+==== Conj《F:Γ→Δ, G:Σ→Π》
   Γ Σ
  -------
    F⊗G
  -------
   Δ Π

3. 選言的併置

  Γ   Σ
  --   --
  F    G
  --   --
  Δ   Π
 ====+==== Disj《F:Γ→Δ, G:Σ→Π》
  Γ | Σ
  ---|---
    F⊕G
  ---|---
  Δ | Π

4. 右(下側)全称導入

   Γ
  +-(x∈X)--
     A
    ---
     F
    ----
    B[x]
  +--------
 ===============△ Diam《X Set, F:Γ, A→B》
     Γ  A
    -------
     <X>F
   ------------
   ∀x∈X.B[x]

4s. 簡略形 右(下側)全称導入

   Γ
  +-(x∈X)--
     F
    ----
    B[x]
  +--------
 ==============△ Diam《X Set, F:Γ→B》
      Γ
    -------
    <X>F
  ------------
   ∀x∈X.B[x]

5. 左(上側)存在導入

  Γ
  +-(x∈X)---
    A[x]
    -----
     F
    ----
     B
  +---------
 ================== △ Squa《X Set, F:Γ, A→B》
  Γ ∃x∈X.A[x]
  --------------
     [X]F
    -----
     B

6. 右(下側)含意導入

   A  Γ
   ------
    F
   ------
   B | Δ
 =========△ Lamb《F:A, Γ→B | Δ》
    Γ
   ----
    ΛF
  ---------
  A⇒B | Δ


6s. 簡略形 右(下側)含意導入

   A  Γ
   -----
    F
   ----
    B
 =========△ Lamb《F:A, Γ→B》
    Γ
   ----
    ΛF
   -----
   A⇒B

組み込みリーズニングのプロファイルは次のように書ける（書き方の約束は省略）。

Comp:: (α| Γ→Δ), (α| Δ→Σ) =▷ (α| Γ→Σ)
Conj:: (α| Σ→Δ), (α| Σ→Π) =▷ (α| Γ, Σ → Δ, Π)
Disj:: (α| Γ→Δ), (α| Σ→Π) =▷ (α| Γ | Σ → Δ | Π)
Diam:: (α| Γ→(x∈X| A → B[x])) ◁=▷ (α| Γ, A →∀x∈X.B[x])
Squa:: (α| Γ→(x∈X| A[x] → B)) ◁=▷ (α| Γ, ∃x∈X.A[x] → B)
Lamb:: (α| A, Γ → B | Δ) ◁=▷ (α| Γ → A⇒B | Δ)

暗黙のリーズニングとリーズニング演算子／リーズニング式

次のリーズニングは組み込みである。

恒等（可逆）
      Γ
      --
      ○
      --
      Δ
    ======△ Id
      Γ
      --
      ○
      --
      Δ
 
複製（可逆）
      Γ
      --
      ○
      --
      Δ
  ====+====△ Dup
   Γ   Γ
   --   --
   ○   ○
   --   --
   Δ   Δ
 
破棄
      Γ
      --
      ○
      --
      Δ
    ====== Dis
      ☆

論理計算が難しいのは、操作対象となるオペランドと、操作を行うオペレーターが何階層にも渡って存在し、それぞれの階層が類似していたり少し違ったりしていて、混乱・混同が起きやすいからである。

階層の最上位にあるオペランドはリーズニングであり、最上位のオペレーターは、

リーズニングを直列結合するオペレーター *
リーズニングを並列結合するオペレーター +

記号を使い果たしているので、算術オペレーターを再利用することにする。

組み込みリーズニングから始めて、リーズニングオペレーターである *, + で組み上げた式がリーズニング式であり、リーズニング図のテキスト表現になる。

組み込み推論をリーズニングの先頭（始まりの部分）に置くときは、

      ☆
  =========== Ent
 組み込み推論

※ Entは、enter, entrance, entry のent、登場。

推論／リーズニングが持つ総称パラメータを具体化する代入〈substitution〉は、

     推論
 ============= Subst 代入
  代入後の推論

あらゆる論理的概念は、最終的にリーズニング図（＝リーズニング式）により正しさが保証される。そのリーズニング図（＝リーズニング式）を組み上げる元になるプリミティブは：

Comp, Conj, Disj, Diam, Squa, Lamb という6つの組み込みリーズニング。このうち、Diam, Squre, Lamb は可逆。
Id, Dup, Disc という3つの組み込みリーズニング。Id, Dup は可逆。
組み込みの推論、または登録済みの推論の導入・登場である Ent
推論が持つパラメータを置き換える代入

リーズニング図の構成図

推論図（命題の構成図）は、命題のあいだの関係、あるいは命題の構成手順を描いた図
リーズニング図（＝推論図の構成図＝命題の構成図の構成図）は、推論図のあいだの関係、あるいは推論図の構成手順を描いた図
リーズニング図の構成図（＝推論図の構成図の構成図＝命題の構成図の構成図の構成図）は、リーズニング図のあいだの関係、あるいはリーズニング図の構成手順を描いた図

リーズニング図の構成図の横棒記法による図は：

横棒記法は三本棒、テキストなら'≡'を並べる。
横棒のラベルは、リーズニングに対する操作であり、COMP（リーズニングの直列結合）、PROD（リーズニングの並列結合／積／併置）、DUP（リーズニングの複製）、DIS（リーズニングの破棄）