「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ拾七「選択公理」「"〇〇 such that □□"みたいなやつ」（予習編）

　直観主義型理論シリーズ。他の回はこちらから。

選択公理

　選択公理はITTでは定理になる。

選択公理の定式化

　新井敏康『集合・論理と位相』を参考にする。

基幹講座数学集合・論理と位相

作者:新井敏康
東京図書

Amazon

　選択公理は以下のような定式化が一般的かもしれない。

　（AC）任意の集合族 $(X_i)_{i \in I}$ について

　 $I \neq \emptyset \land \forall i \in I [X_i \neq \emptyset ] \to \Pi_{i \in I} X_i \neq \emptyset$

しかし、以下もこれと同値である。

　（AC’）任意の集合 $A, B$ と任意の $P \subset A \times B$ について

　 $\forall a \in A \exists b \in B [(a, b) \in P] \to \exists f \in B^A \; \forall a \in A [(a, f(a)) \in P]$

ITT論文ではこのAC'が採用されている。

選択公理の証明

　というわけなので、ITTでは選択公理は以下のように書ける。

　 $(\forall x \in A)(\exists y \in B(x))C(x, y) \supset (\exists f \in (\Pi x \in A)B(x))(\forall x \in A)C(x, \textsf{Ap}(f, x)) \; true$

論理読みをしなかったら

　 $(\Pi x \in A)(\Sigma y \in B(x))C(x, y) \supset (\Sigma f \in (\Pi x \in A)B(x))(\Pi x \in A)C(x, \textsf{Ap}(f, x))$

となる（ $\supset$ よりも $\to$ のほうがよかったかも）。

　これを証明する。以下のようになる（ $A \; set$ や $B(x) \; set \; (x \in A)$ も暗黙的に仮定している）。※カッコがたりてないところアリ。

f:id:cut_elimination:20210625162541j:plain

かなり込み入った導出だが、ポイントは

選択公理は「XならばY」の形をしている。
直観主義数学でこれを証明するには、Xの証明を得ているものとしてYの証明を得ればよい。
選択公理の場合、Xの証明とは、任意の $x \in A$ を $y$ と $C(x, y)$ の証明のペアにうつすメソッドである。
$f$ を任意の $x$ をそのようなペアのひとつめの要素にうつすメソッドであるとすると、任意の $x$ について $C(x, f(x))$ は成り立つ。これはYも成り立たせる。
この議論をITTのなかで形式的にシミュレートしたのが上の導出である。

古典数学との違い

　ZF集合論では選択公理は証明できないので公理として立てる必要がある。しかし選択公理は自明とは言い難い。しかしここでは証明ができなので正当化としては十分である。

　いろいろな言語で選択公理は表現はできても証明できない。例えば有限型のハイティング算術では公理としている。

なぜ証明できるのか？

　古典数学では証明できないのにITTでは証明できるのは何故か？

　新井本にいろいろ書いてある。AC'の形だと選択公理は自明に見える。前件部分を「任意の $a$ に対して適当に $b \in B$ を取ってくれば $(a, b) \in P$ とできる」と読めばそのように思われる。しかし、 $\\exists b \in B [(a, b) \in P]$ を仮定したとて、 $(a, b) \in P$ となる $b \in B$ を表す具体的な式が取ってこれるわけでは必ずしもない。これが選択公理を要請する理由である。

　しかるにITTでは、前件が真であるということがそのような具体的なモノが構成されていることを含意するのである。それを左射影で取り出している。

　なお、前回のヒルベルトの規則も選択公理と同じような理由で要請されていたと思う。

　ACの形だったらどうなるのか、それはわからない。

"〇〇 such that □□"みたいなやつ

the comprehension axiom, the separation principle, the witnessing information

目撃情報

　 $\Sigma$ の応用例としてもうひとつ、"the set of all $a \in A$ such that $B(a)$ holds（ $B(a)$ を満たすようなすべての $a \in A$ の集合）"というのがある。 $A$ を集合、 $B(x)$ を $x \in A$ についての命題とする。定義したいのは要するに $\{x \in A : B(x)\}$ という集合である。 $B(a)$ を満たす $A$ の要素 $a$ を持っているというのはつまり、 $A$ の要素 $a$ とともに $B(a)$ の証明、すなわち $B(a)$ の要素 $b$ を持っているということである。なので $\{x \in A : B(x)\}$ の要素は $b \in B(a)$ を満たすペア $(a, b)$ であり、それはつまり $(\Sigma x \in A)B(x)$ の要素である。よって $\Sigma$ 規則が包括原理やZFの分出公理のような役割を果たす。 $b \in B(a)$ によって得られる情報をフェファーマンは目撃情報（witnessing information）と呼んでいる（ふつう古典的な理論では $\{x \in A : B(x)\}$ だけならば目撃情報は要請されないだろう）。

　このちょうどよい応用例はコーシー列である。

例：コーシー列としての実数(集合)

　コーシー列も新井本に出てくるのだが、ここではあまり関係ない。コーシー列というのは実数を定義するひとつの手法である。ITTでは以下のように定式化できる。まず、

　 ${\mathbb R} \equiv (\Sigma x \in ({\mathbb N} \to {\mathbb Q}))Cauchy(x)$

とする。すなわち、実数集合というのはコーシー条件なるものを満たす有理数列（自然数集合から有理数集合への関数で表現）とそれがコーシー条件を満たすことの証明のペアの集合である。伝統的な書き方をすると $\{x \in {\mathbb Q^{\mathbb N}} : Cauchy(x)\}$ ということになる。このコーシー条件はITTでは次のように書ける。

　 $Cauchy(a) \equiv (\forall e \in {\mathbb Q})(e$ > $0 \supset (\exists m \in {\mathbb N})(\forall n \in {\mathbb N})(|a_{m + n} - a_m|) \leq e)$ （ただし、 $a$ は $a_0, a_1, ...$ という有理数列である。）

コーシー列の直感的な意味はうまく言えない。

　さて、こうすると、 $c \in {\mathbb R}, e \in {\mathbb Q}, d \in (e$ > $0)$ （ $d$ は $e$ > $0$ の証明）とおけば

f:id:cut_elimination:20210625163733j:plain

というようにして具体的な $a_m \in {\mathbb Q}$ が得られる（導出の最下段がそれである）。 $c$ がコーシー条件を満たすことの証明である $\textsf{q}(c)$ が有理数列を構成し、 $m$ 番目に、有理数 $e$ に応じた精度で $a_m$ という近似を出すメソッドとなっているのである。このように具体的な近似値を出せる（どれくらいの手間でどのように出せるかわかるのもも含めて）のが目撃情報であろう。