考えながらダラダラと書く。
まず普通のシーケント計算：
Γ, A ⇒ B ---------- 含意導入 Γ ⇒ A→B Γ, x:A ⇒ P(x) ----------------- 全称導入 Γ ⇒ ∀x:A.P(x)
こう見ると確かに似てる。
PがAとの依存性がないとは、P(x) = B が常に成立。よって、∀x:A.P(x) = ∀x:A.B = A→B 。これが普通の論理だとあまり強調されない。集合の所属関係でもうまく説明できるかな。
集合Aの任意の要素に対して、固定命題Aの証明が得られる -- あるいはxの性質がP(x)だと確認できれば、xに依存しない性質Bだという性質を証明できる。
Pがxに依存してないことを P(!x) と書けば：
- ∀x:A.P(!x) ≡ A→P
- Πx:A.P(!x) ≡ Πx:A.B ≡ [A, B]
入れ子のリーズニング図を描いてみる。
Γ, A
---------
B
============== 含意導入
Γ
------
A→B
Γ, x:A
---------
P(x)
================= 全称導入
Γ
--------
∀x:A.P(x)ラムダ項付き：
Γ, x:A
---------
E:B
============== 含意導入
Γ
---------
λx.E:A→B
Γ, x:A
----------
E(x):P(x)
================= 全称導入
Γ
----------------
λx.E(x):∀x:A.P(x)λx:A.E(x) : ∀x:A.P(x) あるいは λx:A.E(x) : Πx:A.P(x) という型付きラムダ項がキモ。x |→ P(x), x |→ E(x) という型族〈型ファミリー〉と変数入り項の両方を一緒に考える。ま、依存型ってそんなもんだけど。
ファミリー≒バンドルとセクション、バンドル空間とセクション空間だな。Σ型とΠ型を一緒に考えて、双対になるかな。セレクター＝射影＝関数の求値。インサーターはバンドルの要素へのポインターか。
- 底空間は論域＝インデックス集合
- 底空間の点ごとのセレクター＝射影 はセクションの点での値を求める。セクション空間 → ファイバー空間
- 底空間の点ごとのインサーター はファイバーの埋め込み。ファイバー空間 → バンドル空間
- セクション空間＝パイ型＝極限 と バンドル空間＝シグマ型＝余極限 が双対。ファミリーが関手で、ファミリーの域が底空間。
型ファミリーがやはり大事みたい。型ファミリーの域が底空間で、値がファイバー空間で、そこからバンドル空間とセクション空間が作れる。関数空間はセクション空間の特殊なもの。パイ型＝全称命題と関数空間型＝含意との関係はこれだ。
点と空間の概念でも説明できそうだな。空間が命題で点や関数が証明か。
