「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ弍「緒言」「命題と判断」（復習編）

「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ壱「緒言」「命題と判断」（予習編） - 曇りなき眼で見定めブログ　これの復習編です。

f:id:cut_elimination:20210417212903j:plain

緒言

It is free from the deficiency of Russell's ramified theory of types, as regards the possibility of developing elementary parts of mathematics, like the theory of real numbers, because of the presence of operation which allows us to form the cartesian product of any given family of sets, in particular, the set of all functions from one set to another.

これ（可述的な直観主義の型の理論）は、実数の理論のような数学の初等的な部分を展開しうるという点で、ラッセルの分岐的な型の理論の欠点を逃れている。何故なら、任意の与えられた集合族からデカルト積を作る操作が存在するからである。具体的には、あるひとつの集合から他の集合への関数すべての集合である（ITT84, 1ページ）

この"in particular"以下はITTにおける"operation"の具体例を述べているのだと私は解釈したが、そのまま読むとちょっと微妙な書き方なので、もうちょっと読み進めてから再検討ということに。このあたりはいきなりかなりの予備知識を要求していて大変で、有限のドメイン上の量化ならいいが無限になると微妙になるというのもよくわからない。これは直観主義のすごく重要なポイントのような気がする。ビショップの構成的数学あたりもちゃんと勉強しなければ。可述的かつ還元公理なしでかなりの程度の数学が実行できるというのがITTの利点のはずで、となると実数の議論は避けて通れない！

命題と判断

判断の形式

...the premisses and conclusion of a logical inference are judgements.

…論理的推論の前提と帰結は判断である。

これが重要そうである。つまりITTは判断から判断を導いていく体系なのである。

The distinction between propositions and judgements was clear from Frege to Principia. These notions have later been replaced by the formalistic notions of formula and theorem (in a formal system), respectively. Contrary to formulas, propositions are not defined inductively. So to speak, they form an open concept.

命題と判断の区別はフレーゲから『プリンキピア』までは明確である。のちにこれらはそれぞれ（形式体系における）形式的な論理式と定理に置き換わった。論理式と違って命題は帰納的に定義されない。言うなれば、命題は開かれた概念を形成する。

この"open concept"がよくわからなかったのだが、帰納的ではないということなので、帰納的定義に使われる「これのみが〇〇である」というのがないということか、となった。また、論理式には well-formed というのがあるが命題にはない、とか。フレーゲの『概念記法』では命題は内容だから、とか。そんな感じである。

　その後の議論も予習編では書いていなかったが重要だった。ロジックの教科書ではふつう構文論と証明論と意味論を定義して解釈を与えていくが、ITTでは形式と意味の区別がないという。マーティン=レーフ先生によればこれは通常の数学実践に近い。ロジック以外の分野の数学者は形式と意味を分けて考えたりしないからだろう。また、この発想は証明論的意味論に繋がっていくと思われる。

When one treats logic as any other branch of mathematics, as in the metamathematical tradition originated by Hilbert, such judgements and inferences are only partially and formally represented in so-called object language, while they are implicitly used, as in any other branch of mathematics, in the so-calld metalanguage.

ロジックを他の数学の分野と同じように扱うとき、すなわちヒルベルト以来のメタ数学のようにするとき、こうした判断や推論は単に部分的かつ形式的にいわゆる対象言語内で表現されるだけであるが、いわゆるメタ言語内では、他の数学の分野においてと同じように、暗黙のうちにしか使われない。

ここはなかなか英語が読みにくかった！勉強会内で私が言った解釈も間違っていたと思う。つまり、ヒルベルト以来のメタ数学では判断や推論を扱っているが、対象言語内の扱いは不十分だし、メタ言語では依然として明示されない、という点が不満なのである。これを体系内で明示するのがITTなのだ。

　 $\vdash$ 記号の歴史的な意味とかを考えるとおもしろそうだな〜となった。フレーゲの体系ではこの左には何も書かない、と思う。推件計算やITTでは左に書く。

...before a rule of inference can be justified, it must be explained what it is that we must know in order to have the right to make a judgement of any one of the various forms that the premisses and conclusion can have.

…推論の規則を正当化する前に、なんらかの形をした前提と結論の判断をすることが許されるためには何を知っていなければならないか、説明が必要だ。（3ページ、2段落目）

ここは私は予習でスルーしていたが重要なところだった。先述のとおり前提と結論は判断である。このくだりのあとで判断の4つの形式が導入されるが、それによって前提から結論を出す推論規則の前にそもそも前提と結論はどのような形をしていなければならないかがわかるのである。 $A = B$ という判断をするにはその前に $A set$ と $B set$ という判断がなければならない、という注意も付け加わる。こういうのはITT84では上に（）に入れて明示されるし、現代的な記法では $\vdash$ の左に書かれるはず。