1
$\begingroup$

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.

$\endgroup$
8
  • $\begingroup$ 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." $\endgroup$
    – Mauro ALLEGRANZA
    Oct 11, 2021 at 8:02
  • $\begingroup$ @MauroALLEGRANZA I am asking I what sense is zf more constructive? $\endgroup$
    – Violet Flame
    Oct 11, 2021 at 8:05
  • $\begingroup$ 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. $\endgroup$
    – Conifold
    Oct 11, 2021 at 8:26
  • $\begingroup$ @Conifold edited $\endgroup$
    – Violet Flame
    Oct 11, 2021 at 8:32
  • 5
    $\begingroup$ See MathOverflow, In what ways is ZF (without Choice) "somewhat constructive"? $\endgroup$
    – Conifold
    Oct 11, 2021 at 9:02

1 Answer 1

Reset to default
0
$\begingroup$

The Math Overflow thread

Summarises my question pretty nicely and answers its too.

[I'm making a CW answer to get this of the unanswered list]

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.