Intuitionistic logic as quantization of classical logic?

Question

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/mathscinet-getitem?mr=1400617 . ͏ ͏ ͏

Answer 1

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: pre-quantum) 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, Homotopy-type semantics for quantization

Indeed, if anything in logic resembles quantization, then it is the step from intuitionistic non-linear to intuitionistic linear logic, this is discussed a bit more on the $n$Lab at quantum logic . ]

Answer 2

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 non-commutative 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 non-commutative 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 back-to-front. 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.

Answer 3

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 monad-like 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/hopf-algebra-group-monad.html

[4] http://www.cs.nott.ac.uk/~txa/talks/qnet06.pdf

[5] http://sbseminar.wordpress.com/2007/10/07/group-hopf-algebra/

Answer 4

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 easy-to-understand 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.

Answer 5

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.

Answer 6

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 non-empty, 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 non-standard by every account.