3 ms·
>Finally, if you can't claim Lean is good enough for all Mathematics then you can't claim it for any existing system or any system that doesn't take classical l
by logicchains 6y ago
>Finally, if you can't claim Lean is good enough for all Mathematics then you can't claim it for any existing system or any system that doesn't take classical logic seriously (postulating an axiom doesn't count).
Correct me if I'm wrong (I may well be), but couldn't one work classically just by sticking to (-1)-truncated types ("mere prepositions") in a HOTT based system, for which LEM is true by default?
- hejsansvejsan 6y agoLEM for mere propositions is not "true by default", but it is consistent with univalence. So you can take it as an axiom.