2022.08.11
https://gyazo.com/532bc405880b19dccccb61cc7ed01c72
観た
思った
まずデルタ型
$ \lnot \forall \xi. \varphi \Rightarrow \lnot \varphi\lbrack \zeta_i / \xi \rbrack
$ \exists \xi. \varphi \Rightarrow \varphi\lbrack \zeta_i / \xi \rbrack
ただし$ \zeta_iは過去のタブローに出現したどの論理式についてもその自由変項ではない
について
とりあえずまず可能な限り変項$ \zeta_iを創出しまくる
あまりにも大雑把に言えば，$ \exists\forall論理式は頑張ると$ \varphi_1 \lor \varphi_2 \lor \dots \lor \varphi_n（ただし$ \varphi_1\dots\varphi_nは量化子/変項/演算子を含まない述語論理の論理式）に変換出来ることが分かっており，これは命題論理の決定可能性および量化子を含まない述語論理の論理式に関しての決定可能性から決定可能である，というのがHerbrand定理周りの要約なのだろうか（ちゃんと読んでください！） 生産は両方の漢字が出生に関する漢字なのに人間に使う言葉ではないの非直感的すぎる
やった