lean4-logic
lean4-logic copied to clipboard
feat(Modal): Maximality of `๐๐ซ๐ข๐ฏ` and `๐๐๐ซ`
๐๐ซ๐ข๐ฏใจ๐๐๐ซใฏไปฅไธใฎๆๅณใงๆฅตๅคงใชๆญฃ่ฆๆง็ธ่ซ็ใงใใ๏ผ
[!NOTE] ไปปๆใฎ็ก็็พใชๆญฃ่ฆๆง็ธ่ซ็
ฮใซๅฏพใ๏ผฮ โคแดธ ๐๐๐ซใพใใฏ๐๐ โคแดธ ฮ โคแดธ ๐๐ซ๐ข๐ฏใฎใฉใกใใไธๆนใ ใใๆ็ซใใ๏ผ(Makinson, 1971)
- [x] depends on: #39
- [ ] Classical Propositionalใฎๆๅณ่ซใ็จๆใใ๏ผๅฝ้ก่ซ็ใฎใใผใใญใธใผใใฉใใใซๅธฐ็ใใใ่จผๆใใใใใ๏ผ