In a constructive system, it’s often possible to refute a universal proposition without exhibiting a counterexample, by proving that the proposition implies falsehood.

The constructivist will still object that you can’t, from that, conclude that “…therefore a counterexample must exist,” without actually providing a counterexample. But the general principle I was describing still applies - a proof often gives you insight that an example by itself doesn’t.

▲

mb7733 3 hours ago | parent | next [-]

To roughly repeat myself from a sibling comment: I may have been unclear. I didn't claim that the only way to disprove something in a constructive system is to produce a counterexample.

The part that I was referring to was the last statement from the OP: that "a proof of existence of a counterexample necessarily provides more insight than a counterexample". I can't imagine a constructivist would agree with that in general.

	▲	antonvs an hour ago \| parent [-]
		I'm the OP. In the cases where a proposition can be refuted by a proof that doesn't involve counterexamples, by its nature that proof will tell you something about the reason that the proposition is false. Whereas a counterexample, on its own, proves the proposition false but doesn't necessarily tell you anything else. The real difference in the constructive case is that there are fewer classes of proposition for which a proof without witnesses is possible. (Edit: side note, I didn't explicitly say "necessarily" in my original comment. I suppose there could be exceptions, although I'm struggling to think of an example. Constructively speaking, the ball is in your court!)

▲

Jweb_Guru 3 hours ago | parent | prev [-]

I think the constructive position is basically that people's entire issue with lack of excluded middle being absent is just that people like being able to say "P" instead of "~~P" because it sounds better, considering you can prove ~~P for all the classical propositions that use excluded middle.

	▲	antonvs 26 minutes ago \| parent [-]
		> people like being able to say "P" instead of "~~P" because it sounds better It depends on how old an intuitionist/constructionist you are. Back in the day, they were interested in logic as a description of correct reasoning. Brouwer saw LEM as a mistake in the foundations. These days, the influence of formalization, including proof theory and model theory, has removed a lot of the teeth from that debate and made it possible to summarize as you have. I studied this in the early 1980s, and my professor was definitely in the "this is a black and white issue" camp, although he came down on the classical side. (Side note, I was once a back seat passenger in a car with my prof and Quine in the front seat, who was visiting at the time. Quine was famously committed to the idea that first order logic is the only kind worthy of the name.)