証明関係の画像

半形式証明スクリプト 論理 画像

MP導出の図を向きを変える。



スタックとリストの関係と等式の証明


計算図



リーズニング図



紙芝居方式リーズニング図

リーズニング図の同値変形



分岐合流紙芝居方式リーズニング図


線形証明とグラフ証明図とツリー証明図

連言リストと宣言リスト、α, β は論域。

論域をストライプやボックスで表す。

定理と証明の構造

演繹システム (4)

muses 論理 半形式証明スクリプト
  1. 演繹システム - (新) 檜山正幸のキマイラ飼育記 メモ編
  2. 演繹システム (2) - (新) 檜山正幸のキマイラ飼育記 メモ編
  3. 演繹システム (3) - (新) 檜山正幸のキマイラ飼育記 メモ編

$`\newcommand{\derive}{ \vdash }%
\newcommand{\deduce}{ \mathop{\|\!-} }%
\newcommand{\afford}{ \mathrel{\|} }%
\newcommand{\Sign}[1]{ \mathscr{#1} }
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\In}{ \text{ in } }
\newcommand{\ImpL}{ \Leftarrow }
\newcommand{\sto}{ \longrightarrow }
%`$次は同じ意味。

  • $`\mathscr{L} \deduce_\mathscr{D} \Gamma \sto B`$
  • $`\mathscr{L}, \hat{\Gamma} \deduce_\mathscr{D} (,) \sto B`$
  • $`\mathscr{L}, \hat{\Gamma} \deduce_\mathscr{D} (\vdash B)`$

圏論的論理のチュートリアル - (新) 檜山正幸のキマイラ飼育記 メモ編 によれば、次も同じ意味。

  • $`\Gamma \mid \Xi \vdash \psi`$

少し違う点／同じ点は、

  • $`\Gamma`$ は型コンテキストで論理式を含まない。$`\mathscr{L}`$ は型コンテキストだけでなく、論理式を含んでもよい。
  • $`\Xi \vdash \psi`$ と $`\Gamma \sto B`$ は（書き方以外）まったく同じ。
  • $`\Xi`$ を $`\Phi, \Psi`$ に分解して、$`\Gamma \mid \Phi, \Psi \vdash \psi`$ と書いて、一部の論理式を移動して、$`\Gamma, \Phi \mid \Psi \vdash \psi`$ とすれば同じになる。

圏論的論理のチュートリアル

muses 半形式証明スクリプト 論理 課題

これは良いチュートリアルのように思えるが、「ゴッチャにした記述」が気になる。

typing rule として次の3つがある。

  1. （構文的）項の構成規則と対応するプロファイルの決定規則： プロファイルの決定規則に注目して typing rule と呼んでいるようだ。
  2. （意味論的）シング（意味的存在物）の構成規則とシングのアビタ決定規則： とある構成に関してアビタが閉じていることが背景にある。
  3. 文法の生成規則と構文範疇の決定規則： 構文的な構成で記号表現〈項 | 式〉の作り方と、構文範疇の計算法

文法がらみは {syntax | syntactic{al}?} {formation | forming} rule のこと。構文範疇と型は違うが、しばしば混同される。p.4 の Figure 2 を typing rule と呼ぶのは酷すぎる。これは、論理式の文法生成規則。論理式が表すシングがPropと呼ばれるアビタに棲んでいる。

それに対して、p.3 Figure 1 は、デカル閉圏をアビタ（セマンティック背景圏）とする項〈式 | テキスト・コンビネーション〉の構成規則になっている。タイピング〈プロファイリング〉は構成に付随するオマケ的位置付け。セマンティクスを伴う項構成規則でプロファイルも計算可能な規則。

同義語
  • 関数 ＝ オペレーション ＝ 射 ＝ 1-射
  • 型 ＝ ソート ＝ 対象 ＝ 0-射
  • 関数名 ＝ 関数定数 ＝ オペレーション記号 ＝ 射ラベル ＝ 1-ラベル
  • 型名 ＝ 型定数 ＝ ソート記号 ＝ 対象ラベル ＝ 0-ラベル
  • しばしば 関数 ＝ 関数名、型 ＝ 型名
  • 基本型 ＝ 生成0-射
  • 基本関数 ＝ 生成1-射

