述語論理 -- ホモトピー型理論

命題の概念の導入により、一階述語論理を型理論の中で模倣できる。

$$i$$ を階数とする。

-型 $\top :\mathcal {U}(0)$ を $\mathbf {1}$ と定義する。
-型 $P,Q:\mathcal {U}(i)$ に対して、型 $P\land Q:\mathcal {U}(i)$ を $P\times Q$ と定義する。
-型 $\bot :\mathcal {U}(0)$ を $\mathbf {0}$ と定義する。
-型 $P,Q:\mathcal {U}(i)$ に対して、型 $P\lor Q:\mathcal {U}(i)$ を ${\| P+Q\| }_{-1}$ と定義する。
-型 $P,Q:\mathcal {U}(i)$ に対して、型 $P\Rightarrow Q:\mathcal {U}(i)$ を $P\to Q$ と定義する。
-型 $P:\mathcal {U}(i)$ に対して、型 $\neg P:\mathcal {U}(i)$ を $P\Rightarrow \bot$ と定義する。
-型 $P,Q:\mathcal {U}(i)$ に対して、型 $P\Leftrightarrow Q:\mathcal {U}(i)$ を $(P\Rightarrow Q)\land (Q\Rightarrow P)$ と定義する。
-型 $A:\mathcal {U}(i)$ と型の族 $P:A\to \mathcal {U}(i)$ に対して、型 $\forall _{x:A}P(x):\mathcal {U}(i)$ を $\prod _{x:A}P(x)$ と定義する。
-型 $A:\mathcal {U}(i)$ と型の族 $B:A\to \mathcal {U}(i)$ に対して、型 $\exists _{x:A}B(x):\mathcal {U}(i)$ を ${\| \sum _{x:A}B(x)\| }_{-1}$ と定義する。

これらの記法は

\(P\)

や

\(Q\)

が命題である場合に使い、結果も命題であることが分かる。

[005A] 用語

$$i$$ を階数、 $P:\mathcal {U}(i)$ を型とする。 $$P$$ が命題である場合、「 $$P$$ の要素がある」の代わりに「 $$P$$ は真である」という言い方をする。

ただし、特別な公理を課さない限り型理論で模倣できる論理は直観主義論理である。特に、命題

\(P\)

に対して

P\lor \neg P

が真であるとは限らない。

[0059] 公理(排中律)

排中律(law of excluded middle)は任意の階数 $$i$$ と型 $P:\mathcal {U}(i)$ に対して、 $$P$$ が命題ならば $P\lor \neg P$ が真であることを要請する。

排中律は従来の数学では当たり前のように使われるが、ホモトピー型理論ではほとんど排中律を仮定しない。

[0057] 述語論理