# Is there a precise sense in which ZF is constructive

Often times proofs in ZF which do not use the axiom of choice are called constructive, but of course really it is easy to create non constructive proofs using LEM. Is there a precise sense in which ZF is more constructive than working without LEM in the logic?

Basically I am asking what is the advantage of proving things in ZF vs. ZFC when ZF is also not constructive. Is there a certain notion which says that if I prove something in ZF then there is a way in which my proof is a little more constructive? How to make the notion of little more precise.

• See Constructive Set Theory: Constructive and intuitionistic Zermelo-Fraenkel set theories are based on intuitionistic rather than classical logic. [...] The theories Constructive Zermelo-Fraenkel (CZF) and Intuitionistic Zermelo-Fraenkel (IZF) are formulated on the basis of intuitionistic first order logic." Oct 11, 2021 at 8:02
• @MauroALLEGRANZA I am asking I what sense is zf more constructive? Oct 11, 2021 at 8:05
• AC implies LEM, so you get ZF from intuitionistic ZF by adding a strictly weaker axiom than the one you are adding for ZFC. Your second sentence is odd, ZF is not "more constructive" than working without LEM, it is less since it includes LEM. But it is "more constructive" than ZFC. Oct 11, 2021 at 8:26
• @Conifold edited Oct 11, 2021 at 8:32
• Oct 11, 2021 at 9:02