「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ九「規則一般についての注意」「集合族のデカルト積」「定義による同等性」（予習編）

　他の回はこちらから。

　今回は私の担当ではないのでゆるく。

f:id:cut_elimination:20210414213220j:plain

規則一般についての注意

　四種の規則が出てくる。

formation（形成）
introduction（導入）
elimination（除去）
equality（等号）

導入と除去は自然演繹と同じようなものである（とマーティン=レーフ先生も言っている）が、形式としてはそうでもITTでは規則の意味が乗っかっている。導入則は集合のカノニカルな要素を決める規則（つまり集合の意味を定める）で、除去則はそれによって定義された集合上の関数を定義するという。これがどういうことかというのは等号則の意味を考えるとわかる。マーティン=レーフ先生によれば、等号則というのは Prawitz の簡約規則のようなものだという*1。等号則は除去則が導入則で定義された集合（のカノニカルな要素）にどのように作用するかを定義している。証明の簡約は、導入則のすぐあとに同じ規則の除去則がくるような部分を書き換えて消去する。これを関数適用と捉えるわけだ。カノニカルでない要素の同等性も与えていると思う。

　それと形成則というのもある。これと他の規則でうまいこと4つの判断の形式を実現している。一対一に対応しているわけではないようだけど。

集合族のデカルト積

形成と導入

　形成則の帰結はなんらかのものが集合であるということだが、導入則の帰結はそれがどういう集合かということである。

　 $b(x) \in B(x)$ と $(\lambda x)b(x) \in (\Pi x \in A)B(x)$ の違いが問題である。マーティン=レーフ先生も説明を加えているが、「後者は前者の名前といえよう」（14ページ）とのこと。うーーーーん。わからない。

　また、

Since, in general, there are no exhaustive rules for generating all functions from one set to another, it follows that we cannot generate inductively all the elements of a set of the form $(\Pi x \in A)B(x)$ (or, in particular, of the form $B^A$ , like ${\mathbb N}^{\mathbb N}$ ).

一般にある集合から別の集合への全ての関数を生成しつくす規則はないので、 $(\Pi x \in A)B(x)$ （あるいは例えば $B^A$ 、 ${\mathbb N}^{\mathbb N}$ みたいに）という形の集合の全ての要素を帰納的に生成することはできない。

とある。前回の話と違っているようにも思うが、この微妙な違いが重要なのかもしれない。「すべて」が言えることと実際に生成できることは違うのか。帰納的に生成することとカノニカルな要素を定義できることは違うのか、とか。

形成の第二規則の正当化

　以前にも代入規則の正当化のところであったが、仮定付判断の仮定に遡る操作が気になる。

除去と等号の注意点

　Ap $(c, a)$ が $B(a)$ のカノニカルな要素を得るメソッドであるという話。

　 $c \in (\Pi x \in A)B(x)$ というのは前提されている。つまり $c$ は $(\Pi x \in A)B(x)$ のカノニカルな要素である $(\lambda x)b(x)$ を得るメソッドである。もう一つの前提 $a \in A$ を代入して $b(a)$ を得る。これは $\Pi$ 等号規則を使う気がする。 $b(a) \in B(a)$ である。よってこれを計算して $B(a)$ のカノニカルな要素を得る。