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

自然演繹とLean

Lean 論理ダメ出し

Leanの推論規則 - (新) 檜山正幸のキマイラ飼育記メモ編の続き。

https://leanprover.github.io/logic_and_proof/nd_quickref.html に自然演繹のまとめがある。それに従うが、双含意〈bi-inplication〉は除く。

論理記号	導入	消去
Implication	ラムダ抽象、assume	空白右引数エバル
Conjunction	and.intro	and.left, and.right
Negation	ラムダ抽象	空白右引数エバル
Disjunction	or.inl, or.inr	or.elim（コペア構成高階関数）
Truth	trivial
Falsity		false.elim
Reductio ad absurdum	classical.by_contradiction
Universal quantifier	ラムダ抽象、assume	空白右引数エバル
Existential quantifier	exists.intro	exists.elim（高階関数）

バランスが悪い！悪すぎる！！ $\newcommand{\hyp}{\mbox{-} }$ 以下、※はコンビネータ〈リーズニング〉

論理記号	導入	消去
Implication	※ ${}^\cap(\hyp),\; \Lambda$	$\triangleleft,\; \triangleright$
Conjunction	$\blacktriangledown,\; \land\hyp cons$	$\bar{\ulcorner},\; \bar{\urcorner}$
Negation	※ ${}^\cap,\; \Lambda$	$\triangleleft,\; \triangleright$
Disjunction	$\underline{\llcorner}, \; \underline{\lrcorner}$	※ $[\hyp,\hyp]$
Truth	$delete_A,\;\bullet$
Falsity		$create_A,\; \bullet$
Reductio ad absurdum	※ $(\hyp)^\dagger$
Universal quantifier	$\blacktriangledown,\;\forall\hyp cons$	$\bar{\top},\; \forall\hyp proj$
Existential quantifier	$\underline{\bot},\;\exists\hyp inj$	※ $[\hyp]_{x:X}$

次の対応がハッキリしてない。

projection ←→ injection 射の双対
pair ←→ copair コンビネータの双対
decons ←→ cons ボックス入り口出口
有限個別 ←→ パラメトリック

射：

	projection	injection
有限個別	$\bar{\ulcorner},\bar{\urcorner}$	$\underline{\llcorner},\underline{\lrcorner}$
パラメトリック	$\bar{\top}$	$\underline{\bot}$

コンビネータ：

	pairing	copairing
有限個別	※ $\langle, \rangle$	※ $[,]$
パラメトリック	※ $\langle\hyp \rangle_{x:X}$	※ $[\hyp]_{x:X}$

バランス良く表にまとめると、
射：

論理記号	導入	消去
Implication	無理	$\triangleleft, eval$
Conjunction	$\blacktriangledown, cons$	$\bar{\ulcorner}, \bar{\urcorner}, proj$
Negation	無理	$\triangleleft, eval$
Disjunction	$\underline{\llcorner}, \underline{\lrcorner}, inj$	$\bullet, merge$
Truth	$\bullet, delete$	無し
Falsity	無し	$\bullet, create$
Reductio ad absurdum	無理	無し
Universal quantifier	$\blacktriangledown, cons$	$\bar{\top}, proj$
Existential quantifier	$\underline{\bot}, inj$	$\bullet, merge$

コンビネータ：

論理記号	導入	消去
Implication	$\Lambda, curry$
Conjunction	$\langle, \rangle, pair$
Negation	$\Lambda, curry$
Disjunction		$[,], copair$
Truth		無し
Falsity	無し
Reductio ad absurdum	${}^\dagger$	無し
Universal quantifier	$\langle\;\rangle, tuple$
Existential quantifier		$[\;], cotuple$

次が無視されている。

swap 変数の順序が変わる
∧-copy 変数の重複使用（∨-mergeの双対）
∧-delete 変数の未使用（∨-createの双対）
∨-decons 分解された状態から始める
∨-merge テキトーに処理
∧ボックスデフォルト
∨ボックステキトーに処理
∀ボックステキトーに処理
∃ボックステキトーに処理