例によって、次は同義。

  • {base | primitive | atomic | prime | built-in | simple} {type | sort | object} {symbol | name | constant}? = generating 0-morphism label
  • {base | primitive | atomic | prime | built-in | simple} {function | operation | morphism} {symbol | name | constant}? = generating 1-morphism label
項の構成規則

素材は：

  1. 生成0-射 1
  2. 生成1-射 I, X, Δ, !, π^1, π^2

オペレータは

  1. 直積 0-オペレータ（1-オペレータは無し）
  2. 指数〈ベキ乗 | 累乗 | 指数〉 0-オペレータ（1-オペレータは無し）
  3. ペアリング
  4. カリー化
  5. 反カリー化

詳細は DIDLで規則記述 - (新) 檜山正幸のキマイラ飼育記 メモ編

シーケント

当該チュートリアルのいい点は、シーケントの定義が明確な点だろう。シーケントは次の形に書かれる。

$`\quad \Gamma \mid \Xi \vdash \psi`$

Γは型コンテキストで、圏論的な指標になる。x:σ は x:1 → σ とみなすので、1-mor宣言がならぶことになる。型コンテキストとは限らない一般の指標をとってもいい。Γはセオリーを決めると言ってもいい。

Ξ は、論域が共通な命題〈論理式〉のリストで、

$`\quad \Xi = (\varphi_1, \cdots, \varphi_n)`$

したがって、シーケントの一部を抜き出すと、

$`\quad (\varphi_1, \cdots, \varphi_n) \vdash \psi`$

これは、命題の圏のプロファイル。シーケント全体としては、Γが定義する命題の圏のなかのプロファイルを意味する。そのプロファイルを持つ射 F が導出（通常「証明」とも呼ばれる）。X は論域。

$`\quad F : (\varphi_1, \cdots, \varphi_n) \to \psi \text{ on } X \text{ in }\mathrm{Prop}[\Gamma]`$

「シーケントが証明できる」とは、そのシーケント＝プロファイルを持つ導出が構成可能であること。

檜山の課題

p.40に自然演繹の規則が書いてある。これをチャンと圏論的・絵算的に書き換えて、最終的にDIDLで書く。

DIDLで規則記述

半形式証明スクリプト 論理 お絵描き

https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf の P.3 の11個の規則

  1. IDENTITY
  2. WEAKENING
  3. CONTRACTION
  4. EXCHANGE
  5. MULTI-COMPOSITION （もとは無名）
  6. PAIRING
  7. PROJ-1
  8. PROJ-2
  9. ABS
  10. APP
  11. UNIT（むしろTERMINALだろうが）

使う文は以下。

確認と取得

  • we have σ
  • we take σ at location L
  • we possess M:Γ → τ named f
  • we possess Γ → τ due-to M named f

新規導入

  • we get σ
  • we assert σ → τ due-to M named f

操作

  • we use post-compose g
  • we use pre-compose f
  • we use make-id
  • we use 操作 インデックス〈パラメータ〉
IDENTITY

象形文字 I

from wire-palette
we get σ
we use make-id
we assert σ → σ
WEAKENING

象形文字 !

we possess M:Γ → τ
we use pre-compose id[Γ], Delete[σ]
we assert Γ, σ → τ
CONTRACTION

象形文字 Δ

we possess M:Γ, σ, σ → τ
we use pre-compose id[Γ], Copy[σ]
we assert Γ, σ → τ
EXCHANGE

象形文字 X

