Add Propositional Modal Logic

[SnO2WMaN]

close #9

[SnO2WMaN]

このPRでは標準的な様相論理の準備立て，及び $\mathbf{K}$ の弱い形の健全性定理 $\vdash \varphi \implies \vDash \varphi$ までの準備という形まで区切りにしようと思う．

残りは別のPRで出したい．

• 健全性定理 $\Gamma \vdash \varphi \implies \Gamma \vDash \varphi$
• 弱い形の完全性定理 $\vDash \varphi \implies \vdash \varphi$
• 一般的な形の完全性定理 $\Gamma \vDash \varphi \implies \Gamma \vdash \varphi$
• $\mathbf{S4}, \mathbf{S5}$などへの拡張

[SnO2WMaN]

このdefinesの定義は微妙な気がする．

[iehality]

ここでの"定義する"の用法が「数学における証明と真理」にあるものなら以下でよいと思う。

def Defines (fc : Frameclass α) (Γ : Context β) := ∀ f, f ∈ fc.frames ↔ ⊧ᶠ[f] Γ

以降にあるaxiomT.definesなどは代わりに以下のような命題を証明すれば良い（おそらく）。

lemma axiomT.defines : fc.Reflexive → (𝐓 : Context β).Defines fc := by

[iehality]

今気づいたんですがこれは間違っている。おそらく次をしめすか

lemma axiomT.defines : (𝐓 : Context β).Defines fc → fc.Reflexive

もしくは単に以下を示せば良いと思う（こちらのほうが良い気がする）。

lemma axiomT.defines : f.Reflexive ↔ ⊧ᶠ[f] 𝐓

[SnO2WMaN]

より端的に，もはやフレームクラスを使わずにこの形でいいのではないか？と思い書き直した．

lemma AxiomT.ctx.defines : Reflexive f.rel ↔ ⊧ᴹᶠ[f] 𝐓

[iehality]

多くて申し訳ない！

[iehality]

ここでの"定義する"の用法が「数学における証明と真理」にあるものなら以下でよいと思う。

def Defines (fc : Frameclass α) (Γ : Context β) := ∀ f, f ∈ fc.frames ↔ ⊧ᶠ[f] Γ

以降にあるaxiomT.definesなどは代わりに以下のような命題を証明すれば良い（おそらく）。

lemma axiomT.defines : fc.Reflexive → (𝐓 : Context β).Defines fc := by

[SnO2WMaN]

とりあえず全ての問題は直したと思うが，現在lean4のcache周りが壊れていてCIが通っていない．適当なタイミングでCIを再スタートしてほしい．

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20cache.20doesn't.20work

[iehality]

READMEを更新してもらえると助かる。

[SnO2WMaN]

READMEを追記．

[SnO2WMaN]

とりあえず全ての問題は直したと思うが，現在lean4のcache周りが壊れていてCIが通っていない．適当なタイミングでCIを再スタートしてほしい．

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/The.20cache.20doesn't.20work

MathlibのActionsを見るにおそらく復旧したのではないかと思う．再実行してもらえませんか？

[iehality]

問題なさそうなのでmergeします。