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

　Per Martin-Löf, "Intuitionistic Type Theory", 1984の「判断の形式の解釈」「命題」の章を読んで訳したり考えたりしています。

判断の形式の解釈（Explanations of the forms of judgements）

canonical、equality、computation

解釈とは

　解釈と訳したのは explanation であって interpretation ではない。だからなんだって話かもしれないが。

　解釈は以下の問いのどれかに答えることで与えられる。

集合とは何か？－存在論的（古代ギリシア）
何かが集合であると判断するには何を知っていなければならないか？－認識論的（デカルト、カントなど）
「 $A$ は集合である」という形式の判断は何を意味するか？－意味論的（モダン）

しかし本質的には同じ問いである。

カノニカルな要素

At first sight, we could assume that a set is defined by prescribing how its elements are formed.

まず、集合はその要素がいかに形成されるかを規定することで定義される、と仮定してみよう。

"prescribe"は「処方する」という意味もある。この例として自然数集合 ${\mathbb N}$ の定義があげられる。

f:id:cut_elimination:20210421071958j:plain

この規則によって要素が構成される（constructed）。

　しかし、例えば $10^{10}$ なんかは明らかに ${\mathbb N}$ の要素だがなんらかの $a \in {\mathbb N}$ について $a'$ という形はしていない。

We thus have to distinguish the elements which have a form by we can directly see that they are the result of one of the rules, and call them canonical, from all other elements, which we will call noncanonical.

なので、ある規則が適用された結果だと見てすぐにわかる形式の要素をカノニカルといい、他の要素を非カノニカルということにして区別せねばならない。

$10^{10}$ は ${\mathbb N}$ の非カノニカルな要素である。ここから話は二つの非カノニカルな要素の同等性（equality）の定義に向う。この段階ではやや唐突である。すぐに、まずはカノニカルな要素の同等性を形成を規定しましょう、となる。いずれは $10^{10}$ と $10000000000$ や $5000000000 + 5000000000$ が等しいことも判断できるようにしなければならない。

判断の解釈

(1) a set $A$ is defined by prescribing how a canonical element of $A$ is formed as well as how two equal canonical elements of $A$ are formed.

(1) 集合 $A$ は、 $A$ のカノニカルな要素がいかに形成されるか、および $A$ の二つの等しい要素がいかに形成されるかを規定することで定義される。

これが「 $A$ は集合である」という形式の判断の意味の解釈であるという。ちょっと思ったのだが、これは $a \in A$ という形式の判断とは違うのか。おそらく、ここでは「集合の（カノニカルな）要素の与え方」が与えられているだけで「集合の（カノニカルな）要素」が与えられているわけではない。あとで形式体系が導入されるが、「 $A set$ 」という形式の判断は形成則（formation rule）で与えられ、カノニカルな要素は導入則（introduction rule）で与えられる。ここでの議論から考えると形成則は導入則の前提になるような集合（の判断）に適用されるべきであるが（導入則すなわち要素の与え方、が与えられているということなので）、実際そのようになっている。

　しかしなぜ同等性（equality）もあらかじめ定義しておくのだろうか？一階論理は等式の公理（推論規則）も含むのも普通なので別に変ではないか…。

　というわけで同等性（等しさ）の形成（forming）を規定する（prescribe）。先程の ${\mathbb N}$ の規則には以下を加えればよい。

f:id:cut_elimination:20210421112639j:plain

他にも $A \times B$ の例が出ている。

f:id:cut_elimination:20210422112855j:plain

f:id:cut_elimination:20210422145407j:plain

　カノニカルな要素の間の同等性の定義を規定するのに反射的で対称的で推移的ならば特に制限はないとある。けっこう緩い。あとでITTは形式体系ではないということも書く。

　続いて集合の同等性の定義である。

(2) two sets $A$ and $B$ are equal if

and

for arbitrary canonical elements $a$ , $b$ .

これが $A = B$ という判断の意味である。外延の等しさではなく、カノニカルな要素の形成の仕方の等しさということか。

　続いて集合の要素について。

(3) an element $a$ of a set $A$ is a method (or program) which, when executed, yields a canonical element of $A$ as result.