we possess M:Γ, σ, σ' → τ
we use pre-compose id[Γ], Swap[σ, σ']
we assert Γ, σ', σ → τ
MULTI-COMPOSITION

記号 -(-, ..., -)

from node-palette
we assert F:τ_1, ‥‥, τ_n → τ'

we possess F:τ_1, ‥‥, τ_n → τ'
we possess M_1:Γ → τ_1
‥‥
‥‥
we possess M_n:Γ → τ_n
we use left multi-composition
we assert Γ → τ' due-to F(M_1, ..., M_n)
PAIRING

記号 < -, - >

we possess M:Γ → τ
we possess N:Γ → σ
we use pairing[Γ, τ, σ]
we aasert Γ → τ×σ du-to <M, N>
PROJ-1

記号 π^1

we possess M:Γ → τ×σ
we use post-compose proj-1[τ, σ]
we assert Γ → τ
PROJ-2

記号 π^2

we possess M:Γ → τ×σ
we use post-compose proj-2[τ, σ]
we assert Γ → σ
ABS

仮想ベンディング象形文字 ∩

we possess M:Γ, σ → τ
we use curry[Γ, σ, τ]
we assert Γ → [σ, τ]
APP

仮想ベンディング象形文字 ∪

we possess M:Γ → [τ, σ]
we possess N:Γ → τ
we use left uncurry[Γ, σ, τ]
we assert Γ → σ
UNIT

象形文字 !

we have Γ
we use make-terminal[Γ]
we assert Γ → 1

過去のメモ編アーカイブから

muses 半形式証明スクリプト 論理 画像 リンク 具体例

面積問題への対策（あるいは無策） (A21) - (保存用) 檜山正幸のキマイラ飼育記 メモ編 2019-01-08

意味不明な言葉達 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 2018-11-15

お絵描き証明の例 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 2016-02-24

$`\varphi : A\Rightarrow(B\Rightarrow C) \longrightarrow (A\land B)\Rightarrow C`$

関数なら：

$`f : A\Rightarrow(B\Rightarrow C) \rightarrow (A\times B)\Rightarrow C`$

証明オブジェクトとしてのラムダ項 - (保存用) 檜山正幸のキマイラ飼育記 メモ編 2017-08-25

真偽値の集合Prop何でもよい

論理 半形式証明スクリプト セミナー

CoqでもLeanでもPropを使うが、Prepの正体は何でもよくて、デカルト閉半環圏（の対象集合）であればよい。自然数上に定義された述語 p は

  • p: Nat → Prop

だが、その実体が次のいずれでも、さらに他の何かでもいい。

$`\quad p:{\bf N} \to {\bf B} \text{ in }{\bf Set}`$

$`\quad p:{\bf N} \to |{\bf Set}| \text{ in }{\bf SET}`$

DIDL〈ディドル〉

お絵描き 半形式証明スクリプト

ストリング図の描画指令〈instruction〉と記述〈description〉のための言語

  • Drawing Instruction Description Language

目的は違うが名前が似ているもの：

絵の構成素は：

  1. ワイヤーまたはケーブル（0-射）
  2. ノード（1-複射）
  3. グルーピング、グループボックス
  4. 書き換え操作、オペレーションボックス
  5. 部分図（ディスク、境界はサークル）

書き換え操作をグループに適用するときは、Using operatin を使う。

描画指令文／操作指令文と確認文とグルーピングブロックの組み合わで図を記述する。

lawless signature に法則を付け足すときの記法

半形式証明スクリプト 論理 教育 セミナー セオリー論

構文は：

law 2-ラベル :: 閉じた論理式

または

variable 変数の型宣言

law 2-ラベル :: 自由変数を含む論理式

法則の圏論的実体〈シング〉は2-射なので、法則名は2-ラベルとする。

事例：

signature LawlessMonoid within Set {
  sort U
  operation e: 1 → U
  operation m: U×U → U
}

法則を付け加える。

signature Monoid within Set {
  sort U
  operation e: 1 → U
  operation m: U×U → U

  law assoc :: ∀x, y, z∈U. m(m(x, y), z) = m(x, m(y, z))
  law lunit :: ∀x∈U. m(e, x) = x
  law runit :: ∀x∈U. m(x, e) = x
}

または

signature Monoid within Set {
  sort U
  operation e: 1 → U
  operation m: U×U → U

  variable x, y, z∈U

  law assoc :: m(m(x, y), z) = m(x, m(y, z))
  law lunit :: m(e, x) = x
  law runit :: m(x, e) = x
}

信頼できる談話環境

半形式証明スクリプト 論理 教育 STEM

信頼できる談話環境〈trustable discourse environment〉とは、そのなかでの発話行為、または記載（何かが書いてある）がそのまま事実と解釈してよい環境。

一番外側の記述は、信頼できる談話環境のなかにあると考える。そうでないと、「‥‥はほんとうか？」の永久後退が生じて、判断〈judgement〉ができない。信頼できる談話環境では、自動的に判断が出来る。

ある発話や記載が信頼できないときは、信頼できる談話環境内でその発話・記載をサブジェクトにした議論をする。

登録、存在命題、インデックス付き族、規則

半形式証明スクリプト 論理 教育

導出とシーケントを混同する理由 - (新) 檜山正幸のキマイラ飼育記 メモ編 に関連して。

信頼できる目録があるとする。目録に登録されていることが、存在を保証するならば、

  • 登録は存在命題に匹敵する。

演繹システムのシステム指標／ライブラリ指標は、信頼できる目録だから、指標に登録されていると、それはセマンティック背景圏の対象・射・オペレータ・2-射などの存在命題になる。存在命題（インデックス付き存在命題）に対するスコーレム関数は、インデックス付き族となる。

インデックス付き族を“規則”と呼んでいるのだろう。インデックスを具体化することが規則の具体化。規則の具体化は、全称命題の具体化ではあるが、メタ全称命題（インデックス付き存在命題は全称命題）の具体化に対応する。

演繹システムにおいては、次が同じ効果を持つ。

  1. インデックス付き導出族の登録
  2. メタなインデックス付き存在命題（全体はメタな全称命題）
  3. スコーレム関数として与えられる“規則”
  4. 構成的・具体的な関数として与えられる“規則”

登録が、メタなインデックス付き存在命題を主張することと同じであることが見過ごされやすい。また、スコーレム関数があれば十分だが、構成的・具体的に与えられることが多い。

導出とシーケントを混同する理由

半形式証明スクリプト 論理 教育

既存導出を組み合わせて新しい導出作ることにより証明を行う。このとき、実際の導出が何であるかは問題にならない。なので、シーケント〈導出のプロファイル〉を書くだけで導出を書いたことになる。これより、導出とシーケントが混同、あるいは同一視される。

A∧B → A はプロファイルだが、次の命題を考える。

  • [射影命題] ∀A, B.∃f.( f:A∧B → A ) in (a category C)

これが真だとして、スコーレム関数 ψ を考える。

  • (A, B) |→ ( (ψ[A, B] : A∧B → A) in (a category C) )

これは ψ:Obj(C)×Obj(C) → Mor(C) という関数を定義する。射のインデックス付き族になる。

今は 射＝導出 だから、導出のインデックス付き族になり、それを推論規則と呼ぶ。時系列で書くと：

  1. 射影命題のような、インデックス付き存在命題が与えられる。セマンティックな命題、メタ命題。
  2. インデックス付き存在命題のスコーレム関数を考える。
  3. そのスコーレム関数は、インデックス付き導出である。
  4. インデックス付き導出を“規則”と呼ぶ。

ここで注意すべきは、スコーレム関数さえあればよいこと。ψがほんとの射影である必要はない。ψを具体的に与えるとき典型的・簡単なのは射影だが、“規則”の実体が射影である必要性がない。

ここにギャップがある。仕組み上は射影である必要がないが、たいていはスコーレム関数の具体的な実現として射影を想定している。

次の概念のあいだの相互関係をよく理解すべきだ。

  1. インデックス付き存在命題〈indexed existential proposition〉
  2. スコーレム関数〈選択関数 | セクション〉
  3. スコーレム関数と同義のインデックス付き族
  4. 構成的・具体的に与えられたスコーレム関数
  5. スコーレム関数のプロファイル〈シーケント〉
  6. 規則とかパターンとか呼ばれるモノ

演繹システム (3)

muses 半形式証明スクリプト 論理
  1. 演繹システム上で解釈可能な記述〈description〉をスタンドアロンな記述と言う。
  2. 何も提供・公開してない記述をノートパッドと呼ぶ。
  3. スタンドアロンなノートパッドがTypeScrptのスクリプトに対応する。
  4. 演繹システムでは、スタンドアロンではないノートパッドもある。TypeScriptでは、スタンドアロンでないとスクリプトとみなされる。
  5. 何かを提供・公開していれば、それはノートパッドではない。アーティクルと呼ぶ。アーティクルの別名がモジュール。
  6. スタンドアロンなアーティクルは、演繹システム以外の依存性はない。ライブラリなしで解釈できる。
  7. スタンドアロンでないアーティクル／ノートパッドは、依存ライブラリ／依存パッケージを持つ。
  8. パッケージには、ターミノロジー定義、ノーテーション定義も含まれる。
  9. アーティクルの下の名前空間はデビジョンで作る。デビジョンは入れ子にできるので、デビジョンへのパスを定義できる。
  10. 指標と手続きは特殊なデビジョン。よって、パスで参照できる。
  11. デビジョン（指標含む）内にラベルがあれば、ラベルもパスで参照できる。

演繹システム (2)

muses 半形式証明スクリプト 論理

$`\newcommand{\derive}{ \vdash }%
\newcommand{\deduce}{ \mathop{\|\!-} }%
\newcommand{\afford}{ \mathrel{\|} }%
\newcommand{\Sign}[1]{ \mathscr{#1} }
\newcommand{\cat}[1]{ \mathcal{#1} }
\newcommand{\In}{ \text{ in } }
\newcommand{\ImpL}{ \Leftarrow }
\newcommand{\sto}{ \longrightarrow }
%`$
対応があまりピッタリではないが。

演繹システム 類似の既存用語
sys-prop 論理定数
sys-deriv 論理公理
sys-reas 推論規則
sys-equiv 論理法則
user-prop ？
user-deriv 分野公理
user-reas 分野推論規則
user-equiv 分野論理法則

システムを次のように置く。

$`\quad \mathscr{D} = (\mathscr{D}_\mathrm{prop}, \mathscr{D}_\mathrm{deriv}, \mathscr{D}_\mathrm{reas}, \mathscr{D}_\mathrm{equiv})`$

ライブラリは：

$`\quad \mathscr{L} = (\mathscr{L}_\mathrm{prop}, \mathscr{L}_\mathrm{deriv}, \mathscr{L}_\mathrm{reas}, \mathscr{L}_\mathrm{equiv})`$

演繹可能性は：

$`\quad \mathscr{L} \deduce_\mathscr{D} \Gamma \sto B`$

演繹定理から：

$`\quad \mathscr{L}, \hat{\Gamma} \deduce_\mathscr{D} (,) \sto B`$

あるいは、

$`\quad \mathscr{L}, \hat{\Gamma} \deduce_\mathscr{D} (\vdash B)`$

圏論と論理、絵図のメモ編過去記事リンク

リンク 論理 半形式証明スクリプト muses

順不同。

  1. 選言ボックスと二面ノード - (新) 檜山正幸のキマイラ飼育記 メモ編 選言ボックスと二面ノード
  2. デカルト閉復圏とラムダ計算 - (新) 檜山正幸のキマイラ飼育記 メモ編 ラムダ図
  3. これはいいぞ！ ラムダハウス - (新) 檜山正幸のキマイラ飼育記 メモ編 ラムダハウス
  4. メタストリング図 - (新) 檜山正幸のキマイラ飼育記 メモ編 メタストリング図
  5. 連言ボックス、選言ボックス、全称ボックス、存在ボックス - (新) 檜山正幸のキマイラ飼育記 メモ編 各種ボックス
  6. ワイヤリング図関連の同義語 - (新) 檜山正幸のキマイラ飼育記 メモ編 同義語
  7. ケリー／マックレーン・グラフ - (新) 檜山正幸のキマイラ飼育記 メモ編 ケリー／マックレーン・グラフ
  8. デカルト閉復圏とラムダ計算 - (新) 檜山正幸のキマイラ飼育記 メモ編 デカルト複閉圏
  9. 純ワイヤリング図からケリー／マックレーン・グラフ - (新) 檜山正幸のキマイラ飼育記 メモ編 ケリー／マックレーン・グラフ
  10. Leanの論理再考 - (新) 檜山正幸のキマイラ飼育記 メモ編 Leanの論理の絵
  11. 含意と全称 空間と論理 - (新) 檜山正幸のキマイラ飼育記 メモ編 空間、論域の考察

MEDLの構造

muses 半形式証明スクリプト

TypeScriptと比較する。

TypeScript Tenjin MEDL 備考
スクリプト ノートパッド 使い捨て
モジュール アーティクル .medl.md ファイル
パッケージ パッケージ 同じNPM構造
名前空間 デビジョン division
インターフェイス 指標 signature
総称クラス 構成手続き procedure
抽象クラス デビジョン division
.d.ts ファイル ライブラリ指標 .medls.json ファイル

アーティクルの雛形

---
file: foo.medl.md
tags: foo
title: foo
---
article foo

declare A in Set
declare B in Set
define foo1 : A → B in Set := ...

divison bar {
  declare ...

}

devision baz {

}

signature zot {

}