言語 L の型付け関係

定義 5.1（「プログラミング言語論」§5）

型を $T ::= \mathtt{Bool} \mid \mathtt{Nat}$ とする。関係 $\vdash t : T$ （項 $t$ は型 $T$ を持つ）を次の規則で生成される最小の関係とする。

\begin{aligned} &\text{(T-True)} && \vdash \mathtt{true} : \mathtt{Bool} \qquad &&\text{(T-False)} && \vdash \mathtt{false} : \mathtt{Bool} \qquad &&\text{(T-Zero)} && \vdash \mathtt{0} : \mathtt{Nat} \\[4pt] &\text{(T-If)} && \frac{\vdash t_1 : \mathtt{Bool} \quad \vdash t_2 : T \quad \vdash t_3 : T}{\vdash \mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 : T} &&\text{(T-Succ)} && \frac{\vdash t : \mathtt{Nat}}{\vdash \mathtt{succ}\ t : \mathtt{Nat}} \\[4pt] &\text{(T-Pred)} && \frac{\vdash t : \mathtt{Nat}}{\vdash \mathtt{pred}\ t : \mathtt{Nat}} &&\text{(T-Iszero)} && \frac{\vdash t : \mathtt{Nat}}{\vdash \mathtt{iszero}\ t : \mathtt{Bool}} \end{aligned}

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

証明で明示的に参照している定理は、まだありません。