2024.03.23
https://www.youtube.com/watch?v=3g-gzibOR-A
メモ
一部の補題が意味論経由で証明していてグニャグニャになってる
prover作りたすぎる…
が現状のやりかたでどうしようか迷う
現状では演繹体系が完全に直観主義論理専用になってしまっている やりようとしては最小命題論理の演繹体系をベースにして追加で公理を足すのが良さそうだろうか? すなわち
爆発律の論理式全体の集合$ \mathbf{EFQ} = \{\bot \to \varphi \mid \varphi \in \mathrm{Form} \} 排中律の論理式全体の集合$ \mathbf{LEM} = \{\varphi \lor \lnot\varphi \mid \varphi \in \mathrm{Form} \} として
$ \varphi \in \mathbf{LEM} \implies \vdash_{\mathbf{HM + LEM}} \varphi
$ \varphi \in \mathbf{EFQ} \implies \vdash_{\mathbf{HM + EFQ}} \varphi
のように…
これは様相論理のほうで採用しているアプローチに近い
思った
メモ
In 2014 CADE Inc. established the Thoralf Skolem Award to reward a CADE paper that has passed the test of time, by being a most influential paper in the field. Beginning with CADE-25 (2015), at every CADE the Skolem Award Committee selects a paper presented at the CADE held 10 years earlier to receive the Skolem
要するに論文に与えられる?
In 1992 CADE Inc. established the Herbrand Award for Distinguished Contributions to Automated Reasoning
こちらは人間に与えられている気がする
思った
思った
メモ
似たような結果が増えすぎてすごく面倒なので,Geach公理に合わせて一般化することでフレーム定義性 / 完全性定理を書き直したいという目標がある 思った
中間論理は非加算無限個存在するとはどういうことなのか?(単に可算無限なだけでなく非加算なのはなぜか) メモ