Martin-Löf型理論の記法など

判断(justification)

型$ A

型の要素$ a : A

あらゆる数学的対象は型(type)を持つ。数学的対象$ a が型$ A を持つことを

$ a: A

と書く。

$ a は型$ A の要素(element)であるともいう。

数学的対象は変数(variable)に依存する場合もあり、$ a が変数$ x に依存するかもしれないことを強調するときは$ a を$ a[x] と書く。

$ a[x] 中$ x に数学的対象 $ b を代入して得られる数学的対象を $ a[b] と書く。

二つの数学的対象が等しいことを $ a \equiv b で表す。

数学的対象$ a に名前 $ f を付けるときには$ f:\equiv a と書き、$ f を$ a と定義するなどと言う。

各型について4つの推論規則(inference rules)がある

形成規則(formation rule)

導入規則(introduction rule)

除去規則(elimination rule)

等号規則(equality rule)

命題を型として書くと以下の表な表記になる。

$ \begin{array}{rcl}\bot & = & \varnothing \\ \top & = & 1 \\ A \lor B & = & A + B \\ A \land B & = & A \times B \\ A \supset B & = & A → B \\ \exist x:A.B & = & \Sigma x: A.B \\ \forall A.B & = & \Pi X:A.B \end{array}