The constructivist animosity against the law of the excluded middle

[godelian]

Concluding existence from the absurdity of non-existence does not sound like a particularly legitimate argument. Even though my intuition says that rejecting such proof strategy has its merits, I wonder if there are good examples for why this may be so. In what circumstances will the law of the excluded middle lead us astray?

Any constructivist witnesses for constructivism itself?

[Iwannaplato]

Concluding existence from the absurdity of non-existence does not sound like a particularly legitimate argument. Even though my intuition says that rejecting such proof strategy has its merits, I wonder if there are good examples for why this may be so. In what circumstances will the law of the excluded middle lead us astray?

Any constructivist witnesses for constructivism itself?

Sometimes I'm contrructivist. (so the statement Iwannaplato is a constructivist violates the LEM).
Anyway that was a dense paragraph, that first one. Can we tease it out a bit?

Concluding existence from the absurdity of non-existence does not sound like a particularly legitimate argument.

Do you mean the argument that there must be something, rather than nothing, because there being only nothing is absurd? That never having been something makes no sense ontologically? Not merely that it isn't the case, but that it cannot be the case there is not something?

And how does the law of excluded middle come in?

That if we can show nothing is not possible then there must be something, since those are the only options?

And then are you interested in any counterexampls to the LEL, or just those that apply to ontology?

It seems to me the LEM depends on the utter accuracy of language. That our words fit reality perfectly, never ambiguously, and the semantic boundaries are perfect, the scope of every word and every nuance of every word, not only matches what is perfectly but even what might be.

[godelian]

Concluding existence from the absurdity of non-existence does not sound like a particularly legitimate argument. Even though my intuition says that rejecting such proof strategy has its merits, I wonder if there are good examples for why this may be so. In what circumstances will the law of the excluded middle lead us astray?

Any constructivist witnesses for constructivism itself?

Sometimes I'm contrructivist. (so the statement Iwannaplato is a constructivist violates the LEM).
Anyway that was a dense paragraph, that first one. Can we tease it out a bit?

Concluding existence from the absurdity of non-existence does not sound like a particularly legitimate argument.

Do you mean the argument that there must be something, rather than nothing, because there being only nothing is absurd? That never having been something makes no sense ontologically? Not merely that it isn't the case, but that it cannot be the case there is not something?

And how does the law of excluded middle come in?

That if we can show nothing is not possible then there must be something, since those are the only options?

And then are you interested in any counterexampls to the LEL, or just those that apply to ontology?

It seems to me the LEM depends on the utter accuracy of language. That our words fit reality perfectly, never ambiguously, and the semantic boundaries are perfect, the scope of every word and every nuance of every word, not only matches what is perfectly but even what might be.

I would want to see an example, i.e. a definitive witness, in which non-constructive reasoning clearly leads us astray:

https://en.wikipedia.org/wiki/Construct ... thematics)
In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove the existence of a mathematical object without "finding" that object explicitly, by assuming its non-existence and then deriving a contradiction from that assumption. Such a proof by contradiction might be called non-constructive, and a constructivist might reject it.

Non-constructive proofs are questionable. Fine. I intuitively agree with that. However, if I am to insist on constructivism, I want a practical example in which non-constructivism leads to an undesirable outcome.

I simply think that constructivism itself should be more constructivist.

[Skepdick]

Concluding existence from the absurdity of non-existence does not sound like a particularly legitimate argument.

That's not what the constructivists are doing. That's precisely what the classical logicians are doing.

Let X = ¬Existence
Assume X.
Derive contradiction.
Therefore ¬X (by LEM)
Substitute X for its value: ¬¬Existence
By double negation elimination: Existence


That's why proof by contradiction is NOT a valid proof methodology in constructive reasoning.

[godelian]

Concluding existence from the absurdity of non-existence does not sound like a particularly legitimate argument.

That's not what the constructivists are doing. That's precisely what the classical logicians are doing.

Let X = ¬Existence
Assume X.
Derive contradiction.
Therefore ¬X (by LEM)
Substitute X for its value: ¬¬Existence
By double negation elimination: Existence


That's why proof by contradiction is NOT a valid proof methodology in constructive reasoning.

Yes, but the question is : why?

I assume that there exists an example of a proof by contradiction that actually leads us astray.

What is a good example?

[Skepdick]

Yes, but the question is : why?

I assume that there exists an example of a proof by contradiction that actually leads us astray.

What is a good example?

Of course. Russel's paradox.

Does the set of all sets blah blah blah contain itself? Assume it doesn't. Contradiction. Therefore it does.
Of course, you could've just gone the other way. Assume it does. Contradiction. Therefore it doesn't.

If your premises are already self-contradictory that literally means you already assume P and not-P to both be true.
You can always start at P and get to not-P. Or you can always start at not-P and get to P.

Naturally. Because ALL deductive reasoning is truth-preserving. If P is true, and not-P is true then they are isomorphic.

And the classical logicians assume them to be isomorphic under negation. negating not-P gives you P.
Negating P gives you not-P.

