A classically trained mathematician is more likely to be familiar (at least anecdotally) with an area of mathematical physics such as deformation quantization than with intuitionistic logic. It is helpful in any sense (philosophical or mathematical) to think of intuitionistic logic as a quantization of classical logic? Has anyone explored such an approach? Note that the idea itself of comparing the passage from classical to intuitionistic logic to denying commutativity is not new; see Richman's "Interview with a constructive mathematician" at http://www.ams.org/mathscinetgetitem?mr=1400617 . ͏ ͏ ͏

3$\begingroup$ I suspect that the thinking behind this question is that it is sometimes said that classical mathematicians ought to be willing to acknowledge intuitionistic mathematics in the same way that they do noncommutative group or ring theory. I agree with this professionally, but I do not think that there is a significant mathematical analogy to be made. Howover, I would certainly like to hear from someone who does know about quantum groups, for example, maybe with a substantive positive answer to this question. $\endgroup$ – Paul Taylor Apr 23 '13 at 15:21

$\begingroup$ I note that in your "Practical Foundations" you use a similar analogy: "In classical logic, as in classical physics, particles enact a logical script, but neither they nor the stage on which they perform are permanently altered by the experience. In the modern view, matter and its activity are created together, and are interchangeable (the observer also affects the experiment by the strength of the metalogic)." $\endgroup$ – Mikhail Katz Apr 23 '13 at 15:25

$\begingroup$ +1 for the link to this fascinating article. $\endgroup$ – Joël Apr 23 '13 at 15:55

2$\begingroup$ That piece of prose is in the Introduction to the book, which I wrote in a hurry because there had to be an Introduction, so don't pay much attention to it. If there is ever a second edition then the Introduction will go: I am still quite pleased with the way I started off in Section 1.1. $\endgroup$ – Paul Taylor Apr 23 '13 at 18:58

1$\begingroup$ @Paul: There is an approach by Heunen, Landsman and Spitters (arxiv.org/abs/0709.4364) where they combine quantum mechanics, noncommutative geometry, and toposes, where one of the main point of toposes is that the internal logic is intuitionistic. I'm not wellversed enough in topos theory to really make sense of that article though. $\endgroup$ – Jan Jitse Venselaar Apr 23 '13 at 20:41
No, intuitionistic logic is not the quantization of classical logic in a useful sense. (It is obtained from classical logic by removing artifical constraints, which is a step rather different from quantization.)
But there is a way to see the point of intuitionistic logic from a perspective motivated from quantization.
To see this, the main point to notice is that intuitionistic logic is the logic that allows to carry out reasoning in ambient toposes other than that of plain sets, hence in geometric contexts. That's the whole point of it.
And this is something that all of quantization theory starts with (usually secretly, of course): the "classical" (really: prequantum) data that quantization is applied to lives in generalized differential geometry where path spaces and spaces of differential forms etc. exist as smooth spaces. And this means that all of quantization starts (usually secretly, of course) in an ambient intuitionistic context. Of course there are plenty of ways to fight noticing this, which is why it's still an exotic perspective sociologically, even though it is the natural perspective fundamentally. The lecture notes geometry of physics try to give the natural perspective.
In
 Urs Schreiber, Mike Shulman, Quantum gauge field theory in Cohesive homotopy type theory
an intuitionistic axiomatization of (pre)quantum physics is laid out, and in
 Domenico Fiorenza, Chris Rogers, Urs Schreiber, Higher geometric prequantum theory
it is is discussed how Heisenberg groups, Poisson Lie algebras, Heisenberg Lie algebras, (pre)quantum operators etc. drop out naturally from these intuitionistic axioms.
Indeed, once axiomatized in intuitionistic logic this way, all these concept become much simpler than they are usually thought of. They are really sitting just a tad above the very foundations (univalent foundations, that is). See the above articles for why and how.
[edit Jan 2014:
Meanwhile with Joost Nuiten we have further developed the formalization of quantization in intuitionistic linear logic, details are here
 Urs Schreiber, Homotopytype semantics for quantization
Indeed, if anything in logic resembles quantization, then it is the step from intuitionistic nonlinear to intuitionistic linear logic, this is discussed a bit more on the $n$Lab at quantum logic . ]