(3) 集合 $A$ の要素 $a$ は、実行の結果として $A$ のカノニカルな要素が得られるメソッド（プログラム）である。

これは「 $a \in A$ 」という形式の判断の意味。計算の規則が書いてある。ここはけっこうちゃんと決まっている。集合 $A$ の要素 $a$ の計算過程で得られる $b$ について、 $b$ の最も外側の形が $A$ のカノニカルな要素であるならば、その $b$ を値として停止する。これは正規順序（normal order）とか遅延評価（lazy evaluation）とか書いてある。例として $(2 + 2) \in {\mathbb N}$ から $(2 + 1)'$ というカノニカルな要素が得られるというのが挙げられている。これはこの式のなかの $2$ を実行すると $1'$ になるがそれを最初にはやらないということだろう。ただし $2 + 1$ が ${\mathbb N}$ のカノニカルな要素だという判断にも計算が必要なのではないかと思うがどうか。それはさておきこれはラムダ計算の簡約の順番に関する戦略で正規順序簡約といわれるやつらしく、プログラミング言語ではHaskellで採用されている遅延評価に当たるものなのであろう。調べます。

　続いて要素の等しさ。

(4) two arbitrary elements $a$ , $b$ of a set $A$ are equal if, when executed, $a$ and $b$ yield equal canonical elements of $A$ as results.

(4) 集合 $A$ の二つの任意の要素 $a$ , $b$ が等しいのは、 $a$ と $b$ の実行の結果として $A$ の等しいカノニカルな要素が得られるときである。

これは「 $a = b \in A$ 」という形式の判断の意味。この定義の「集合 $A$ の等しいカノニカルな要素」というのは(1)ですでに与えられているのでよい感じである、とある。

