Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

Constructive mathematics rejects the law of excluded middle.

In a non-constructive mathematics it is true that 'either A or not A is true' and that allows you to prove existence of objects with certain properties by disproving their non-existence (if it cannot not-exist then it has to exist, by the law of excluded middle). Constructive mathematics, on the other hand, says that that's not enough and to prove that there exist objects with some properties you have to prove their existence.



Constructive mathematics does not affirm excluded middle. That's distinct from rejecting it.


What do you mean? (sorry, english is not my first 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.


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.


“Not affirm” means they don’t take it as an axiom (“we don’t take this to be obviously true”)

“reject” would mean that if, given their set of axioms, it could be proven, they would try and tweak their axioms in order to make it unprovable or provably false in their system (“we think this cannot and should not be true”)

So, “not reject” means they would happily use it in their proofs, if it could be proven from their set of axioms (“interesting. That gives us a powerful tool to do proofs”)


Thanks




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: