feat(Modal): Boxdot Translation between `𝐆𝐋` and `𝐆𝐫𝐳` Part.1

FormalizedFormalLogic / Foundation

Lean4 Logic Formalization

Apache License 2.0

84 stars 5 forks source link

Closed SnO2WMaN closed 3 months ago

SnO2WMaN commented 3 months ago

𝐆𝐋は𝐆𝐫𝐳を介してboxdot変換で埋め込める．逆を証明するには意味論的な分析がいる（はず）

lemma boxdotTranslatedGL_of_Grz : 𝐆𝐫𝐳 ⊢! p → 𝐆𝐋 ⊢! pᵇ