$\begingroup$ @Urs: thanks for elaboration. However, Heyting algebras are not a mere analogy (or nonanalogy) here. There is a connection to topos theory, which I could not articulate, not being conversant in the theory. I found useful information on this under the following link (to a project which you coauthored): ncatlab.org/nlab/show/Heyting+algebra#to_toposes_35 $\endgroup$ – Margaret Friedland Apr 24 '13 at 19:43

$\begingroup$ @Margaret, right, so Heyting algebras are to toposes as logic is to type theory (ncatlab.org/nlab/show/type%20theory): the latter includes the former. So what I said above involves not just intuitionistic logic, but also intuitionistic type theory (ncatlab.org/nlab/show/intuitionistic%20type%20theory). But that's only natural. $\endgroup$ – Urs Schreiber Apr 24 '13 at 19:58
MathOverflow is a valuable resource because it is interdisciplinary. Some of the people who have written about this question come from a traditional pure mathematical background where classical logic is the norm, whilst others are based in computer science departments and generally use intuitionistic logic(s). Something that even those of us in the latter category perhaps do not credit enough is that some quite substantial "heterodox" mathematics has been done in the past thirty years. This means, for example, that Dan Pipponi's answer presupposes some quite sophisticated ideas.
I suspect that the thinking behind this question is that it is sometimes said that classical mathematicians ought to be willing to acknowledge intuitionistic mathematics in the same way that they do noncommutative group or ring theory. I agree with this professionally, but I do not think that there is a significant mathematical analogy to be made.
If we are looking for analogies in ring theory to the classical/intuitionistic distinction, I think a better one would be the passage from $\mathbb Z$ to (commutative) integral domains in which ideals need not be principal. The development needs to be rewritten, but for the most part this is a matter of "cleaning things up" rather than doing a completely different and vastly more difficult thing like noncommutative ring theory. Unfortunately, rather a lot of the literature is made "dirty" with Excluded Middle, so there is a Herculean task to clean it up.
Treating logic in terms of (Boolean or Heyting) algebra is in most circumstances misleading. At primary school we evaluated arithmetic expressions from the inside out, but then we learned to manipulate ones with indeterminate values. Similarly, logic is not about things that "are either true or false" but which instead may perhaps be deducible from one another. Here I am simply making an observation about what mathematicians actually do, even classical ones.
The deduction operation that is at issue is Excluded Middle.
Essentially, Excluded Middle is like the fear of water. If your parents take you swimming as a baby, maybe before you can walk, then you do not develop the fear of water and learn to swim entirely naturally.
Similarly, if your teachers do not constantly indoctrinate you by beginning every proof in their lectures with "suppose not" then you will naturally grow up to be a constructive mathematician. It is only difficult because you have been told to think it is.
It is common to see arguments that use contradiction quite gratuitously. They are much more complicated because, instead of proving $C\Rightarrow D\Rightarrow E$, they prove $\lnot E\Rightarrow\lnot D\Rightarrow\lnot C$, so the argument is backtofront. When some parts of a proof that is naturally $$ A\Rightarrow B\Rightarrow C\Rightarrow D\Rightarrow E\Rightarrow F\Rightarrow G$$ are written forwards and others backwards, it turns into spaghetti: $$ A\Rightarrow B\Rightarrow C,\qquad \lnot E\Rightarrow\lnot D\Rightarrow\lnot C\qquad E\Rightarrow F\Rightarrow G. $$
In fact, as Dan has said, there is a lot of work in theoretical computer science based on the idea that the double negation rule is like a "computational effect" (such as exceptions and gotos) in programming. Unless used vary skillfully, such effects make programs next to impossible to understand.
On the other hand, there is considerable skill (that classical mathematicians refuse to acknowledge) in pulling a classical proof apart, teasing out its underlying concepts and creating a new constructive proof.
I would, for example, strongly recommend Constructive Analysis by Errett Bishop and Douglas Bridges, which gets on with proving the theorems without dwelling on the counterexamples.
The reason why some of us regard intuitionistic logic as fundamental and classical logic as an aberration lies in the following analogy (often called an "isomorphism") that was made by Haskell Curry in the 1930s and spelt out by William Howard in the 1960s. This analogy nowadays probably forms the basis of the masters' logic course in any computer science department.
A proof of the conjunction $P\land Q$ is a pair $(p,q)$, where $p$ is a proof of $P$ and $q$ is a proof of $Q$.
A proof of the implication $P\Rightarrow Q$ is a function $f$, where $f(p)$ is a proof of $Q$ whenever $p$ is a proof of $P$.
A proof of the univeral quantification $\forall x:X.P(x)$ is a function $f$, where $f(a)$ is a proof of $P(a)$ whenever $a$ is an element of $X$.
Whilst this might perhaps be seen as begging the question, it is difficult to see how one treat the other two connectives otherwise than:
A proof of the disjunction $P\lor Q$ is a pair $(i,r)$, where either $i=0$ and $r$ is a proof of $P$ or $i=1$ and $r$ is a proof of $Q$.
A proof of the existential quantification $\exists x:X.P(x)$ is pair $(a,p)$, where $a$ is an element of $X$ and $p$ is a proof of $P(a)$.
The point here is that there is no obvious way of translating excluded middle.
I say "obvious" because the work to which Dan refers seeks to do exactly that.
However, it is important to stress that those who are working on this kind of thing have not "seen the error of their ways" and returned to the "true faith" of classical logic, but are doing something that is way more sophisticated.
Returning to the original question, I am very skeptical. But the reason for this is not a lack of faith in intuitionistic logic or to disparage the work that people are doing in quantum mechanics. It is because those who are doing work like this probably use intuitionistic logic as a matter of course and would never consider naive classical logic as an alternative.

