LKで「恒真ではない」ことを示すのが難しい気がする

Summer498.icon

証明したい式が恒真な式　ならば　LKで証明する際の、ある完全分解木の葉は全て初期シークエントになることは分かるhttps://www2.yukawa.kyoto-u.ac.jp/~kanehisa.takasaki/edu/logic/logic9.html

任意の完全分解木の葉が全て初期シークエントになるとは言っていない

任意の～と仮定すると

証明したい式が恒真な式　ならば　LKで証明する際の、任意の完全分解木の葉は全て初期シークエントになる

対偶を取って

LKで証明する際の、ある完全分解木の葉は「全て初期シークエントになる」わけではない　ならば　「証明したい式が恒真な式」なわけではない

これは、ある完全分解木の葉が「全て初期シークエントになる」ときにも　「証明したい式が恒真な式」なわけではない　ことがあると言ってるようなもの

これはおかしい

ある完全分解木の葉が「全て初期シークエントになるなら、それを上から辿っていけば「証明したい式が恒真な式」だと分かる　から

よって対偶が偽

めっちゃふわっとした議論やなぁ

対偶が偽なので仮定が偽

つまり、完全分解木を組み立てる際ににハズレを引くこともあるということ＝そうでもない連言と二重否定の関係について#65b601f4ed60e60000f1b92a

DNF の恒真性の証明が NP 完全問題であることを思い出せば当然だったわSummer498.icon

ハズレ無しで LK の完全分解木を構築できるなら毎手毎手演算子が減るから P=NP になっちゃう

ホント？途中で複数の枝に分裂するタイミングがあるからそっちの作用でまだ P にはならなくないか

逆に証明したい式が恒真な式ではないことを証明するには、全ての完全分解木を検証して恒真でないことを示す必要がある

しんど！！！！Summer498.icon

完全分解木の枝分かれの際に一部恣意的な選択があるが、これを全網羅すれば恒真でないことの証明になるか？

実行順序は関係ないのか？