[0057] 述語論理

$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}$と定義する。

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

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