■ - Finite Groups Fun 有限群あるいはちょこっと計算ファンの日記

[HoTT]HoTTをこっそり学ぶ　その3

　Martin-L $\rm\scriptsize{\ddot{o}}$ fのextensional版とintensional版についてもう少し追及してみる。その後の調査では、 $a=_{A}b$ というようなidentity typeの導入（intensional identity typeと呼ばれるそうな）があるものをintensional版と理解すればよいようである。非常に見分けやすい。ただし、identity typeが導入されていてもそのelementが常に等しくなるような理論はextensionalである。紛らわしいがそういう記述のある文献もあった（後述するUIP公理を仮定するケースである）。

さて、Martin-L $\rm\scriptsize{\ddot{o}}$ f自身の関連文献の変遷を見ると、

1972年版 "An Intuitionistic Theory of Types" (Girard's paradoxに言及あり)

1975年版 "An Intuitionistic Theory of Types: Predicative Part"

1984年版 "Intuitionistic Type Theory"

となっており、1975年版からintensionalであるとのことで確かに"1.7. Identity"に $I(x,y)$ としてintensional identity typeが導入されている。しからば1972年版はどうなっているのかとみてみると...おお、identity typeの定義が無いですよ。では、等号はどう解釈されているかというと、typeにせよproofにせよ、（文献中に定義されている）簡約化を行ったものが同じになったら等しいという定義にされている。文献中ではtypeやproofが文字つづりとして異なっていてもそれが抽象的なobjectとして等しいものを表現しているという意味でdefinitionally equalという言葉を使っている。等号はdefinitionally equalという意味となる。しかし、この理論においては propositionとしての"a=b"たとえば"2+2=1+3"といったpropositional equalityの証明が唯一しかないというUIP（Uniqueness of Identity Proofs）の公理が設定される必要があり、その場合、モデルはかなり強い制約を受けるだろう。

ところでおまけだが1972年版の1.9節にGirardのparadox（の改良版？）の説明があったので、ちょっと紹介してみよう。記法は同論文に従う。

typeの全体の集まりをtypeだと想定して、 $V$ としよう。このとき $V \in V$ が成立している。さて、無限減少列をもたない順序（an ordering without infinite descending chains）を定義するためにつぎの２つのproposition $P$ , $Q$ を定義する。

type $A$ とその上の二項関係 $<$ が定義されているときに

$P(A,<)=(\prod x\in A)(\prod y\in A)(\prod z\in A)(x < y \to ( y < z \to x < z))$

と定義する（原論文では $(\prod z\in A)$ がミスプリで抜けていると思われる）。これは見ての通り $<$ が推移律を満たしているという意味になっている。Martin-L $\rm\scriptsize{\ddot{o}}$ f理論では $\prod$ は全称記号 $\forall$ と解釈される。

もうひとつ

$Q(A, < )=(\prod f\in \mathbb{N}\to A)( (\prod n\in \mathbb{N})(f(n+1) < f(n))\to \bot)$

$K \to \bot$ は否定 $\neg K$ と解釈する。この意味は、（カッコの位置に注意しつつ）『自然数 $\mathbb{N}$ から $A$ への任意の写像 $f$ が与えられたとき、「全ての $n \in \mathbb{N}$ に対して $f( n+1) < f(n)$ 」は成立しない』すなわち『 $A$ の元の無限列に対して、減少し続けるようなものは存在しない』という解釈となる。さて、もし $P ( A,<)$ , $Q ( A, < )$ が成立するなら $a\in A$ で $a < a$ なるような $a$ は存在しないことがわかる。存在すると無限減少列 $\ldots < a < a < a$ ができてしまうからである。次に $U$ なるtypeを定義する。

$U=(\sum A\in V)(\sum < \in A \to (A \to V ) ) ( P(A, < )\times Q(A, < ))$

$\sum$ は存在記号 $\exists$ 、 $\times$ は論理積 $\wedge$ と解釈する。
$< \in A \to (A \to V )$ の部分がわかりにくいが、２つの $A$ の順序対が与えられたときに $V$ の元、すなわちあるtypeを返す写像である。その像であるtypeのelementが存在するとき『真』、存在しないとき『偽』とする二項関係と解釈される。すると $U$ は、無限減少列が存在しないような type $A$ とその上の関係 $<$ のペア全てが成すtypeと解釈される。( $U$ の元は $( A, < _A,p_A,q_a )$ と書かれる規約だが以下では $(A, < _A)$ と略記する。)

さて、 $U$ そのものの上に二項関係 $< _U$ を次のように定義する。

$\scriptsize{ ( A,< _A) < _U ( B, < _B)}$
$\scriptsize{\quad =(\sum f\in A\to B)(\sum b\in B) ( ( \prod x\in A)(\prod y\in A ) (x < _A y \to f(x) < _B f(y) )\times ( \prod x\in A ) ( f(x) < _B b)) }$

ややこしいが順に解釈してみよう。『写像 $f:A\to B$ と $b \in B$ が存在して、 $f$ は順序を保存し( $\small{\forall x\in A \forall y\in A (x < _A y \to f(x) < _B f(y) )}$ )、その像は $b$ によって抑えられている( $\small{ \forall x\in A ( f(x) < _B b)}$ )』となる。この定義で $P ( U, < _U)$ つまり推移律が成立しているのは見やすいだろう。

次に $( U, < _U)$ に無限減少列が存在しないことを証明する。仮に無限減少列が存在して、

$( A_{n+1},< _{n+1} ) < _U (A_n, < _n), n=0,1,\ldots$

となっているとしよう。この関係を成立させる $< _U$ の条件を $f_n:A_{n+1}\to A_n$ , $a_n \in A_n ; \forall a\in A_{n+1}(f_n(a) < _n a)$ とする。
このとき特に、 $f_n(a_{n+1}) < _n a_n$ であり、この関係式に順次 $f_{n-1},\ldots,f_1,f_0$ を作用させると

$f_0(f_1(\ldots ( f_n ( a_{n+1} ) \ldots) < _0 f_0(f_1(\ldots f_{n-1} ( a_n)\ldots), n=0,1,\ldots$

が作れるが、これは $( A_0, < _0)$ 内の無限減少列を与えているので矛盾である。よって $( U, < _U) \in U$ となっていることがわかる。だんだんきな臭くなってきた。次に $( U, < _U)$ が $U$ の中でmaximalな元であることを示す。もしこれが示せたら $( U, < _U) \in U$ だったので、 $( U, < _U) < _U ( U, < _U)$ が成立することになるが、これは $( U, < _U)$ が無限減少列をもたないことに矛盾し、結局体系そのものが矛盾を含んでいることがわかる。順序数全体が集合であると仮定すると矛盾を起こすという Burali-Forti のパラドックスと同じ論法である。無論、その原因は本家で順序数全体が順序数になってしまうのと同じように $U$ というtypeが定義されてしまう点にあり、もし階層的なuniverseを仮定すると $U$ は一つの階層内に収まらないため定義できなくなり、この矛盾は回避されてしまうという仕掛けである。

さて、証明を完成させよう。
任意の $( A, < _A) \in U$ に対して、 $( A, < _A) < _U (U, < _U)$ を証明したい。この関係式を成立させるには順序を保存する $f:A \to U$ を定義する必要があるが、 $f(a)=(A_a, < _a) \in U$ ここに $A_a=(\Sigma x\in A)(x < _A a)$ と定義する。 $A_a$ はいわゆる $a$ 切片というやつで、 $< _a$ は $< _A$ の制限とする。まず、 $f$ が順序を保っていることを証明しよう。
$a < _A b$ とすると $(A_a, < _a) < _U (A_b, < _b)$ かどうかが問題だが、自然な包含関係 $A_a \to A_b$ と $A_a < _b b$ より、この関係は成立している。また、任意の $a\in A$ に対して $f(a)=(A_a, < _a) < _U (A, < _A)$ は、同じく包含関係 $A_a \to A$ と $a \in A$ により成立しており、以上より $f$ と $( A, < _A) \in U$ が $( A, < _A) < _U (U, < _U)$ を成立させている。よって、 $(U, < _U)$ は $U$ でmaximalである。

[HoTT]HoTTをこっそり学ぶ その3

[HoTT]HoTTをこっそり学ぶ　その3