1

3$\begingroup$ It was a reference to the discussion on another question in which someone claimed authority on the grounds of having won a gold medal in the International Mathematical Olympiad. My point is that the IMO is about problems that are technically difficult but depend only on school maths and therefore no conceptual or philosophical consideration. $\endgroup$ – Paul Taylor Apr 23 '13 at 15:03

6$\begingroup$ As a classically trained mathematician, I like a good counterexample now and then. But as an occasional cook, I can attest it is more complicated to remove the salt that was added during cooking :) – Margaret Friedland 0 secs ago $\endgroup$ – Margaret Friedland Apr 23 '13 at 17:56

2$\begingroup$ I am glad to hear that Asaf avoids arguments by contradiction wherever possible, even in a classical setting. That is part of the hygiene of writing clear proofs. Unfortunately, many mathematicians routinely start an argument by saying "suppose not", as in "are you calling me a liar?". $\endgroup$ – Paul Taylor Apr 23 '13 at 18:53

2$\begingroup$ Margaret, before I rewrote my answer it occurred to me that you were its intended audience, so I tried unsuccessfully to find an email address for you so that I could discuss it with you. I was trying to explain that I use intuitionistic logic on a daytoday basis where you use classical, just as I use pounds where you use dollars. I was also trying to explain the things that computer science students learn and which are needed as background for Dan's answer. However, it seems that this has earned me downvotes. $\endgroup$ – Paul Taylor Apr 25 '13 at 14:53
Looking at this from a computational perspective, a common structure here is the monad, or something like it.
In intuitionistic logic we can prove
$a\rightarrow\neg\neg a$ and $\neg\neg(\neg\neg a)\rightarrow\neg\neg a$.
Similarly if $S$ is some set then we have natural maps $S\rightarrow span(S)$ and $span(span(S))\rightarrow span(S)$ where $span(S)$ is the vector space of formal linear combinations of elements of $S$.
Both of these are closely related to a monad or monadlike structure [1], [2]. The vector space example is relevant because quantum mechanics is a lot like classical mechanics where (some) classical states become labels for basis vectors in a larger state space given by quantum mechanics. This leads to a "quantum" monad [4].
When studying the semantics of computer programs, monads are frequently used to model "effects". There is a common heuristic to "deform" code written in a pure functional language so as to incorporate monadic effects. For example if we implement a data structure to represent groups and then "deform" it in this way we end up with a quantum group data structure [3], [5].
As mentioned by Paul Taylor, the fact that double negation gives rise to a monad is closely related to the notion of a continuations whch (among other things) gives a way to implement "effects" like branching. Glivenko's theorem means we can embed classical logic into intuitionistic logic using $\neg\neg$ and that, in turn, gives a way to interpret classical propositions computationally in terms of continuations.
The common structure here means that code written to specify and simulate quantum computers can have quite a bit of surprising commonality with code making use of continuations.
Note that this is going the opposite direction to that proposed in the question. Classical logic becomes a quantised version of intuitionistic logic.
[1] http://www.cs.nott.ac.uk/~txa/publ/Relative_Monads.pdf
[2] https://lists.chalmers.se/pipermail/agda/2009/001347.html
[3] http://blog.sigfpe.com/2008/08/hopfalgebragroupmonad.html
[4] http://www.cs.nott.ac.uk/~txa/talks/qnet06.pdf
[5] http://sbseminar.wordpress.com/2007/10/07/grouphopfalgebra/
A common relationship between Boolean algebras and Heyting algebras that holds a similar position as quantisation does between commutative and noncommutative geometry is known as a Galois Connection. This provides a way to reinterpret the result of classical logic in constructivist terms and vice versa, though the relationship is fairly blunt. It is also a standard relationship between syntax and semantics and is one means of understanding the BHK semantics.
This relationship is also what is used in turning ontological theories of science into operationalist ones. In fact, this has been done in the monoidal categories where quantisation occurs and works by people like Bob Coecke have explored the constructivist side of quantum mechanics, so you get the full circle back to what you consider an easytounderstand language if you follow this approach.
I also subscribe to Paul Taylor's comments about the primacy of constructivist thought. In most of the natural formulations, constructivism has less prerequisites than classical logic and reasons about things that are intuitively comprehensible because it doesn't make certain infinitary claims. Topoi come before Set, for instance, in intensional axiomatics.

