型の圏（複圏、多圏もある）と命題の圏（複圏、多圏もある）との関係。カリー／ハワード／ランベック対応（むしろ、カリー／ハワード／ランベック・フレームワーク）があるので似てる。抽象化すれば同じになる。が、型コンテキストの圏の対象の上に命題の圏が乗って置換〈substitution〉と限量子で命題の圏が繋がる構造を持っている。一言で言えば、ハイパードクトリン。インスティチューションとしても定式化できる。
共通の用語や、異なる用語。
- コンテキスト → 型コンテキスト、命題コンテキスト
- コンテキストのラベル → 変数名／変数番号、命題名／命題番号
- 命題コンテキスト ＝ 命題の宣言リスト（実体、データ型として）
- 命題コンテキスト ＝ 仮定（役割として）
- ターゲット → 関数のターゲット型〈戻り値型〉、導出のターゲット命題
- ターゲット命題 ＝ 結論
- シーケント〈プロファイル〉 → 型シーケント〈{複}?関数のプロファイル〉、命題シーケント〈導出プロファイル〉
- スワップ射 → 型スワップ射、命題スワップ射
- コピー射 → 型コピー射、命題コピー射
- 破棄射 → 型破棄射、命題破棄射
- グラフティング → {複}?関数グラフティング、導出グラフティング
- 複結合 → {複}?関数複結合、導出複結合
- ペアリング → 関数ペアリング、導出ペアリング
- 導出ペアリング ＝ 連言導入
- 射影 → 型射影、命題射影
- カリー化 → 関数カリー化、導出カリー化
- 関数カリー化 ＝ ラムダ抽象
- 導出カリー化 ＝ 含意導入リーズニング
- アンカリー化 → 関数アンカリー化、命題アンカリー化
- 関数アンカリー化 ＝ 関数適用
- 命題アンカリー化 ＝ 含意消去リーズニング
- 終対象 → 終型、終命題
- 終型 ＝ ユニット型
- 終命題 ＝ 真命題
- 始対象 → 始型、始命題
- 始型 ＝ 空型
- 始命題 ＝ 偽命題
- 終型 ＝ ユニット型
- 終命題 ＝ 真命題
- 終射 → 終関数、終導出
- 始射 → 始関数、始導出
- 恒等 → 恒等関数、恒等導出
- General substitution
- Substitution by Delete
- Substitution by Copy
- Substitution by Swap
- Substitution by Function term
様々な規則
https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf の規則を列挙しておく。
型の圏の“規則”
- IDENTITY 恒等単純関数がある／使える。
- WEAKENING 破棄多関数をプレ多結合してよい。
- CONTRACTION コピー多関数をプレ多結合してよい。
- EXCHANGE スワップ多関数をプレ多結合してよい。
- MULTI-COMPOSITION 多関数を多結合してよい。多関数項と多関数記号を組み合わる。
- PAIRING 2つの複関数をペアリングして複関数を作ってよい。デカルト性。
- PROJ-1 第一射影単純関数をポスト結合してよい。
- PROJ-2 第ニ射影単純関数をポスト結合してよい。
- ABS 複関数をカリー化してよい。
- APP 複関数をアンカリー化してよい。エバル複関数と複結合してよい。
- UNIT 終複関数がある／使える。
恒等単純関すと各種の結合が圏類似構造の公理だとして、次の基本構成の存在を要請している。
- 破棄多関数 Γ, σ → Γ
- コピー多関数 Γ, σ → Γ , σ, σ
- スワップ多関数 Γ, σ, σ' → Γ, σ', σ
- 第一射影単純関数 τ×σ → τ
- 第ニ射影単純関数 τ×σ → σ
- 終複関数 Γ → 1
射もモノイド積に相当するマージ規則を許せば、次のように単純化できる。
- 破棄多関数 σ → (,)
- コピー多関数 σ → σ, σ
- スワップ多関数 σ, σ' → σ', σ
- 第一射影単純関数 τ×σ → τ
- 第ニ射影単純関数 τ×σ → σ
- 終多関数 Γ → (,)
演繹の構造規則
- IDENTITY 恒等単純導出がある／使える。
- CUT 2つの複導出をグラフティングしてよい。
- WEAK-PROP 破棄多導出ををプレ多結合してよい。
- CONTR-PROP コピー多導出をプレ多結合してよい。
- EXCH-PROP スワップ多導出をプレ多結合してよい。
- WEAK-TYPE 破棄多関数で引き戻してよい。
- CONTR-TYPE コピー多関数で引き戻してよい。
- EXCH-TYPE スワップ多関数で引き戻してよい。
- SUBSTITUTION 一般的な複関数で引き戻してよい。
プレ多結合してよい多導出は：
- 破棄多導出 Θ, ψ → Θ
- コピー多導出 Θ, ψ → Θ, ψ, ψ
- スワップ多導出 Θ, φ, ψ → Θ, ψ, φ
引き戻し〈置換 | 翻訳〉に使ってよい関数類は：
- 破棄多関数 Γ, σ → Γ
- コピー多関数 Γ, σ → Γ , σ, σ
- スワップ多関数 Γ, σ, σ' → Γ, σ', σ
- 一般的な複関数 Γ → σ （終複関数を含む）
論理の規則 so-called 自然演繹
- TRUE 終複導出がある。
- FALSE 始単純導出 ⊥ → ψ がある。仮定を水増しして Θ, ⊥ → ψ の形も使う。
- AND-I 2つの導出の連言ペアリングをしてよい。直積ペアリングと同様。
- AND-E1 第一射影単純導出がある。ポスト結合してよい。
- AND-E21 第ニ射影単純導出がある。ポスト結合してよい。
- OR-I1 第一入射単純導出がある。ポスト結合してよい。
- OR-I2 第ニ入射単純導出がある。ポスト結合してよい。
- OR-E 2つの導出の選言コペアリングをしてよい。直和コペアリングと同様。
- IMP-I 複導出をカリー化してよい。
- IMP-E 複導出をアンカリー化してよい。MP複導出と複結合してよい。
- ∀-I x:σ とういう変数を足して、破棄多関数 Γ, σ → Γ の置換の随伴が作れる。
- ∀-E 複関数 Γ → σ でインスタンス化できる。
- ∃-I 複関数 Γ → σ を証拠にして存在を主張できる。
- ∃-I x:σ とういう変数を足して、破棄多関数 Γ, σ → Γ の置換のもうひとつの随伴が作れる。
