2017-08-18

用語法を注意しないといけない。

証明：順方向証明か逆方向証明か曖昧
証明：証明オブジェクトかリーズニングか曖昧
証明図：自然演繹の証明図かシーケント計算の証明図か曖昧
自然演繹の証明図：テキスト証明図かピクチャー証明図か曖昧

基本的に証明は自然演繹の証明図の意味で使う。

証明図＝自然演繹の証明図＝{自然演繹のテキスト証明図 | 自然演繹のピクチャー証明図}

証明図は混合証明図なので、順方向と逆方向の区別はしない（一緒に考える）が、次の用語を使う。

導出推論図：アトミックな順方向証明図 derivation デリベーション
還元推論図：アトミックな逆方向証明図 reduction, resolution

推論図＝{導出推論図 | 還元推論図}＝{{導出ピクチャー推論図 | 導出テキスト推論図} | {還元ピクチャー推論図 | 還元テキスト推論図}}

証明図は推論図の組み合わせになる。

導出証明図：導出推論図だけからなる証明図
還元証明図：還元推論図だけからなる証明図

規則＝推論規則＝{導出推論規則 | 還元推論規則}＝{{導出推論 | 導出規則} | {還元推論 | 還元規則}}

一般の証明図は、導出証明図でも還元推論図でもなくて、それらの混合物（mixture）。

証明図＝{導出証明図 | 還元推論図 | 混合証明図}

リーズニングとは、証明図の変形過程。既にある証明図に推論図をアタッチするだけのこともあれば、証明図を全面的に書き換えることもある。リーズニングのアトミックな過程を基本リーズニングと呼び、基本リーズニング図で描く。

証明	リーズニング
命題＝論理式	証明
推論＝基本証明	基本リーズニング
一般の証明	一般のリーズニング
証明の生成方法	リーズニングの生成方法

次のような対応関係がある。

項	論理式	証明
敵数記号と関数記号	項と述語記号	論理式と規則記号
基本項（関数の適用）	基本論理式（述語の適用）	基本証明（規則の適用）
一般の項	一般の論理式	一般の証明
項の生成方法	論理式の生成方法	証明の生成方法

これを考慮すれば：

証明	リーズニング	メタリーズニング
論理式と規則記号	証明とメタ規則記号	リーズニングとメタメタ規則記号
基本証明（規則の適用）	基本リーズニング（メタ規則の適用）	基本メタリーズニング
一般の証明	一般のリーズニング	一般のメタリーズニング
証明の生成方法	リーズニングの生成方法	メタリーズニングの生成方法

シーケントの書き方は：

シーケント＝証明のプロファイル記述： f:Γ→Δ （fは証明、Γ, Δは命題列）
メタシーケント＝リーズニングのプロファイル記述：α::f⇒g:Γ→Δ （αはリーズニング）

メタ規則：

( $\otimes$ )：テンソル積＝モノイド積
(∪←A)：右左カップ結合
(∪→A)：左右カップ結合
(∩←A)：右左キャップ結合
(∩→A)：左右キャップ結合
(／↓A)：下スラッシュ結合
(／↑A)：上スラッシュ結合
(＼↓A)：下逆スラッシュ結合
(＼↑A)：上逆スラッシュ結合
(;)：全結合
(^s)：置換後結合
(s^)：置換前結合
(*)：転置

メタ規則の適用パターンの図がメタ規則図＝メタ推論図、区切り記号に'='を使用。シーケント矢印は'⇒'。

メタメタ規則：

エレベーター規則
恒等規則
結合規則
ニョロニョロ規則
転置規則

メタメタ規則の適用パターンの図がメタメタ規則図＝メタメタ推論図、区切り記号に'≡'を使用。シーケント矢印は'≡>'。

次元を使ったネーミング：

n	n-規則	n-リーズニング区切り	n-シーケント矢印	変数
0	推論規則	証明 --	シーケント →	命題変数
1	メタ推論規則	リーズニング ==	メタシーケント ⇒	証明変数
2	メタメタ推論規則	メタリーズニング ≡≡	メタメタシーケント ≡>	リーズニング変数

使う変数は：

無向命題変数
有向命題変数
タプル無向命題変数
タプル有向命題変数
証明変数
タプル証明変数＝マルチスレッド証明変数
リーズニング変数
タプルリーズニング変数＝マルチスレッド・リーズニング変数

自然演繹の欠点を克服したい。
自然演繹とシーケント計算を別々に扱うのではなくて、融合・統合して一体として扱いたい。
証明オブジェクトと証明オブジェクトの操作であるリーズニングを区別したい。そして、曖昧性を排除したい。
人間が通常行っている混合証明／混合リーズニング（混合証明オブジェクトの操作）を定式化したい。
特に、トンネル論法（両端から掘り進めて中間地点で出会う）を合理化したい。
アブダクションの定式化をしたい。
科学的帰納法など、科学的論理の定式化をしたい。

ちなみに、トンネルで片方から掘るのは「片押し」と言うらしい。両側から掘る際の誤差は、2016年6月開通のスイス「ゴッタルドベーストンネル」（全長57km、現在世界最長の鉄道トンネル）の出会い時の誤差は8cm程度とのこと。すげーな。

[Γ→Δ],[Π→Σ]⇒Γ,Π→Δ,Σ Γ→Δ Π→Σ ===============(×) Γ,Π→Δ,Σ [Γ→Δ,A], [A,Π→Σ]⇒[Γ,Π→Δ,Σ] (A has ↓) Γ→Δ,A A,Π→Σ ====================(＼↓A) Γ,Π→Δ,Σ [Γ→Δ,A],[Π→A*,Σ]⇒[Γ,Π→Δ,Σ] (A has ↓) Γ→Δ,A Π→A*,Σ ======================(∪→A) Γ,Π→Δ,Σ

[Γ→Δ],[Π→Σ]⇒Γ,Π→Δ,Σ before Γ Π --- --- : : : : --- --- Δ Σ after Γ,Π ------ : : ------ Δ,Σ [Γ→Δ,A], [A,Π→Σ]⇒[Γ,Π→Δ,Σ] before (A has ↓) Γ A,Π ---- ---- : : : : ---- ---- Δ,A Σ after Γ,Π ----- : : ----- Δ,Σ [Γ→Δ,A],[Π→A*,Σ]⇒[Γ,Π→Δ,Σ] before (A has ↓) Γ Π --- --- : : : : ---- ----- Δ,A A*,Σ after Γ,Π ----- : : ----- Δ,Σ

[Γ→Δ,A], [A,Π→Σ]⇒[Γ,Π→Δ,Σ] before (A has ↓) Γ : --- : : : : : ---- : Δ,A : : A,Π : ---- : : : : : ---- : Σ after Γ,Π ----- : : ----- Δ,Σ

(保存用) 檜山正幸のキマイラ飼育記メモ編

混合証明、(メタ)リーズニング、コンパクト有向(メタ)シーケント

コンパクト有向シーケント計算／高次シーケント計算の動機

コンパクト有向シーケント計算の規則