$\begingroup$ Very interesting. I looked at the wiki article on "Galois connection" (incidentally, you could fix the link). Is this notion related to "equivalence of categories"? What would be a concrete example to illustrate the power of this notion as a means of clarifying the theory? $\endgroup$ – Mikhail Katz Apr 23 '13 at 17:56

$\begingroup$ As a piece of basic category theory, a Galois connection is an adjunction between one preorder (qua category) and the opposite of another; equivalences of categories are a special case of this. However, that is getting us away from the main issues of this page. $\endgroup$ – Paul Taylor Apr 23 '13 at 18:47

1$\begingroup$ I am not too familiar with this material and am curious to find out more. Can you summarize why one might think of a Galois connection more in terms of intuitionistic logic as a quantisation of classical logic than vice versa, for example? The wiki page is written in such general terms that it is hard to tell how something like this could be applied. $\endgroup$ – Mikhail Katz Apr 24 '13 at 12:19
If "quantization" is understood as "the procedure of constraining something from a relatively large or continuous set of values (such as the real numbers) to a relatively small discrete set (such as the integers" (like in Wikipedia), then I think it happens at the level of semantics. Classical propositional logic is modeled by Boolean algebras, while intuitionistic logic uses Heyting algebras. A propositional formula is true in intuitionist sense if and only if, for every valuation into any Heyting algebra, its value is the top element of that algebra. Boolean algebras are these Heyting algebras which satisfy the excluded middle, so an intuitionistically true propositional formula is classically true, but not necessarily the other way round.
I am not a logician, so my understanding might be flawed. Corrections and elaborations are welcome.
Edit: I am also not sure when Heyting algebras started to be systematically used as models for intuitionistic logic. And I think it was Tarski who observed that a collection of open sets of an arbitrary topological space form a (what is now known as) Heyting algebra.

1$\begingroup$ Here is a relevant quote from MacTutor: "When the Dutch Mathematical Association announced a prize question in 1927 they gave Heyting an ideal topic on which to compete. They asked for a formalisation of Brouwer's intuitionist theories and Heyting's outstanding essay was awarded the prize in 1928. This essay was then polished and expanded by Heyting and published in 1930." See wwwgap.dcs.stand.ac.uk/~history/Biographies/Heyting.html $\endgroup$ – Mikhail Katz Apr 23 '13 at 15:04

3$\begingroup$ This would give the classical logic as "quantization" of the intuitionistic one. $\endgroup$ – Margaret Friedland Apr 23 '13 at 15:04

$\begingroup$ @Margaret, yes, and even apart from this nonanalogy it should be made clear that the answer to the original question is definitely NO. $\endgroup$ – Urs Schreiber Apr 24 '13 at 17:09

