[antonvs]

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]

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]

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]

I think maybe a better way of explaining it would be that an uninformative proof by definition needs to be based on proving that the set under consideration must be inhabited without ever defining an object in that set. This generally means you must show the set is inhabited by exploring some abstract properties of the set itself. A single counterexample, by contrast, by itself is a direct proof that the set is inhabited, so you don't necessarily learn any other interesting properties about the set. So it's not really about constructive vs. non-constructive, I think it's closer to e.g. the idea that point-free stuff tends to be more beautiful and meaningful than pointed stuff (which I think most mathematicians would agree with and which really has nothing to do with intuitionism per se).

In this case, I think part of the problem is that there was kind of no good reason to think the Jacobian conjecture was true in > 2 dimensions other than it being kind of hard to find counterexamples. So a really interesting disproof would be one that, e.g., was able to exhaustively classify the counterexamples, or showed why it seemed in practice to be hard to come up with functions violating the conjecture. AFAIK, this doesn't really accomplish either of those things, not even after you learn the procedure that constructed the function -- it kind of tells you why we should have expected to find a counterexample but not how rare such counterexamples are.

[Jweb_Guru]

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]

> 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.)

[Jweb_Guru]

Ah, I didn't realize this was a generational thing. I am definitely a "new" intuitionist, so that probably greatly influences my perspective. I suppose that before results like this, the setoid model, etc. were known constructivism was indeed a much more hardline position to have to take!