search

FormalizedFormalLogic / Foundation

Lean4 Logic Formalization
https://formalizedformallogic.github.io/Summary/
Apache License 2.0
84 stars 5 forks source link

feat(Modal): Rewrite completeness of `𝐆𝐋` #123

Closed SnO2WMaN closed 3 months ago

SnO2WMaN commented 3 months ago

濾過法の同値関係を使ったGLの完全性証明を，使わない証明に書き換えた．

close after #124

SnO2WMaN commented 3 months ago

濾過法の同値関係を使った証明の形式化も残してはおきたい（おそらくこの方法の形式化はMaggessi & Brogiにはない）が，リファクタリングで変に困る気もするので一旦削除することにする．