「直観主義型理論（ITT, Intuitionistic Type Theory）」勉強会ノート其ノ弐拾壱「有限集合」「無矛盾性」（予習編）

有限集合

規則

　これまでの規則はすべて、ある集合（あるいは集合族）からある集合を作るものだったが、ここで導入する有限集合は前提なしに直接に与えられるものである。 $n = 0, 1, 2, ...$ によって無限個のルールがあることに注意。

f:id:cut_elimination:20210709024844p:plain

${\mathbb N}_n$ 形成則

　前提がない。

${\mathbb N}_n$ 導入則

　 ${\mathbb N}_0$ には要素がない（これは図にも書いたように $m \in \{x \mid 0 \leq x$ < $n\}$ として $n$ を変えていくとわかりやすいかも）。 ${\mathbb N}_1$ はひとつのカノニカルな要素 $0_1$ を持ち、 ${\mathbb N}_2$ はカノニカルな要素 $0_2, 1_2$ を持つ、などなど。

${\mathbb N}_n$ 除去則

　 $C(z) \; set \; (z \in {\mathbb N}_n)$ はふつうに ${\mathbb N}_n$ 上の性質として解釈できる。前提を知っていると仮定して、 ${\textsf R}_n$ を以下のように解釈する。

　まず、 $c$ を実行する。すると $m_n \; (0 \leq m \leq n - 1)$ となる。対応する $C(m_n)$ の要素 $c_m$ を選んでさらに実行する。 $m_n$ は $c$ と等しいということだったので前提の $c_m \in C(m_n)$ と合せて $d \in C(c)$ となる。

　 ${\textsf R}_n$ は有限集合 ${\mathbb N}_n)$ 上の再帰（recursion）である。場合わけによる定義のようなものである。 $n$ 個の規則がある。

${\mathbb N}_n$ 等号則

　 $0$ と $1$ の規則のみを作っておいて、 ${\mathbb N}_2 \equiv {\mathbb N}_1 + {\mathbb N}_1, {\mathbb N}_3 \equiv {\mathbb N}_1 + {\mathbb N}_2$ などなどと定義して他の規則を導出することもできる。

例： ${\mathbb N}_0$

　 ${\mathbb N}_0$ には要素がないので、導入則がない。なので

　 $\bot \equiv \emptyset \equiv {\mathbb N}_0$

とするのは自然である。

${\mathbb N}_0$ 除去則

　要素 $c \in {\mathbb N}_0$ はありえないので、 ${\textsf R}_0(c)$ を実行することはできない。 ${\textsf R}_0(c)$ という形のプログラムの命令の集合は空になる。これはダイクストラによって導入されたアボート（中断）という文と似ている。

$\bot$ 除去則

　 $C(z)$ が $z$ に依存していないとき、前提と帰結の証明（構成）を隠して $\bot$ 除去則を得る。矛盾からはなんでも出てくるというやつである。もうひとつの形の正当化もかいておいた。

例： ${\mathbb N}_1$

　 $\top \equiv {\mathbb N}_1$

と定義する。 ${\mathbb N}_1$ 導入則によって $0_1 \in {\mathbb N}_1$ を得るので $0_1$ は ${\mathbb N}_1$ の要素であり、 $\top$ は true である。

　 $0_1$ が ${\mathbb N}_1$ の唯一の要素であることは（たぶんカノニカルとかを無視して）図を参照。

例： ${\mathbb N}_2$

　 $Boolean \equiv {\mathbb N}_2$

と定義する。これはプログラミングにおける真理値 $\textsf{true, false}$ で構成される。 $\textsf{true} \equiv 0_2, \textsf{false} \equiv 1_2$ と定義しよう。すると $\textsf{if} c \textsf{then} c_0 \textsf{else} c_1 \equiv \textsf{R}_2(c, c_0, c_1)$ と定義できる。 $c$ が $\textsf{true}$ というのは $c$ を実行すると $0_2$ になるということで、 ${\mathbb N}_2$ 等号則によって $\textsf{R}_2(c, c_0, c_1)$ は $c_0$ と同じ値を持つ。そうでなければ、 $c$ を実行すると $1_2$ になり、 $\textsf{R}_2(c, c_0, c_1)$ は $c_1$ と同じ値を持つ。

　何故こんなに上手くいくのだろう？

　 ${\mathbb N}_2$ の要素が $0_2$ か $1_2$ であることは証明できるが、命題の形となる。図を参照。

例：否定

　~ $A \equiv \lnot A \equiv -A \equiv A \to {\mathbb N}_0$

とすると、いちばん右のに含意の導入と除去がそのまま使えるので、それがそのまま否定の規則になる。ここで $Cons \equiv \lnot Der('\bot') \equiv Der('\bot') \supset \bot$

無矛盾性

　規則の体系の無矛盾性について。

　無矛盾性は二つの方法で理解できる。

(1)数学的無矛盾性

　理論 $T$ の無矛盾性を証明するには、別の理論 $T'$ を考える。この $T'$ はもとの理論 $T$ の命題のコードと述語 $Der$ を持つ。 $Der('A')$ はコードが $'A'$ の命題 $A$ が $T$ で導出可能であるということを表す。ここで $Cons \equiv \lnot Der('\bot') \equiv Der('\bot') \supset \bot$ と定義して、 $Cons$ が $T'$ で true であることを（頑張って）証明する。この方法は、ヒルベルトがやったように、公理や推論規則の意味論的正当化を諦めるならできる。直観主義型理論でもやろうと思えばできるのだが、我々は構文論と同じくらい意味論も重視しているので、ここではそれをとらない。以下の単純な無矛盾性を考える。

　第2不完全性定理がらみの難しい話ですな。

(2)単純な無矛盾性

　単純に $\bot$ が証明できないこと、あるいは $\bot \; true$ という判断ができないということである。上の $Cons$ と違って数学的な命題ではない（よくわからないが）。こちらの無矛盾性は以下のように示す。

　 $c \in \bot$ とすると、 $c$ は実行したらカノニカルな要素 $d \in \bot$ となる。しかし $\bot$ は空集合なのでカノニカルな要素を持たない。 $\bot \; true$ が証明されるとしたら直観主義型理論の規則の何かが間違っていることになるが、（ザックリしているけど）そんなものはない。 $\bot$ を導出する規則などないので。よって $\bot \; true$ の証明はない。

　少なくとも $T'$ の単純な無矛盾性を仮定すれば、もとの $T$ の数学的無矛盾性からその単純な無矛盾性を出せる。：ある $c$ について $c \in Cons$ が証明できたとする。 $T$ が単純な無矛盾ではないとすると、 $T$ における $\bot \; true$ の証明、すなわちある $a$ について $a \in {\mathbb N}_0$ の証明がある。コーディングによって $'a' \in Der('\bot')$ が与えられる。 $c \in Cons$ とこれに $\supset$ 除去則を適用して $\textsf{Ap}(c, 'a') \in \bot$ を得る。すなわち $\bot \; true$ は $T'$ で導出可能である。よって $\bot \; true$ が $T'$ で証明可能でない、すなわち $T'$ が単純な無矛盾であると仮定するとメタな意味で矛盾し、下線部が否定される。