推論規則の表記

型あり→型規則の導出木

表記

規則X:\mathcal{J}_1かつ\mathcal{J}_2かつ\cdotsかつ\mathcal{J}_nならば、\mathcal{J}_0

を以下のように表記する

\frac{\mathcal{J}_1\,\mathcal{J}_2\cdots\mathcal{J}_n}{\mathcal{J}_0}\qquad(X)

水平線より上の前提が全て成り立つ場合に、下の結論を導出できることを示す

前提のない公理の場合は、水平線の上はない表記になる

\frac{}{0\in\mathcal{T}}

具体例

ペアノの公理の加算の定義を以下に示す

\frac{}{Z \, \mathrm{plus}\, n\, \mathrm{is} \, n}

\frac{n_1\,\mathrm{plus}\,n_2\,\mathrm{is}\,n}{S(n_1)\,\mathrm{plus}\,n_2\,\mathrm{is}\,S(n)}

関連

参考