ホモトピー型理論

[0057] 述語論理

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

[0058] 記法

iiを階数とする。

  • -:U(0)\top :\mathcal {U}(0)1\mathbf {1}と定義する。
  • -P,Q:U(i)P,Q:\mathcal {U}(i)に対して、型PQ:U(i)P\land Q:\mathcal {U}(i)P×QP\times Qと定義する。
  • -:U(0)\bot :\mathcal {U}(0)0\mathbf {0}と定義する。
  • -P,Q:U(i)P,Q:\mathcal {U}(i)に対して、型PQ:U(i)P\lor Q:\mathcal {U}(i)P+Q1{\| P+Q\| }_{-1}と定義する。
  • -P,Q:U(i)P,Q:\mathcal {U}(i)に対して、型PQ:U(i)P\Rightarrow Q:\mathcal {U}(i)PQP\to Qと定義する。
  • -P:U(i)P:\mathcal {U}(i)に対して、型¬P:U(i)\neg P:\mathcal {U}(i)PP\Rightarrow \bot と定義する。
  • -P,Q:U(i)P,Q:\mathcal {U}(i)に対して、型PQ:U(i)P\Leftrightarrow Q:\mathcal {U}(i)(PQ)(QP)(P\Rightarrow Q)\land (Q\Rightarrow P)と定義する。
  • -A:U(i)A:\mathcal {U}(i)と型の族P:AU(i)P:A\to \mathcal {U}(i)に対して、型x:AP(x):U(i)\forall _{x:A}P(x):\mathcal {U}(i)x:AP(x)\prod _{x:A}P(x)と定義する。
  • -A:U(i)A:\mathcal {U}(i)と型の族B:AU(i)B:A\to \mathcal {U}(i)に対して、型x:AB(x):U(i)\exists _{x:A}B(x):\mathcal {U}(i)x:AB(x)1{\| \sum _{x:A}B(x)\| }_{-1}と定義する。
これらの記法はPPQQが命題である場合に使い、結果も命題であることが分かる。

[005A] 用語

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

ただし、特別な公理を課さない限り型理論で模倣できる論理は直観主義論理である。特に、命題PPに対してP¬PP\lor \neg Pが真であるとは限らない。

[0059] 公理(排中律)

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

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