Looking back, I had constructivist inclinations long before I heard of constructivism. I was reading a Dutch textbook on Euclidean geometry, and came to the point where it were proving that the bisector of the top vertex of an isoceles triangle bisects the base. (At least, I think it was that theorem. It might have been another. With the decades, memory starts to lapse.) They first supposed that it intersected to the right of the midpoint and derived a contradiction; then they said similarly assuming it intersected to the left would lead to a contradiction; therefore the only remaining possibility was that it intersected at the midpoint, q.e.d.
This bothered me. It seemed to me that they talked all around the midpoint, but that they hadn't actualy managed to target the bisector at the midpoint. True, I couldn't think of an alternative, but still.... I talked to my father about it -- after all, it was his book I had borrowed -- and he explained that there were no more alternatives so it had to be that one. I had already understood that argument and felt uneasy about it, but I couldn't really say what it was that bothered me. It was as if I thought the proof had to *make* the bisector reach the midpoint rather than just talking about what might happen to happen in various conterfactual situations, but at the age of about ten or twelve, I realy couldn't express that. I decided to accept it provisionally in order to go on reading the book, which I had much fun doing.
(By the way, I looked this theorem up in Euclid a few days ago, and it turned out that Euclid had a constructive proof, except for failing to prove that the intersection point was actually in the triangle. Euclid often fails to prove this kind of obvious detail. This kind of thing wasn't actually put in the axioms for geometry until approx 1900. (TODO: look for reference about this.)).
When I tell this tale to my children, they tell me I must have been bored out of my skull to have been reading that kind of stuff for fun. Well, I didn't have such a plethora of competing media in the 50's as we have now. I didn't even have access to a television. Maybe I would have turned out very different if I had grown up in the 00's this century instead.
Later. I read Rosenbloom; my father had bought a copy. I learned all about Boolean algebra. I'm not sure whather it was there or in some other book at university that I first heard of alternative logics for mathematics, such as intuitionism that rejected proof by contradiction, and such as negation-free logics. Not much was said about these, just enough to make me curious.
It wasn't until after my masters' degree in math that I encountered a notice about a conference on Intuitionism and Proof Theory, in 1968. I could have gone there on the way to starting my Phd studies at Waterloo, but I didn't.
It was at the University of Waterloo, in Fisher's course on computability theory, that I encountered my next nudge to intuitionism. At the beginning of the course, to show how counterintuitive and tricky the results might be, he announced that there was an algorithm for telling whether there were seven consecutive sevens in the decimal expansion of pi. I thought, interesting, I'd like to see that, until I saw his proof. He presented two algorithms, "print true" and "print false" and pointed out that there either were of were not seven consecutive sevens, and so one of these was correct. Therefore there was an algorithm, but I still had no way to figure out whether there were seven consecutive sevens.
I realised that this was indeed a proof, according the all the rules of logic I had learned hitherto. But it wsa profoundly unsatisfying, and failed to convince me. Instead it led me to a deep suspicion of the very rules of logic. There seemed to be no way to say what I meant by existence of such an algorithm that couldn't be subverted by a proof of this form.
From then on I tried to make sure that, whenever possible, I would use constructive proofs, just as a matter of explicitness. But I really wasn't a constructivist yet. Maybe a potential constructivist. Maybe a closet constructivist.
It wasn't till years later, at the Mathematical Centre in Amsterdam, that I made my next step. Amsterdam was a hotbed of intuitionism, and I had many chances to discuss these issues with Lambert Meertens, who understood constructivism and took it seriously. He explained how it made sense, how the constructive interpretation of the logical primitives could be explained in an informal metatheory. And that metathory was also constructive. He showed me how you could recognise that "not false" isn't necessarily "true" even though there is no third logical value that is neither true nor false, Intuitionism isn't a three-valued logic.
One day I was pondering these matters while walking outside the Academische Boekhandel near het Spui, a well-known canal, and I realised that intuitionistic logic was easy to justify using intuitionistic metareasoning, just as classical logic was easy to justify using classical metareasoning. And although each could be used to prove various well-behavedness theorems about the other, such proofs seemed overly complicated and unnatural.
In one direction classical logic was just a superset of intuitionistic -- you just drop proof by contradiction and a whole lot of theorems, so evidently you still have consistency. But this didn't account for one controversial property of intuitionism -- that you could rely on any specific theorem having a proof, and that you could perform induction on the structure of that proof. This is used in proving, for example, the fan theorem. But because it was a caontroversial piece of constructive logic, one could kind of ignore it. Anyway, it's trivial to prove the fan theorem classically by a completely different method that doesn't use proof-induction.
In the other direction, it was possible to translate classical logic into constructive logic by the so-called double-negation interpretation. Statements were translated into statements, proofs into proofs, showing that classical logic was consistent relative to constructive. But it wasn't equivalent. There were lots and lots of contructive theorems that were never touched by this translation, so it almost seemed as if constructive logic was richer than classical, rather then being a cut-down version.
It took a while to realise that the real difference between classical and intuitionistic logic was the meaning of the logical operations. Intuitionistically, P or Q means that P is true or Q is true, and you can know which. Classically it just means that P is true or Q is true. There may be no way whatsoever of determining which.
But it turns out that che classical P or Q can more or less be expressed intuitionistically as not (not P and not Q). (This is an example of the double-negation interpretation in action) So the whole of classical logic is embedded in constructive, and you can distinguish the constructive P or Q from the translation (not (not P and not Q)) of the classical P or Q. These are not, in general, equivalent constructively, though they are equivalent classically. and foe some specific propositions P amd Q they may be equivalent constructively.
But in the translation, lots of classical theorems become convoluted and unintuitive.
It's decades later; I'm still a constructivist. But I understand classical logic. It's perfectly valid, even to me, when talking about things about which one can in principle determine truth of falsity. Most finite situations are of this kind; in particular most practical problems in computer programming. But when a classical mathematician goes on to talk about set theory with large cardinals and everything of that sort, I stand in awe of the results, much as one can stand in awe of a well-written fantasy novel.
-- hendrik