自然演繹とデカルト閉オペラッド

オペラッドの射をオペ射と呼ぶ。オペラッドのホムセットをオペホムセットと呼ぶ。オペホムセットを O(A, B⇒C) のように書く。⇒の左が空なら終対象を置き、右が空なら始対象を置く。ニ様なシーケント（http://d.hatena.ne.jp/m-hiyama-memo/20161026/1477451384）と同じ書き方をする。

推論規則	オペラッド解釈	備考
∧導入	∇∈O(A, B⇒A∧B)	射
∧除去	π1∈O(A∧B⇒A), π2も	射
∨導入	ι1∈O(A⇒A∨B), ι2も	射
∨除去	[ , ]:O(A⇒C)×O(B⇒C)→O(A∨B⇒C)	二項オペレータ
⇒導入	Λ:O(Γ, A⇒B)→O(Γ⇒A⊃B)	単項オペレータ
⇒除去	ε∈O(A, A⊃B⇒B)	射
¬導入	Φ:O(Γ, A⇒⊥)→O(Γ⇒¬A)	単項オペレータ
¬除去	η∈C(A, ¬A⇒⊥)	射
⊥導入	η∈C(A, ¬A⇒⊥), 上に同じ	射
⊥除去	θ∈O(⊥⇒A)	射