HNHacker News
TopNewBestAskShowJobs

stacksemantics

3 karma · joined December 2, 2020

submissionscomments
stacksemantics··on Formalising Mathematics: An Introduction
Constructive mathematicians do not assert that excluded middle is true since there is no constructive proof of (P not P). Nor do they assert that it is false, since that statement, (not (P or not P)), is constructively refutable i.e. there is a constructive proof of (not not (P or not P)). So there are no instances in constructive mathematics where excluded middle is false. But there are constructive settings where excluded middle holds, e.g. Boolean topoi, but you have to prove excluded middle is validated.

So we can't claim constructive mathematicians reject excluded middle, since they reject the rejection of excluded middle. I admit this will be confusing for people used to classical logic at first, even those for whom English is their native language.

> The way I understand it is that if you have the law of excluded middle you cannot discard 'non-constructive' proofs as invalid since they follow straight from the axioms.

This is accurate, my above point is just a pedantic one about semantics.

stacksemantics··on Formalising Mathematics: An Introduction
There is only one kind of proof by contradiction. Assume not P, derive a contradiction which implies not not P, then conclude (via excluded middle) P.

If you assume P, derive a contradiction, then conclude not P, that is a direct proof of negation not a proof by contradiction.

stacksemantics··on Formalising Mathematics: An Introduction
Constructive mathematics does not affirm excluded middle. That's distinct from rejecting it.