ゲンツェンの自然演繹(NK)
Natural deduction
つまり、使う規則をミスると答えにたどり着けない
ので、使う規則は、考えて精査する必要がある
推論規則
全ての推論規則に名前がついている
「~導入」は「~I」
「~除去」は「~E」
推論規則の読み方
以下のような規則があったとき、「∧i」の部分が規則名
「∧」を「導入(Introduction)」する規則ということ。
下段が「根」であり、上段が「葉」である
下段が「結論」であり、上段が「仮定」である
https://gyazo.com/53c0f5c59ff4fe2b9aa214d927cb0af5
推論の手順
最下段の根から上向きに葉を生やしていく
葉は前提かスタックしたものでないといけない
全ての葉が以下のいずれかになるように進めていく
仮定
解消される仮定
仮定の種類
解消されていない仮定
解消された仮定
推論の例
三段論法: $ \alpha\rightarrow\beta, \beta\rightarrow\gamma \vdash\alpha\rightarrow\gammaを示す つまり根に結論$ \alpha\rightarrow\gamma、葉に前提$ \alpha\rightarrow\betaと$ \beta\rightarrow\gammaが来ればいい
1.
https://gyazo.com/10a3e3b473ca29ff4313c633bc2b831b
推論規則を見て、結論が同じ形のものを探す
当てはまるものが複数あるなら、仮定の方も見て扱いやすいものを選ぶ
根から書いていく「→導入」を使った
ここで「$ \alpha」に対する条件がスタックされている
2.
https://gyazo.com/34bff56d4b176e1825892bc656a42a8c
普通に「→除去」を適用
左上の$ \beta\rightarrow\gammaは仮定なので、コレは葉になる
3.
https://gyazo.com/b82854ded61ea00d0641b6b505c337e1
最後に「→除去」を適用
ここで右肩の$ \alphaはどこから来たの？って話になるが、手順1でのスタックがあるのでそれを使う
参考
詳説
例題など
localの「数理論理学」というpdfが詳しい
3章の最後の方に例題がいっぱい載ってる！