Provable predicate should not depend on base theory

[iehality]

現状理論 T の可証性述語 ProvabilityPredicate U T はその性質を保証するベース理論である U にも依存しているが，可証性述語それ自体は U に依存しないのだから依存すべきでないと思う．

structure ProvabilityPredicate (T : Theory L) where
  prov : Semisentence L 1

class HBL (T₀ : Theory L) (𝔅 : ProvabilityPredicate T) where
  D1 {σ : Sentence L} : T ⊢!. σ → T₀ ⊢!. prov/[⌜σ⌝]
  D2 {σ τ : Sentence L} : T₀ ⊢!. 𝔅 (σ ➝ τ) ➝ (𝔅 σ) ➝ (𝔅 τ)
  D3 {σ : Sentence L} : T₀ ⊢!. (𝔅 σ) ➝ 𝔅 (𝔅 σ)

のように定義し直すのはどうだろうか？

[SnO2WMaN]

可証性述語の本質的性質を捉えるために入れておいたが，確かに形式化の上でそうである必要は特になかった．修正します．

[SnO2WMaN]

書き直しを試してみたが，却ってベース理論が適切に推論されずに冗長に引数を指定する必要が生じて煩雑になってしまう気がする．困るなら修正するが，そうでないならこのままでも良いとも思う．

[iehality]

T₀ を outParam で指定するのはどうだろうか．