lean4-logic

lean4-logic copied to clipboard

現状理論 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₀ ⊢!. (𝔅 σ) ➝ 𝔅 (𝔅 σ)

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