SnO₂WMaN

Visserの定理（黒本 Thm 5.3.3） #304 のあとにマージする．

適切にスコープやファイルを分け，依存関係の更新の手間を減らしたり，そもそもMathlibに移管したりしたほうが良さそうなものなどを検討したりしたほうがよさそうな気もする．

証明を読む感じではKripkeフレーム側の操作としても，算術としても，形式化できるのかという目処は全くつかない．

Kriesel-Putnamの論理はDPを持つ．

Auto proving for formula with modal degree is 0

1

AutoProverを適当に使えば様相次数が0の論理式のトートロジー判定は自動で出来るはず？

> Let $L$ be consistent normal modal logic and $\varphi \notin \mathbf{Ver}$ and $\varphi \in L$, then some formula $\psi$ exists s.t. $\diamond\psi \in L$ 参考にしている資料によると様相CNFと様相DNFを考えてこの$\psi$の存在を示すが，あまりにも形式化が面倒なので別の方法で示せるなら示したい．

Generating kite for arithmetics is broken

1

多分なのだが，算術のKiteを生成するのに膨大なメモリを要求しており，GitHub Actions上で生成することが出来ないので，もっと良い実装を与える

Function calculates Gödel number of negated sentence

1

問題意識としては https://github.com/FormalizedFormalLogic/Foundation/issues/108 も参照 文 `σ` に対して `⌜∼σ⌝ = neg ⌜σ⌝` となる関数 `neg` の構成と，その利用として `“x. ¬!𝔅.prov (neg x)”`: $\lnot \mathrm{Pr}(\dot{\lnot}(x))$ のような論理式を考えたいのだが，どう定義すればいいのかよくわからなかった．良い案はあるだろうか？