On `Semantics` category

[iehality]

• 複数の論理体系に共通する意味論を扱う際に一つのカテゴリに制限したくない．
• 一般に分離できるものは分離したほうが scalability などの観点から好ましい．
• ロジックに関わる議論と意味論に関する組み合わせ論的議論が混雑していると見通しがつきにくい．

などの理由から LO.MagariAlgebra や（可能であれば）一部の Kripke意味論など，それ自体は論理学の枠組みから自由なものは Foundation/Semantics カテゴリに移動したほうが良いと思っているがどうだろうか？

@SnO2WMaN

[SnO2WMaN]

べき論で言えばそうするべきだと思うが，本当にそう上手く可能なのだろうか，早すぎる共通化になってしまってないか，という懸念（特にKripke意味論とか）がずっとある．代数とかは上手くやれそうだが…

[iehality]

Kripke 意味論については，現状の様々なヴァリアントにその結果を再利用できるような扱いやすい，純粋に組み合わせ論的な基盤を作るべきだと思っている．
おそらく現状の Kripke モデルは散在しているうえにおそらくあまり扱いやすくないので，例えば，次のように定義したい．

structure Prekripke (α : Type*) where
  points : Set α
  Rel : α → α → Prop
  po : IsPartialOrder points fun x y ↦ Rel x y

（定義方法については，mathlib がグラフ理論にどのように取り組んでいるかが参考になるかもしれない． cf. https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Graph.20Minors ）．

うまくやれば #561 や #562 のようなものももっと簡単に解決できるだろうと思う．

[iehality]

Vorspiel/Rel もそこに置くには独自性の強い要素が多いので Semantics 下においてよいと思う．