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

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

「直観主義型理論(ITT, Intuitionistic Type Theory)」勉強会ノート其ノ伍「等号の規則」「仮定付判断と代入規則」(予習編)

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

等号の規則 

 前回は"equality"を「同等性」とか「等しさ」と訳していたけど、今回は「等号」という訳も使う。記号と考えたほうが「規則」という概念と相性がいいかと思い。「判断の形式の解釈」の節では「カノニカルナ要素の等しさを決めておく必要がある」ということが論じられていたが、それをもとにカノニカルでない要素も含めた等号の規則が導入される。それはしかし反射性・対称性・推移性といういつものやつで、それをITT風に判断の形にしている。

仮定付判断と代入規則

 hypothetical judgement, extensional function, depending

仮定付判断

 B(x) \; set \; (x \in A) という判断は現在の標準的な記法では x:A \vdash B(x) \; set \; (type) となるはず。

  「仮定付判断」という訳は佐藤雅彦先生の「フレーゲの計算機科学への影響」という論文で採用されているものである。この論文も岡本先生のと同じで『分析哲学の誕生*1』という本に収録されている。ここでこの論文から引用しておく。

 マーティンレーフはまた仮定付判断(hypothetical judgment)とよばれる判断形式を計算機科学における一般的な用語として定着させることにも寄与している.本来,判断はそれ単独で意味が定まるものであり,したがって,判断の記述には自然に様々な仮定が必要となる.通常はこれらの仮定は議論の文脈の中で暗黙の内に仮定されるが,仮定付判断はそれらの仮定をすべて明示的にひとつの判断に記述したものとなる.一方,フレーゲの判断は,まさにそのような仮定をすべて明示的に記述したものであり,マーティンレーフによる仮定付判断はフレーゲの判断形式を現代に再興したものといえる.さらに言えば,マーティンレーフの型理論はゲンツェンによる自然演繹の体系の拡張とも言えるものであり,自然演繹の推論規則も仮定付判断から仮定付判断に移行する規則と見ることができる。(136ページ)

ちょっとこれの検討はまた今度にしようかな。おそらくITTの長所は一行の判断のなかに証明(ラムダ項)と仮定と命題(型)が同時に現れることなのだと思う。なので現代的な仮定付判断の記法のほうが良い気がする。

 "B(x) is a family of sets over A"とある。A 上の集合族といったらふつうは A の部分集合の集合という意味ではないかと思うが、ここではそうではなく、A は添字集合で B(x)A で添字付けられる集合族である。実際には B(x)A の要素 a_0, a_1, a_2, ... について \{B(a_0), B(a_1), B(a_2), ...\} という集合である。あるいは A からなんかしらの全体への関数と考えるか。

代入

The notation B(x) \; set \; (x \in A)(本当は上下に書かれている)only recalls that we make (have proof of) the judgement that B(x) is a set under the assumption x \in A, which does not mean that we must have a derivation within any particular formal system (like the one that we are in the process of building up).(9ページ)

この一節はちょっと奇妙だと思った。やはり形式的な導出は必要ないということが書かれているが、しかし我々はそういうのをいま作ろうとしている、とある。いずれは x \in A から B(x) \; set への導出も形式的に与えられるからそれまで待てということだろうか? 最初のほうで「数学の基礎あるいは哲学としてのロジック」という宣言がなされていたが、個々の数学ジャンルごとに与えればよくて、いまはもっと大局的で根源的でそれゆえインフォーマルということだろう。

 代入の4つ目の規則はこれまでの規則から導けるようなのでやってみた。

f:id:cut_elimination:20210429185423j:plain

②とか③というのは代入規則の2つ目と3つ目という意味である。c \in A はこの導かれる規則の前提 a = c \in A に暗黙のうちに入っている。

 (3)の b(x) \in B(x) \; (x \in A) という判断の解釈で extensional function(外延的関数)という語が出てくる。この「外延的」というの語は見るたびに意味がよくわからない。内包しかり。ここでは関数の同一性が入力に対する値の同一性によって与えられるという意味か。というのはラムダ計算の \eta 同値である。それで、b(x)ドメイン A からレンジ B(x) への外延的関数ということだが、この B(x) は項 x に依存して(depending on)変る。この依存というのは今後も重要である。値域が入力に依って変るというのははなはだ不思議である。