Hacker News Reader

Comment by tromp | Hacker News Reader

The CoC implementation includes inductive types, so is this an implementation of CiC, the Calculus of Inductive Constructions, with the same proving power as Lean?

View on HN

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

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

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/ad1a017949674a947f0...

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.

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.

Reply on news.ycombinator.com