演繹
一般的な前提から、個別的な結論を導く論理的推論
推論していく元となるものが正しいかどうかは不明
それを正しいと仮定するなら、それによって導かれる結論は正しい
抽象から具体へ
例: Modus Ponens
全ての人間は死ぬ (大きな前提)
ソクラテスは人間である (↑を含意する前提)
だから、ソクラテスは死ぬ (結論)
例: 関数適用 ref
a の値に、 a->b の関数を適用すると、 b が得られる例: 公理系APLで用いているproofを一般化したもの
「公理」と「公理以外の仮定」から、推論して得ること
これを\Gamma\vdash Cと書く
論理式の集合\Gammaから、ごにょごにょしてCが得られるということ
\Gammaはいわば仮定の集まり
この中に入っているものを組み合わせてCを導く
公理は演繹の特別パターン
\vdash Cになっている
つまり仮定がない空集合からCが得られる
>
左側の矢印が大きな前提、右側の矢印が小さな前提
そこから赤矢印が得られる