I think you'd be hard-pressed to find a classical mathematician who thinks that about intuitionist math - after all, every intuitionist theorem is also a classical theorem, and finding explicit constructions is useful in its own right. We might look at you a bit funny for making life harder on yourselves, same as the compass-and-ruler people looked at the compass-and-straightedge people (everybody looked at Mohr and Mascheroni funny
), but theorems are theorems.
Oh, you proof irrelevantists!
Every classical theorem is also an intuitionistic theorem. You can, and you sometimes
do, just add a hypothesis on the front that says you have the necessary instances of excluded middle (that you can decide some property), or that you have a suitable choice function.
But you can be less cheeky. Here are three classical theorems which are not intuitionistically valid:
1) ~~P → P (double negation elimination)
2) P ∨ ~P (excluded middle)
3) ~(∀x. ~P(x)) → (∃x. P(x)) (the classical infinite DeMorgan Law)
But, with slight adjustment, I can make three intuitionistically valid theorems:
1) ~~~P → ~P
2) ~~(P ∨ ~P)
3) ~(∀x. ~P(x)) → ~~(∃x. P(x))
From here, it's possible to show that you can take any classical theorem, shove a few double negations onto some of the subexpressions, and you get an equivalent classical theorem which is
also an intuitionistic theorem. This translation is called an "embedding", and it shows that intuitionistic logic is formally more expressive than classical: the semantics is necessarily richer, and any contradiction in classical logic also reliably kills intuitionistic logic, even though the intuitionistics have fewer axioms.
In this sense, I can look at a classical proof and see the theorem as an intuitionistic theorem with choice double negations wrapping some of the expressions, and I'll declare that it's the wrong theorem, and that the theorem I really want is the one without the double negations, which will be stronger.
There are even bigger differences though. If you're going to work constructively, you will sometimes need to choose different representations, so you really end up proving different theorems. And the demands of constructivists is that they need theorems that end up doing more work: they at least always have a computational interpretation. So you end up with definitions that tell you, for instance, that every function in constructive real analysis is continuous! That's pretty strong.
Ok, can you explain why you think we should be doing math intuitionistically over classically? Yes, the math comes out different, but why do you think one is better than the other? What does 'better' mean in this situation? Is this different than a compass-and-straightedge vs compass-and-ruler situation?
I plan for computer science to eat the entire world, and when we come to eat maths, we'll be making it intuitionistic, because it will force you guys to think in a way that always has a computational interpretation. I'm offering you a head-start before we begin the invasion in full.
Can you expand on this? From my readings of the classical Greek mathematicians, that is not the case in the arguments they explicitly used, even if modern-day intuitionist proofs can be found for those results.
I think I can explain this quite pithily. Take any proof in Euclid which ends QEF. These are the constructive proofs, where his goal is to obtain a geometric figure. You don't have to look hard. Proposition I in Book I is: "to draw an equilateral triangle."
Now imagine that proof beginning: "for suppose I cannot...."
It would obviously be a failure. And the reason is because the logic involved in producing a geometric construction doesn't admit double-negation elimination.
I stole this joke from a slightly different context and this excellent video:
[youtube]https://www.youtube.com/watch?v=zmhd8clDd_Y[/youtube]
Here's another example. Suppose Euclid had a proposition that read "To construct a triangle or to construct a circle." This would be really weird. How could he
not know which thing he's going to construct. All I need to do is read to the end of the proof, and see whether he ended up with a triangle or a circle, and delete as appropriate from the original proposition.
This is not how classical mathematics works, and classically, a bare-faced disjunction is a perfectly normal thing. Indeed, the law of excluded-middle is just such a bare-faced disjunction.
"Either I draw a triangle or I fail to draw a triangle."
"Okay. And how did it turn out?"
This is not to say that all of their logic is constructive, only the logic that's at work when they're talking in deeds: "I can do this", "I can produce that." But if they're just proving a property of a figure "it is the case that", then they
can use classical axioms. It's a mixed approach.
The most extreme forms of modern constructivism, by contrast, say that our logic should uniformally be about constructing things, even if it's just the construction of a
proof that a figure or other mathematical object has such-and-such a property. Proofs are to be treated as mathematical objects much as anything else.
There is at least one famous computer scientist I've read who works in an intuitionistic formal verifier, but is happy to use classical axioms if he's just proving a property about something, and doesn't really care about the proof as an actual object. This is the sort of mixed approach I take the ancient Greeks to have been using. It's not the way modern mathematics is done, and if you look at, say, Hilbert's modern adaptation of Euclid, you can't immediately tell if the theorems give you a reliable means of constructing a figure, or whether they just tell you that the figure "exists" (where, I don't know).
