4 ms·

Lean is a classical theory, I don't see how any intuitionistic theory can hope to possibly compete. A mathematician would laugh you out of the store if you trie

by voxl 6y ago

Lean is a classical theory, I don't see how any intuitionistic theory can hope to possibly compete. A mathematician would laugh you out of the store if you tried to get them to used cubical Lean (Lean 2 by the way implemented HoTT ideas) and give up classical logic. The HoTT people are doing good work and I don't doubt that automation can help with the _significant_ additional complexity of higher dimensional cubes, but that's not really all that would be missing. 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).

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 ago
  LEM for mere propositions is not "true by default", but it is consistent with univalence. So you can take it as an axiom.
zozbot234 6y ago
Proving "classical" propositions in an intuitionistic system is trivial. Intuitionistic logic can be viewed as an extension of classical logic with new "constructive OR" and "constructive EXISTS" operators. The classical operators are recovered via negation: NOT (NOT a AND NOT b) is classical OR, whilst NOT FORALL x (NOT p) is a classical existential quantifier.
hejsansvejsan 6y ago
I'm confused by "postulating an axiom doesn't count". Are you aware that choice is an axiom in Lean? https://github.com/leanprover-community/lean/blob/master/library/init/classical.lean#L13 https://github.com/leanprover-community/lean/blob/master/lib...
tlringer 6y ago
Lean isn't classical. Lean is the calculus of inductive constructions with uniqueness of identity proofs. Classical logic in Lean requires using axioms.

by voxl 6y ago

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 ago
LEM for mere propositions is not "true by default", but it is consistent with univalence. So you can take it as an axiom.

zozbot234 6y ago

Proving "classical" propositions in an intuitionistic system is trivial. Intuitionistic logic can be viewed as an extension of classical logic with new "constructive OR" and "constructive EXISTS" operators. The classical operators are recovered via negation: NOT (NOT a AND NOT b) is classical OR, whilst NOT FORALL x (NOT p) is a classical existential quantifier.

hejsansvejsan 6y ago

I'm confused by "postulating an axiom doesn't count". Are you aware that choice is an axiom in Lean? https://github.com/leanprover-community/lean/blob/master/library/init/classical.lean#L13 https://github.com/leanprover-community/lean/blob/master/lib...

tlringer 6y ago

Lean isn't classical. Lean is the calculus of inductive constructions with uniqueness of identity proofs. Classical logic in Lean requires using axioms.