= 27d567bc2d48d9f40e9ccc20ea370b15)
AlexMennen comments on Constructive mathemathics and its dual - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (30)
Nitpick: any 2 theorems are equivalent to each other, so that's redundant. Perhaps you meant to say that they are in fact intuitively related to each other.
Maybe a better phrasing could have been: if you assume one as an axiom, the other follows as a theorem.
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.