$\begingroup$ @katz: I removed the reference to Heyting's 1941 paper, since it deals with intuitionistic aspects of field theory and does not introduce (what we now know as) Heyting algebras. Such algebras do not appear in his 1930 paper either; it is just propositional intuitionistic logic, without semantics. $\endgroup$ – Margaret Friedland Apr 24 '13 at 20:14

2$\begingroup$ I really object to this definition of "quantization". Quantization in physics is not about going from something continuous to something discrete, it is about going from functions on a set to operators on a Hilbert space (which may or may not have a discrete spectrum). $\endgroup$ – Nik Weaver Apr 24 '13 at 22:55
First, let me acknowledge Nik Weaver's objection. However, there is a notion of quantization in error correction coding. This notion might be compared with numerical methods that establish a policy by which some rational number is fixed to represent the real number of a given calculation. That is, an admissible value is accepted in relation to some actual value. So, Margaret Friedland's notion will be accepted for this response.
The initial objections to classical logic by Brouwer and others had to do with the definiteness of working with finite systems that differed from infinite systems. So, the sense of Margaret Friedland's notion would not seem to be the direct comparison to be made. And, in that same context, the original posted question seems badly construed.
Insightfully, however, Ms. Friedland thought the issue might lie with semantics.
The following remarks are from personal unpublished researches. As a philosophical matter, I reject logicism. The focus of my investigations had been the sign of equality and identity.
When Leibniz introduced the principle of identity of indiscernibles in "Discourse on Metaphysics", he did so by invoking geometric intuitions,
"What St. Thomas affirms on this point about angels or intelligences ('that here every individual is a lowest species') is true of all substances, provided one takes the specific difference in the way that geometers take it with regard to their figures."
Leibniz
My personal view on this is that numerical identity relies on geometric  or, more precisely, topological  notions. So, I interpret Leibniz' remarks along the line of Cantor's intersection theorem for nonempty, nested closed sets of vanishing diameter.
The semantic sense of Leibniz' remarks are to be found in another quote from one of his papers on logic (the name of which escapes me at this moment). Although somewhat deprecated in mathematical logic, the paradigm singular term in classical logic is the notion of a name. This is what Leibniz says about names,
"All existential propositions, though true, are not necessary, for they cannot be proved unless an infinity of propositions is used, i.e., unless an analysis is carried to infinity. That is, they can be proved only from the complete concept of an individual, which involves infinite existents. Thus, if I say, "Peter denies", understanding this of a certain time, then there is presupposed also the nature of that time, which also involves all that exists at that time. If I say "Peter denies" indefinitely, abstracting from time, then for this to be true  whether he has denied, or is about to deny  it must nevertheless be proved from the concept of Peter. But the concept of Peter is complete, and so involves infinite things; so one can never arrive at a perfect proof, but one always approaches it more and more, so that the difference is less than any given difference."
Leibniz
This, too, can be related directly to topological considerations in the guise of uniformities and uniform spaces.
Semantically, the identity relation is represented by the diagram or diagonal of the Cartesian product of a model domain. Under the received view, logical identity is not given by a metric interpretation. It is in the metrization lemma found in Kelley's "General Topology" wherein a system of relations containing the diagonal (say, a uniformity) and meeting certain other conditions generate a pseudometric. In other words, it is in the theory of uniformities where the original Leibnizian conception and modern semantical notions coincide.
It is for this reason that I am personally inclined to view the topological designations of open and closed sets (in particular, closed sets) in the context of the kind of "quantization" mentioned by Margaret Friedland.
For completeness with respect to the preceding remarks, let me observe that both Frege and Russell included descriptivist theories of naming in their logical analyses. Kleene reports that the eliminability of descriptions had been established in 1934 by Hilbert and Bernays. Robinson had been critical of Russellian description theory and discusses the use descriptions in relation to model diagonals in his paper "On constrained denotation".
Along similar lines, the logical interpretation of Leibniz' principle of identity of indiscernibles seems to have been established by the time of Kant. Kant criticizes Leibniz' application of that principle and asserts that identity associated with appearances is based on geometric notions. With respect to modern description theory, this notion of numerical identity in relation to geometry can be found in another critic of Russell  P. F. Strawson discusses the matter in his book, "Individuals".
Let me reiterate that these are only personal views, and, that they are nonstandard by every account.

$\begingroup$ I put the quotes into quote blocks to make them stand out from your text. $\endgroup$ – David Roberts May 15 '13 at 5:17