It’s standard to say that the axiom of choice is equivalent to the well-ordering principle, which means that if you add either to ZF, the other follows and you get ZFC. As I’m reading this, the relevant paragraph in the OP reads,
Notice though: ECQ and TND are both theorems (or axioms) of classical logic. They are in fact equivalent. ECQ is espressed as ¬(A∧¬A), but under the DeMorgan laws, double negation elimination and commutativity of disjunction: ¬(A∧¬A)↔(¬A∨¬¬A)↔(¬A∨A)↔(A∨¬A), which is the TND.
So I interpret MrMind as giving the analogous statement with ZF → (DeMorgan + DNE + commutativity of disjunction + possibly something else?), axiom of choice → ECQ, well-ordering principle → TND, and ZFC → “classical logic” … which is probably meant to mean classical propositional logic in this context?
I haven’t checked this claim, if indeed that was what was intended, though.
The problem is that double negation elimination is already equivalent to classical logic (i.e. adding double negation elimination to minimal logic gives the law of excluded middle as a theorem), so there is no “background theory” like ZF to work in.
Ah, okay. I had been interpreting him as saying that they are equivalent in classical logic. But yeah, they probably are equivalent under a weaker subset of classical logic in which neither is a theorem on its own.
Yes, that’s what equivalence means. And if X and Y are both theorems, then if you assume either as an axiom, then the other must follow as a theorem.
It’s standard to say that the axiom of choice is equivalent to the well-ordering principle, which means that if you add either to ZF, the other follows and you get ZFC. As I’m reading this, the relevant paragraph in the OP reads,
So I interpret MrMind as giving the analogous statement with ZF → (DeMorgan + DNE + commutativity of disjunction + possibly something else?), axiom of choice → ECQ, well-ordering principle → TND, and ZFC → “classical logic” … which is probably meant to mean classical propositional logic in this context?
I haven’t checked this claim, if indeed that was what was intended, though.
The problem is that double negation elimination is already equivalent to classical logic (i.e. adding double negation elimination to minimal logic gives the law of excluded middle as a theorem), so there is no “background theory” like ZF to work in.
Ah, okay. I had been interpreting him as saying that they are equivalent in classical logic. But yeah, they probably are equivalent under a weaker subset of classical logic in which neither is a theorem on its own.