| |
| ▲ | Jweb_Guru 4 hours ago | parent | next [-] | | As a constructivist: we don't disagree :) We just distinguish between "don't disagree" and "agree." Constructive mathematics says it's fine if you want to claim that there's not no counterexample -- you just can't use that in a situation that demands an actual counterexample (like an algorithm that produces a result). This tends to guide people towards looking for results that don't require this kind of indirection, since they apply more broadly and in more kinds of logics -- orthodox constructive results are kind of a lowest common denominator of consistent truth and remain broadly compatible with most axioms, while nonconstructive results often fail in particular models. Which seems like a pretty sane stance to me, but maybe I'm too thoroughly indoctrinated to see how unreasonable it is :P (Note that this is about excluded middle. There ARE constructive logics with interpretations of excluded middle, e.g. some forms of classical linear logic, but they do not play as nicely with other logics. Constructivists often reject even weak forms of choice for largely the same reasons--there are some forms of choice that are constructively valid in some logics, but these results often fail to hold true in more conventional logics. And the same is true for a whole host of related notions that proof assistants like Rocq reject by default, propositional extensionality (which says that two proofs of the same proposition are equal) and function extensionality (which says functions are equal whenever their results are equal on all the arguments in their domain -- which might seem obviously acceptable until you realize that it's false in most programming languages!) being prominent but much less discussed examples. It's all about remaining broadly compatible with lots of different types of reasoning, not because people think the reasoning is invalid per se). | | |
| ▲ | mb7733 3 hours ago | parent [-] | | Maybe I was unclear. The part that I meant a constructivist would disagree was the subjective part: "This kind of proof (existence of a counterexample) provides more insight into the problem than simply finding a counterexample." I find it hard to believe that a constructivist would agree that across the board, proof of existence of X is more interesting than a construction of X. Isn't that the point!? | | |
| ▲ | Jweb_Guru 38 minutes ago | parent [-] | | A direct counterexample is more "informative" in a very literal sense (its truth value doesn't collapse). But the extra proof relevant content we can use here is not that large -- all it means in this case is that we can directly compute the object and its Jacobian, a well as two points evaluating to the same result. That's nice, but it's not that interesting by itself unless I can use the exact constructed form to prove other interesting stuff (and we can! Most of the followup results that immediately followed from the disrpoof come from being able to directly transform this object into counterexamples to other conjectures; if we didn't have constructive proofs of thoe counterexamples, we wouldn't have such procedures). But being more interesting than a completely uninformative counterexample still doesn't mean it's inherently interesting or enlightening. If anything I'd indeed argue constructive arguments are generally less mysterious and magical than nonconstructive proofs -- in some sense, the constructive proof pulls back the curtain and shows you where the trick is. |
|
| |
| ▲ | antonvs 3 hours ago | parent | prev [-] | | 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 28 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.) |
|
|
|