　さて、カノニカルは正規（normal）と考えてよいのだろうか？そうすると計算を実行してカノニカルな要素を得るというのが証明の正規化に対応することになっていい感じなのであるが。しかし $(2 + 1)'$ は素直に見るとまだ計算が終っている感じがしない（ $0''''$ という形じゃないと）。

　例として $e, f \in A \times B$ というのが挙げられている。 $e$ と $f$ はそれぞれ $A \times B$ のなんらかのカノニカルな要素 $(a, b), (c, d)$ を得るメソッドである。 $e = f \in A \times B$ であるのは $(a, b) = (c, d) \in A \times B$ という計算結果として得られるカノニカルな要素の等しさによる。そしてこれは先ほどの $A \times B$ の要素の等しさの定義より、 $a = c \in A$ かつ $b = d \in B$ である場合に成り立つ。

命題（Propositions）

命題、証明、集合としての命題

命題の定義

　古典的には命題とは真理値でしかない、とある。しかしそれだと無限のドメイン上の量化を含む命題を正当化するのが困難になるとあり、やはり無限の量化の問題が出てくる。量化を含む命題の真偽は、そこにドメインの要素（の名前）を代入した命題の真偽をチェックすることで決まるが全称量化された文ならば真のとき、存在量化ならば偽のとき、すべての要素を代入してチェックしなければならない。これは確かに困難である。

　というわけなので直観主義では以下のように考える。

a proposition is defined by laying down what counts as a proof of the proposition,

a proposition is true if it has a proof, that is, if a proof of it can be given.

命題は、その命題の証明とみなされるものを定めることで定義される、

命題が真であるのは、それが証明を持っているとき、つまり、その証明が与えられうるときである。（これはプラヴィッツの"Intuitionistic logic: a philosophical challenge"という論文の引用）

命題の定義と真理の定義はけっこう別問題だと思うのだが、証明を真理と置き換えることで命題を真理値ではなく証明可能性で定義するということではあろう。

proofとderivationと不完全性定理

　しかし次がわからない。

Thus, intuitionistically, truth is identified with provability, though of course not (because of Gödel's incompleteness theorem) with derivability within any particular formal system.

よって、直観主義の考え方では、真理は証明可能性と同一である。ただしもちろん（ゲーデルの不完全性定理があるので）なんらかの特定の形式体系内の導出可能性と同一ではない。

まず、provabilityとderivabilityの違いってなんだろうか。調べてみると、驚くべきことに、私と同じようにこのITT84を読んで同じところで疑問に思っている人がいた。以下のQ&Aサイトで「derivabilityとprovabilityの違いとは？」という質問がある。

logic - What is the difference between derivability and provability? - Mathematics Stack Exchange

回答によると、proofは通常の数学で使うインフォーマルな概念でderivationは形式体系で定義される形式的なやつである、とのこと。これは"Basic Proof Theory"でも同じ方針だったのでけっこう一般的なことかもしれない。ITTはどうも言語が明確に定義されるものではないようで、命題のproofの形式定義もない。

　では、これがゲーデルの不完全性定理とどう関係するのか？第一不完全性定理は真理と証明可能性のズレを示唆するので、それを言っているのかもしれない。しかし「真だが証明できない命題」と言ったときの「真」は証明体系と別で与えられることであって、証明体系内では意味を持たないと考えてもよい、はず。なので証明から真理を定義するなら証明できない命題は真ではないとしてしまえばよいのではないかと。ロッサーの不完全性定理の「証明も反証もできない」は真理値を決められないが、直観主義論理では安全なのではないかと。このあたりは数学的にも哲学的にも難しそうである。不完全性定理ってわかるようでわからない。

　しかしもっと怪しいのは、ITTが形式体系ではないとしても形式化はできるのではないかということである。だからこそプログラミング言語の基礎理論となっているのでは。となるとITTも（算術を扱うならば）不完全性定理からは逃れられない。以下のQ&Aは難しいけれどそういうことを言っているっぽい（proofとderivationの違いも先ほどのと同様）。

lo.logic - How do we construct the Gödel’s sentence in Martin-Löf type theory? - MathOverflow

　まだまだ勉強が必要である。

論理演算子の意味の解釈、すなわち証明の解釈

　論理結合子の意味の解釈はこれまでの流れのとおり、それを含んだ証明の解釈によって与えられる。

f:id:cut_elimination:20210422113149j:plain

というのがいわゆるBHK解釈のだいたい一般的なバージョンであるが、これをもうちょっと明確にすると以下のようになる。

f:id:cut_elimination:20210422113156j:plain

ただしこれらはすべてカノニカルな形の証明で、本当はカノニカルな証明を得るメソッドはすべて証明される命題の要素となる、と注意がある。

　私からの補足。 $A \supset B$ と $(\forall x)B(x)$ の違いであるが、前者の $B$ は $A$ の要素と無関係であるのに対して後者の $B(x)$ は量化のドメインの要素に依存して決まる。命題を型とみなしたとき、これが依存型になる。

The Formulae-as-Types Interpretation

　If we take seriously the idea that a proposition is defined by laying down how its canonical proofs are formed (as in the second table above) and accept that a set is defined by prescribing how its canonical elements are formed, then it is clear that it would only lead to unnecessary duplication to keep the notions of proposition and set (and the associated notions of proof of a proposition and element of a set) apart. Instead, we simply identify them, that is, treat them as one and the same notion. This is the formulae-as-types (propositions-as-sets) interpretation on which intuitionistic type theory is based.

　命題をそのカノニカルな証明の形成法（上の二つ目の表のように）を定めることで定義されるというアイデアを真面目に受け止め、かつ集合はそのカノニカルな要素の形成法を規定することで定義されるということも受け入れるならば、命題と集合という概念（およびそれらと関連する命題の証明と集合の要素という概念）を分けておくのは不要な繰り返しにしかなりそうにない、ということは明らかとなる。そうではなく、単純に同一視する、すなわちそれらを同じひとつの概念として扱おう。これが「型としての論理式（集合としての命題）」という解釈で、直観主義型理論のベースとなっている。

　形成法が似ているという観察から同一視していいのかという疑問があるのだが、そもそも論理式と型は導出体系のなかでまったく同じ振る舞いをするという前提がある。この対応は形に関するものだが、命題と集合というもっと概念（notion）的な、内部構造的な部分でも同じであるというのがマーティン=レーフ先生の主張なのだろう。