9 ms·

Lean’s type theory extends CIC with the (global) axiom of choice, which increases consistency strength over base CIC.

• wk_end 1y ago
  Slightly out of my depth, but per Diaconescu's theorem [0] axiom of choice implies the law of the excluded middle. Does that make Lean non-constructive? [0] https://en.wikipedia.org/wiki/Diaconescu%27s_theorem https://en.wikipedia.org/wiki/Diaconescu%27s_theorem
  • cwzwarich 1y ago
    Yes, in fact Lean proves the law of the excluded middle using Diaconescu's theorem rather than assuming it as an independent axiom: https://github.com/leanprover/lean4/blob/ad1a017949674a947f0d6794cbf7130d642c6530/src/Init/Classical.lean#L35-L67 https://github.com/leanprover/lean4/blob/ad1a017949674a947f0...
  • cvoss 1y ago
    Yes, but for an even more immediate reason. The axiom of choice itself is a non-constructive axiom. It asserts the existence of the inhabitant of a certain type, without in any way furnishing the inhabitant. But Lean sequesters off the classical logic stuff from the default environment. You have to explicitly bring in the non-constructive tools in order to access all this. So, actually, I would disagree with GP that Lean's type system includes a choice axiom.
    • nrds 1y ago
      Right, I was about to comment the same thing that "Lean" does not itself assume choice. Mathlib4 does, and Lean4 is designed so that all the built-in stuff is _consistent_ with choice. But you can do purely constructive mathematics in Lean and it's is even designed so that any non-propositions depending on choice have to be annotated "noncomputable", so the walled garden of choice is baked in at a language level. Even within "noncomputable" code, choice still shows up in the axiom list if used.