導出木 - mrsekut-p

導出木

推論規則の表記

表記

規則$ 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)}