Intuitionistic vs Classical Logic

Isn't this the law of excluded middle (rejected by intuitionists and constructivists)?

By "constructively" do you mean in a constructivist logic like intuitionist logic? I'm too lazy to work it out right now, but I'd place my money on that statement not being valid in intuitionist logic.

You are probably thinking of intuitionistic logic versus classical logic. In the former, the law of excluded middle is not built in.

There is an entire movement within maths called 'intuitonist logic' that does not want to use ¬¬ϕ = ϕ.The point behind it is to only use 'constructive' proofs. Or rather, to avoid proofs that show a counter-example is impossible.

It's a reference to intuitionism, a constructivist approach to math and logic. Because the law of the excluded middle is disallowed in intuitionist proofs, you can't show what the parent comment was annoyed about.

I like seeing something along the line of constructive logic in the wild (i.e. not (not p) != p).

I've heard that propositional logic helps with this because you don't assume everything is either true or false, but rather look at what can be implied.You can then decide if you want the law of the excluded middle or not. I'm paraphrasing a talk I watched but would love to hear from someone knowledgeable on this subject...

Sure, if you restrict yourself to intuitionistic logic... which is odd (to use the most charitable description I can give of it).

You are confusing "excluded middle" (¬p⋁p) with "non-contradiction" (¬(p∧¬p)). The former is not valid in e.g. constructive logic, whereas the latter is a basic statement of consistency.

The article mentions law of excluded middle which doesn't hold in constructive logic so I wonder what exactly happens in the constructive setting.