[godelian]

Of course. Russel's paradox.

Does the set of all sets blah blah blah contain itself? Assume it doesn't. Contradiction. Therefore it does.
Of course, you could've just gone the other way. Assume it does. Contradiction. Therefore it doesn't.

If your premises are already self-contradictory that literally means you already assume P and not-P to both be true.
You can always start at P and get to not-P. Or you can always start at not-P and get to P.

In the following paper, the author actually proves Russell's paradox in a constructivist way:

https://www.ams.org/journals/bull/2017- ... 1556-4.pdf

First he exploits the subtle difference between the law of the excluded middle and the law of non-contradiction:

- excluded middle: For every proposition P , either P or not P.
- non-contradiction: There is no proposition P such that P and ¬P.

So, let's define R = {x ∈ V | x !∈ x}, i.e. Russell's set of all sets that do not contain themselves.

Next, he observes that:

(1) if R ∈ R, then by the definition of R also R !∈ R, which is absurd. This proves by negation: ¬(R ∈ R)
(2) if R !∈ R, then again by the definition of R also R ∈ R, which is absurd. This proves by negation: ¬(R !∈ R) which is equivalent to ¬¬(R ∈ R).

Hence, since the above proves both ¬(R ∈ R) and ¬¬(R ∈ R), then according to non-contradiction R cannot exist.

Next, the author writes:

We could read the above splitting of the proof into two observations as an application of excluded middle (either R ∈ R or R !∈ R), but we
do not have to!

Hence, we come to exactly the same conclusion about Russell's paradox, both in a constructive and in a non-constructive way. There is absolutely no difference in outcome.

I actually wanted an example in which the outcome would be different between the constructive and the non-constructive approach, with the non-constructive approach turning out to be seriously problematic.

[Skepdick]

In the following paper, the author actually proves Russell's paradox in a constructivist way.

No, he doesn't. He disproves the existence of the set R.

If the set R doesn't exist then the question "Is R a member of itself?" is incoherent/invalid.

The question is meaningless.

Hence, we come to exactly the same conclusion about Russell's paradox, both in a constructive and in a non-constructive way. There is absolutely no difference in outcome.

Nonsense. The difference is that you asked a question: is R a member of itself?

I wasted no time asking questions about sets which don't exist.

I actually wanted an example in which the outcome would be different between the constructive and the non-constructive approach, with the non-constructive approach turning out to be seriously problematic.

This is different. I am forbidding you from asking meaningless questions.

This leads to a peculiar universe of Mathematics where I demand that every question you ask is formalized in a query language.

https://en.wikipedia.org/wiki/Query_language

And the answers to your questions are constructive witnesses.

[godelian]

Nonsense. The difference is that you asked a question: is R a member of itself?
I wasted no time asking questions about sets which don't exist.

I literally copied the argument below from the author's paper. It is on page 483:

https://www.ams.org/journals/bull/2017- ... 1556-4.pdf
Observe that:
(1) if R ∈ R, then by the definition of R also R 1∈ R, which is absurd;
(2) if R !∈ R, then again by the definition of R also R ∈ R, which is absurd.

Above, the author does ask questions about a set R that does not exist -- as he concludes later on.

He insists that his argument is still constructivist because he does not use the excluded middle in his conclusion but rather non-contradiction.

[Skepdick]

Nonsense. The difference is that you asked a question: is R a member of itself?
I wasted no time asking questions about sets which don't exist.

I literally copied the argument below from the author's paper. It is on page 483:

https://www.ams.org/journals/bull/2017- ... 1556-4.pdf
Observe that:
(1) if R ∈ R, then by the definition of R also R 1∈ R, which is absurd;
(2) if R !∈ R, then again by the definition of R also R ∈ R, which is absurd.

Above, the author does ask questions about a set R that does not exist -- as he concludes later on.

He insists that his argument is still constructivist because he does not use the excluded middle in his conclusion but rather non-contradiction.

I don't think you understand what it is that you are observing.

The author starts with the claim "There is no set of all sets."
And then he proceeds to prove that claim.

Nowhere in your quote is the author asking the question "Is the set R a member of itself?

There is a difference between "What is the truth-value of R ∈ R?" and attempting to obtain an answer.
And testing ALL possible truth-values (in this case there is only two of them) and deriving an absurdity from both.

He is literally proving ¬∃R

[Skepdick]

Nonsense. The difference is that you asked a question: is R a member of itself?
I wasted no time asking questions about sets which don't exist.

I literally copied the argument below from the author's paper. It is on page 483:

https://www.ams.org/journals/bull/2017- ... 1556-4.pdf
Observe that:
(1) if R ∈ R, then by the definition of R also R 1∈ R, which is absurd;
(2) if R !∈ R, then again by the definition of R also R ∈ R, which is absurd.

Above, the author does ask questions about a set R that does not exist -- as he concludes later on.

He insists that his argument is still constructivist because he does not use the excluded middle in his conclusion but rather non-contradiction.

