SnO₂WMaN

#544 で`tailModel`を導入した最中に気付いたが，`extendRoot`の番号の割り振り方が意図したものと逆だった．本来は元のフレームの根に近いほど `0`，遠いほど大きな値にしないと`tailModel`と整合性が取れない．特に問題は無いかもしれないが，気になったら直す．

To prove #546

Autoprover for Modal Logic

1

特にこのあたりで顕著だが，`◇` や `□` の双対性などを形式的証明で扱うのは微妙に面倒なので，今はKripke意味論に帰着させて証明している． https://github.com/FormalizedFormalLogic/Foundation/pull/525/files#diff-f5899a18245603fffa46037c9f8e004e5163d5eb0e1ad963832f4e6d70b252fdR177-R198 しかし `K` で証明できることぐらいは自動化したい．

https://www2.kobe-u.ac.jp/~tk/jp/workshop/LWS2/LWS2.pdf の定理2.7．証明はこのpdfのものに基本的に沿うものとする．

Thanks @Rob23oba

add(FirstOrder): Church's Undecidability Theorem

9

現行の形式化ではいくつかの事実が弱く，示せないような気がする．

Blackburn, de Rijke, Venema, Prop 2.14

If $X \vdash_L \varphi$, then $X_0 \subseteq_\text{Fin} X$ and $n \in \omega$ exists s.t. $L \vdash \Box^{\leq n} \bigwedge X_0 \to \varphi$.