命題の概念の導入により、一階述語論理を型理論の中で模倣できる。
iを階数とする。
- -型⊤:U(0)を1と定義する。
- -型P,Q:U(i)に対して、型P∧Q:U(i)をP×Qと定義する。
- -型⊥:U(0)を0と定義する。
- -型P,Q:U(i)に対して、型P∨Q:U(i)を∥P+Q∥−1と定義する。
- -型P,Q:U(i)に対して、型P⇒Q:U(i)をP→Qと定義する。
- -型P:U(i)に対して、型¬P:U(i)をP⇒⊥と定義する。
- -型P,Q:U(i)に対して、型P⇔Q:U(i)を(P⇒Q)∧(Q⇒P)と定義する。
- -型A:U(i)と型の族P:A→U(i)に対して、型∀x:AP(x):U(i)を∏x:AP(x)と定義する。
- -型A:U(i)と型の族B:A→U(i)に対して、型∃x:AB(x):U(i)を∥∑x:AB(x)∥−1と定義する。
これらの記法は
Pや
Qが命題である場合に使い、結果も命題であることが分かる。
iを階数、P:U(i)を型とする。Pが命題である場合、「Pの要素がある」の代わりに「Pは真である」という言い方をする。
ただし、特別な公理を課さない限り型理論で模倣できる論理は直観主義論理である。特に、命題Pに対してP∨¬Pが真であるとは限らない。
排中律(law of excluded middle)は任意の階数iと型P:U(i)に対して、Pが命題ならばP∨¬Pが真であることを要請する。
排中律は従来の数学では当たり前のように使われるが、ホモトピー型理論ではほとんど排中律を仮定しない。