いくつかの事例、シーケント推論図の形式： [Γ→Δ],[Π→Σ]⇒Γ,Π→Δ,Σ Γ→Δ Π→Σ ===============(×) Γ,Π→Δ,Σ [Γ→Δ,A], [A,Π→Σ]⇒[Γ,Π→Δ,Σ] (A has ↓) Γ→Δ,A A,Π→Σ ====================(＼↓A) Γ,Π→Δ,Σ [Γ→Δ,A],[Π→A*,Σ]⇒[Γ,Π→Δ,Σ] (A has ↓) Γ→Δ,A Π→A*,Σ =========…

自然演繹の欠点を克服したい。 自然演繹とシーケント計算を別々に扱うのではなくて、融合・統合して一体として扱いたい。 証明オブジェクトと証明オブジェクトの操作であるリーズニングを区別したい。そして、曖昧性を排除したい。 人間が通常行っている混合…

用語法を注意しないといけない。 証明： 順方向証明か逆方向証明か曖昧 証明： 証明オブジェクトかリーズニングか曖昧 証明図： 自然演繹の証明図かシーケント計算の証明図か曖昧 自然演繹の証明図： テキスト証明図かピクチャー証明図か曖昧 基本的に証明は…