3 ms·

How does that definition compare to the usual sense of "constructive"?

• ykonstant 3y ago
  I don't know, for two reasons: one, I am not sure about the relationship between the foundational type system Lean uses (the Calculus of Inductive Constructions) and usual set theories. Two, there is more than one notion of constructiveness, and I do not care to dig into the semantics of each. Myself, I am not a constructivist in any way. I just like to produce data whenever I can, and I believe that sometimes constructive proofs give additional insights for the objects we study; therein lies my interest in constructive arguments.
  • gowld 3y ago
    I was asking a less sophisticated question. I think the answer is "Lean is constructive if you use the base system without known non-constructive axioms".
  • eru 3y ago
    > Myself, I am not a constructivist in any way. I just like to produce data whenever I can, and I believe that sometimes constructive proofs give additional insights for the objects we study; therein lies my interest in constructive arguments. Constructive proofs also have an interesting relationship with algorithms to construct the object in question. (Funny enough, to proof some algorithms correct, you can use non-constructive proofs.)