Fix propositional variables in modal logic

[SnO2WMaN]

様相論理のKripke意味論においてやはりFrame.alt αのように命題変数の型に（幽霊型として）依存するような実装は気持ち悪く，また実装も妙なところで煩雑になってしまっている気がする． 以前なんらかの際に述語論理側は（特に算術では）言語を固定して議論しているような実装になっていると言っていた記憶があり，その方針に沿おうかなと思っている．すなわち今現在，様相論理側でαとして自由度を持たせている意味は特に無いはずなので，意味論の定義などはFormula Nat（Natでなくともよい）に固定しようかなと思っているのだが，どう思うだろうか．

[iehality]

以前なんらかの際に述語論理側は（特に算術では）言語を固定して議論しているような実装になっていると言っていた記憶があり

議論するの意味にもよるがこれはおそらく間違いだと思う．現時点では言語を固定しなくて良いならば通常の意味論や等号を含む意味論なども全て固定せずに議論している（算術の理論のモデルなどを考えるときは，定義上 $\mathcal{L}_{OR}$のモデルのみを扱わなければならないが （しかしその場合でも $\mathcal{L}_{OR}$ を含む任意の言語のモデルの議論とはあまり変わらない））．

できるだけ非本質的な拘束はしたくないので，α はパラメータとするべきだと思うが，それでどのような問題が起きる/起きうるのか教えてほしい．

[SnO2WMaN]

大雑把にこんな問題が思いつく，あまり本質的な問題ではないと言われたらそれまでですが．

---

例えば今S4_Soundは以下のようになっているが，フレームクラス側に#αのようにあたかも依存してしまっているように見えるし，さらに言えばこの場合αはInhabitedであることを要請しているので単にフレームの集まりであるフレームクラスに対して命題変数に関する要請が入ってきてしまっているのであまり良くないように思える．（これは主観的な意見です．）

instance S4_sound : Sound (𝐒𝟒 : Hilbert α) (PreorderFrameClass#α) := inferInstance

---

（これは勘違いで全然関係ないかもしれません）

またFormulaでα : Type uとしていてかなり自由度があり，これが以下の主張において型レベルを指定する必要があるとにらんでいる．今後このような事態は避けたい．

theorem undefinable_irreflexive : ¬∃ (Λ : Hilbert α), ∀ F, F ∈ 𝔽(Λ) ↔ F ∈ IrreflexiveFrameClass.{0}

（追記：GLのKripke意味論周りはこの問題がかなり顕著にあらわれている）

---

今，αがInhabited, DecidableEqなどの性質を満たすかどうかは各命題たちに対して個別に指定しているが，普通の様相論理でそこまで細かく条件を精査する必要があるかは正直疑問がある．普通の慣習上または暗黙の了解に従ってInhabited, DecidableEqなどの命題変数の集合としては当然あってほしい性質を満たすPropVarのような型を適当に導入してそれで固定すれば十分では，という気がする． これは実装上楽をしたいのもあるが，たまにDecidableEqであるという条件が外れていてSupplemantalのdeductを使う証明がsimpなどで通らないことをうっかり気が付かないときがある，などのミスを避けたいという気持ちもややある（よくやってしまうので）．

---

ともかくとして，命題変数を固定するように書き換えてみて，うまくいきそうならPRを出してみます．

[iehality]

理解した．ただ命題変数をℕに固定するなら，意味論だけでなく論理式の定義からそのように書き直したほうが自然だし，簡潔になるんじゃないだろうか．

[SnO2WMaN]

それはそう．