SnO₂WMaN
SnO₂WMaN
Add McKinsey axiom (M), K4.1 = K4 + M. S4.1 = S4 + M.
TODO: 補に関するMaximalConsistentSetに関する議論はModalと全く同じなのでどうにか共通化できないか検討する．
https://github.com/FormalizedFormalLogic/Foundation/blob/191915ab15a5a72ba2d62e3099f0e250475f4075/Foundation/ProvabilityLogic/Classification/GeneralizedTrace.lean#L382-L405 > 骨延長したフレームの高さは，元のフレームの高さ + 伸ばした分に等しい． > 骨延長したフレームの 0 以降は，元のフレームを a で切ってk-単純拡張したものと同型になっている．ここから様相同値が生える． #549 が問題になる可能性がある（定義側を変えればおそらくいいが）
https://github.com/FormalizedFormalLogic/Foundation/blob/191915ab15a5a72ba2d62e3099f0e250475f4075/Foundation/ProvabilityLogic/Classification/GeneralizedTrace.lean#L133 点生成されたフレーム上の点のランクは元のフレームのその対応する点のランクと等しい．
https://github.com/FormalizedFormalLogic/Foundation/blob/9d748422e298301f8366dacefb29a0b081c79e78/Foundation/ProvabilityLogic/Classification/LetterlessTrace.lean#L641-L643 逆はKripke意味論的議論ですこし煩雑．