lean4-logic
lean4-logic copied to clipboard
iehality
Lean4 Logic Formalization
Rewrite modal logic based on #44 Depends - #44 - #46 - #50
`๐๐ซ๐ข๐ฏ`ใจ`๐๐๐ซ`ใฏไปฅไธใฎๆๅณใงๆฅตๅคงใชๆญฃ่ฆๆง็ธ่ซ็ใงใใ๏ผ > [!NOTE] > ไปปๆใฎ็ก็็พใชๆญฃ่ฆๆง็ธ่ซ็`ฮ`ใซๅฏพใ๏ผ`ฮ โคแดธ ๐๐๐ซ`ใพใใฏ`๐๐ โคแดธ ฮ โคแดธ ๐๐ซ๐ข๐ฏ`ใฎใฉใกใใไธๆนใ ใใๆ็ซใใ๏ผ(Makinson, 1971) - [x] depends on: #39 - [ ] Classical Propositionalใฎๆๅณ่ซใ็จๆใใ๏ผๅฝ้ก่ซ็ใฎใใผใใญใธใผใใฉใใใซๅธฐ็ใใใ่จผๆใใใใใ๏ผ
`aesop`ใไฝฟใฃใฆ็ฐกๅใช่ชๅๅใๅ ฅใใฆใใใ๏ผ้ ใใไธๆใ่กใใชใใใจใๅคใไธไพฟ
่ฉณ็ดฐ: https://scrapbox.io/sno2wman/Boxdot%E7%89%B9%E6%80%A7 close #41
_Originally posted by @SnO2WMaN in https://github.com/iehality/lean4-logic/issues/34#issuecomment-2053638218_