Let me try again. In simplest possible English.

Assume R.

By LEM it follows that either R ∈ R is true OR ¬(R ∈ R) is true.

This is in itself misleading, because (as it turns out) the correct statement is NEITHER R ∈ R is true NOR ¬(R ∈ R) is true.

So in this instance the application of LEM literally presents us with a false dichotomy.

Syntactically speaking this is perfectly coherent to computer scientists. We have the Either monad which brings us a step closer to natural language.

Either P is true or not-P is true. OK! Which one? Neither!

Thus negating LEM: ¬Either((R ∈ R) , ¬(R ∈ R)

[godelian]

Nonsense. The difference is that you asked a question: is R a member of itself?
I wasted no time asking questions about sets which don't exist.

I literally copied the argument below from the author's paper. It is on page 483:

https://www.ams.org/journals/bull/2017- ... 1556-4.pdf
Observe that:
(1) if R ∈ R, then by the definition of R also R 1∈ R, which is absurd;
(2) if R !∈ R, then again by the definition of R also R ∈ R, which is absurd.

Above, the author does ask questions about a set R that does not exist -- as he concludes later on.

He insists that his argument is still constructivist because he does not use the excluded middle in his conclusion but rather non-contradiction.

Let me try again. In simplest possible English.

Assume R.

By LEM it follows that either R ∈ R is true OR ¬(R ∈ R) is true.

This is in itself misleading, because (as it turns out) the correct statement is NEITHER R ∈ R is true NOR ¬(R ∈ R) is true.

So in this instance the application of LEM literally presents us with a false dichotomy.

Syntactically speaking this is perfectly coherent to computer scientists. We have the Either() monad. From the monadic/computational view the statement of LEM is simply the disjunct P ∨ ¬P. One of those is true.

OK! Which one?

This is perfectly consistent with the BHK interpretation.

https://en.wikipedia.org/wiki/Brouwer%E ... rpretation

He literally writes " if R ∈ R". This assumes R too, even though later on R turns out not to exist. So, just like with LEM, he assumes the existence of R first.

[Skepdick]

He literally writes " if R ∈ R". This assumes R too, even though later on R turns out not to exist. So, just like with LEM, he assumes the existence of R first.

He literally provides a counter-example to LEM.

The statement of LEM is: P ∨ ¬P. Either R contains itself or it doesn't.
He proves: ¬(P ∨ ¬P). Neither of those claims is true - a false dichotomy!

The true claim is: Neither (R ∈ R) NOR ¬(R ∈ R)

Thus demonstrating an instance where LEM does not hold.
That doesn't mean LEM never holds. But it does mean that LEM doesn't always hold. e.g it's not an axiom.

The animosity!

[godelian]

He literally writes " if R ∈ R". This assumes R too, even though later on R turns out not to exist. So, just like with LEM, he assumes the existence of R first.

He literally provides a counter-example to LEM.

The statement of LEM is: P ∨ ¬P. Either R contains itself or it doesn't.
He proves: ¬(P ∨ ¬P). Neither of those claims is true - a false dichotomy!

The true claim is: Neither (R ∈ R) NOR ¬(R ∈ R)

Thus demonstrating an instance where LEM does not hold.
That doesn't mean LEM never holds. But it does mean that LEM doesn't always hold. e.g it's not an axiom.

The animosity!

Agreed.

It is unfortunate that the author of the paper does not explicitly write that the purpose of his argument is to provide an instance in which LEM does not hold. What he writes instead, is this:

We could read the above splitting of the proof into two observations as an application of excluded middle (either R ∈ R or R !∈ R), but we do not have to!

In fact, his comment suggests that proof by LEM would work as well. It is clear that application of excluded middle would indeed be a false dichotomy. He even proves it. His paper is truly confusing!

[Skepdick]

It is unfortunate that the author of the paper does not explicitly write that the purpose of his argument is to provide an instance in which LEM does not hold.

Because it isn't. The purpose of the argument is to prove the theorem "There is no set of all sets".

That the negation of LEM in the proof happens to be true is a red herring because it serves to prove the theorem.

Unless you are a Classical logician who just lost an axiom.... In which case it makes sense as to why you'd lose track of the goal.

We could read the above splitting of the proof into two observations as an application of excluded middle (either R ∈ R or R !∈ R), but we do not have to!

In fact, his comment suggests that proof by LEM would work as well.

Not at all. What his comment suggests is that you could undertake the following line of reasoning:

You could indeed view (either R ∈ R or R !∈ R) as an exemplar of excluded middle.
Therefore the statement is true. Axiomatically. Proof terminates!

Which leaves you with "If R exists then either R is a member of itself or it isn't". OK. Nothing weird or alarming here.

But then the constructivists goes on to ask further: Which of the two disjuncts is true?
There is no witness to R ∈ R; or R !∈ R so the answer is "Neither"

So what it is that you have proven exactly?

If R exists then R is neither a member of itself nor it isn't.

That's absurd. Q.E.D