曇りなき眼で見定めブログ

学生です。勉強したことを書いていく所存です。リンクもコメントも自由です! お手柔らかに。。。更新のお知らせはTwitter@cut_eliminationで

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ四「判断の形式の解釈」「命題」(復習編)

予習編はこちら

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ参「判断の形式の解釈」「命題」(予習編) - 曇りなき眼で見定めブログ

 

 

集合は型だと思ったほうがいいかも

 このITT84では \in 記号を採用しているが、やはり集合を素朴な意味で捉えると何かの集まりが予めあるように思ってしまうので、適宜" : "に読み替えるとよさそうである。集合といっても中身を前提としない。a \in A または a \notin A が任意の aA について成り立つわけではない。排中律は成り立たないので。

 しかし型ではなく集合という用語に拘っているのにも理由があるようで、それは後述。

3つの哲学

 判断の形式の解釈をするうえでマーティン=レーフ先生は、まず集合に関する存在論・認識論・意味論を提示し、これらは本質的に同じだという。私はここはスルーしてしまっていたのだが、ものすごく強い主張をしている。存在論と認識論と意味論が同じだなんて! しかしITTは構成主義の理論であり、数学的対象の存在を構成によって与えるという立場である。そこに判断という認識論的なものを入れているのがITTの特徴である。さらに全体としては構文論と意味論を同時に与えるという試みでもある。ということは確かに3つの哲学を本質的に同じと考えることがITTの哲学的立場なのである。

何がカノニカルな要素か?

 不完全性定理の回避のくだりでも示唆されているが、ITT84はなんらかの形式体系を導入しているわけではないようである。{\mathbb N}\times はなんとなく常識的に使われるこれらをITTで表現しましたという感じで、例えば {\mathbb N} は数字の定義をしていないし \times単位元とか空集合の定義がなくて演算としての使い方がよくわからなかったりする。(空集合はあとで \bot として出てくる)

equality

 なぜ等号の規則を集合の定義に組み込むのか? これはITTの独自性でありよくわからない部分でもある。しかし集合の等しさは要素の等しさで定義され、要素の等しさは計算によって定義される。要素はメソッドあるいはプログラムである。その実行結果から等しさが判断される。ということは、等号を集合の定義に組み込むのは、計算(computation)がITTにとってプリミティブだということの表明なのだと思う。

カノニカルかどうかはどう知るのか?

 (2 + 2) を遅延評価で実行すると (2 + 1)' となる(ここでも唐突に足し算が出てくる)。これと 2 + 1 \in {\mathbb N} より 2 + 2 \in {\mathbb N} という判断をしている。しかし 2 + 1 \in {\mathbb N} という判断をするには 2 + 1 \in {\mathbb N} を実行してカノニカルな要素を得なければならないはずで、これはおかしい。このあたりはわりと計算規則のたてようによるのではないか、という感じ。

例をさらに具体的に

 要素の等しさの判断の例として e, f \in A \times B というのが挙げられているが、より具体的に (2 + 2, 3 + 3) = (3 + 1, 4 + 2) \in {\mathbb N} \times {\mathbb N}という判断を考える。(2 + 2, 3 + 3)(3 + 1, 4 + 2) をそれぞれ遅延評価で実行すると、途中で (2'', 3''')(2'', 3''') という等しいカノニカルな要素が得られる。もしくは ((2 + 1)', (3 + 2)')((3 + 0)', (4 + 1)') という段階でも等しいと判断していいかもしれない。そのへんはゆるそうだ。

判断はいつされるのか?

 計算が終るときである。たぶん。これが直観主義なのではないかと。計算が実行される前に判断結果は決まっていない。それは古典的な考え方である。「判断」という言葉にはそうした思想が含まれているように思う。

真理と証明可能性

 真理値の定義を証明可能性によってしているのではなく、古典論理において真理が果す役割を直観主義では証明に置き換える、ということかと。

全称量化と含意、存在量化と連言の関係

 依存型を導入するとわかるが、含意は全称量化の、連言は存在量化の、依存関係のない特殊ケースである。つまり命題論理は述語論理の特殊ケースであるとも言える。で、私は、全称量化は連言を繋げたもので存在量化は選言を繋げたものという感覚があるので、特に連言が存在量化に相当する \Sigma 型から作られるのが不思議だった。しかしそうでもない。

 述語論理に入門するとまず教わるやつで、\forall x(Fx \supset Gx) 型の論理式と \exists x(Fx &  Gx) 型の論理式がある。これらの式でなぜ全称量化は含意と、存在量化は連言とペアになるのか説明が難しいと思っていたのだが、今回のケースはまさにこれなのである。

 なんかうまく言えないけどこれには感動した。勉強会仲間からこれを指摘されて目からウロコだった。ありがとう。つまり、依存型や証明による命題の定義を考えていくと、全称量化と含意、存在量化と連言の親和性はごく自然なのである。

 これについてはもうちょっとじっくり考えてみたいかも。

命題と論理式、集合と型

 命題と論理式、集合と型という用語には使い分けがあるようである。思い返すと2ページで論理式は帰納的に定義されるが命題は"open concept"であるという話があった。この違いは集合と型にも適用できるのではないかと思う。型は形式体系で帰納的に定義されるが集合は"open concept"であろう。このITT84が形式体系にこだわらないのは"open concept"を重視していることと関係があるだろうと。CHIが体系における導出の形でなくそのものの性質から帰結するのは、論理式と型ではなく命題と集合の対応であると考える必要がどっかであるのか。

 CHIはなぜ成立するのか? 勉強会仲間が名言を放っていた。「同じものについて語ってるから同じものになるよね」。つまり、導出体系が同型になるのは、そもそも同じものについての導出体系だからなのである。