Refactor Provability Predicate and Arithmetical Soundness

[SnO2WMaN]

いくつか変更した。以下は主要な変更点についてのメモ。気になる点があったら指摘してほしい。

---

structure ProvabilityPredicate [Semiterm.Operator.GoedelNumber L (Sentence L)] (T₀ : Theory L) (T : Theory L) where
  prov : Semisentence L 1
  spec {σ : Sentence L} : T ⊢!. σ → T₀ ⊢!. prov/[⌜σ⌝]

以前までは異なる言語L₀とLをパラメータとして与えることが可能だったが、証明可能性述語としてそのようなものを考えるだろうか？と思い両方とも同じ言語のTheory上に定義するようにした。
D1はそもそも証明可能性述語として当然要請されるはずの前提（無いと逆に証明可能性述語とは呼ばないと思う）なのでこれは組み込みで入れるようにした。（定義上はspecとしているが別名として後でD1として定義し直している、このようにしないと毎回𝔟.D1のように呼び出す羽目になって表記上のバランスがよくない）

---

instance (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable]
  : ArithmeticalSoundness (𝐆𝐋 : Hilbert α) (T.standardDP T) := ⟨arithmetical_soundness_GL⟩

$\Delta_1$ 定義可能な $\bf I\Sigma_1$ の任意の拡大理論 $T$ は $\bf GL$ について算術的健全という事実だが、ここでは $\mathrm{Pr}_T$ を明確に指定している。証明可能性論理における普通の用法としては、証明可能性述語がどれかというのは気にせずに理論に対して算術的健全と言うと思うので、ここでの定義は少し変という気もする（どうしようもないが）。

---

タイミングが悪く FormalizedFormalLogic/Foundation#132 の変更がArithmetization側のFoundationに取り込まれていないのと、おそらく今後もFoundationのModal側で何かしら $\bf GL$ やKripke意味論に関する修正をするかもしれないので Foundationにも依存するようにしたが、これがArithmetizationで依存しているFoundationと競合したりするかもしれない。現状は特に何も起きていないが…

[iehality]

ArithmetizationとIncompletenessのmasterを一応アップデートした．一部対応する補題がわからずコメントアウトしたので適当に上書きしてほしい．

[iehality]

ところで⦍𝔟⦎の表記は煩わしい気がしており，instance : CoeFun (ProvabilityPredicate T₀ T) (fun _ => Sentence L)を定義するのはどうだろう．またinterpretationはProvabilityPredicateのnamespace下に定義して𝔟.interpret f pのような表記で書いたほうが見やすいと思う．

[SnO2WMaN]

レビューを受け修正。問題なければマージする。

Modal/以下はProvabilityLogicに移している。

前者についてはCoeFunを入れた。それに辺り𝔟だと小さくて見にくいので証明可能性述語は𝔅とすることにした。

後者についてはRealization以下に生やした。（正直まだ算術的完全性の形式化に着手していないので表記の見やすさはどうなるかはわからない）

[SnO2WMaN]

修正しました。マージします。