タブロー法のときのように機会的には行えない

つまり、使う規則をミスると答えにたどり着けない

ので、使う規則は、考えて精査する必要がある

推論規則

規則一覧はこのページを参照

全ての推論規則に名前がついている

「~導入」は「~I」

「~除去」は「~E」

推論規則の読み方

以下のような規則があったとき、「∧i」の部分が規則名

「∧」を「導入(Introduction)」する規則ということ。

下段が「根」であり、上段が「葉」である

下段が「結論」であり、上段が「仮定」である

推論の手順

最下段の根から上向きに葉を生やしていく

葉は前提かスタックしたものでないといけない

全ての葉が以下のいずれかになるように進めていく

仮定

解消される仮定

仮定の種類

解消されていない仮定

解消された仮定

推論の例

三段論法: \alpha\rightarrow\beta, \beta\rightarrow\gamma \vdash\alpha\rightarrow\gammaを示す

つまり根に結論\alpha\rightarrow\gamma、葉に前提\alpha\rightarrow\betaと\beta\rightarrow\gammaが来ればいい

1.

推論規則を見て、結論が同じ形のものを探す

当てはまるものが複数あるなら、仮定の方も見て扱いやすいものを選ぶ

根から書いていく「→導入」を使った

ここで「\alpha」に対する条件がスタックされている

2.

普通に「→除去」を適用

左上の\beta\rightarrow\gammaは仮定なので、コレは葉になる

3.

最後に「→除去」を適用

ここで右肩の\alphaはどこから来たの？って話になるが、手順1でのスタックがあるのでそれを使う

参考

詳説

例題など

localの「数理論理学」というpdfが詳しい

3章の最後の方に例題がいっぱい載ってる！