[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Kalani Thielen wrote : > But I'm not sure that I've got a straight story on this interpretation > of negation, quite. I think that it's suggesting that the size of the > set of continuations A->_|_ is |_|_|^|A|, or 0^|A|, which should be 0, > right? So there are 0 continuations -- they're impossible to > construct? Dear Kalani, The cardinal of A->empty is 0 only in the case |A| is non-empty. Otherwise, there is exactly 1 function. Therefore, by interpreting continuations as you do with sets, you do obtain an interpretation of classical logic, however with boolean truth values, and no structure of proofs. Continuations are not interpreted as arrows A->_|_ but as A->R for some chosen R. To witness the difference, let me take a proof of a Sigma^0_1 formula P (roughly speaking, a datatype containing no arrow type). Through the appropriate translation, this gives an intuitionistic proof of (P->R)->R with R not appearing in P. Now I may choose R=P and deduce an intuitionistic proof of P by applying to \x.x. >From the computational perspective, this corresponds to the fact that the reduction of a program containing control operators is only defined with respect to an initial context (here the empty context corresponding to \x.x). (Your question is relevant. There have been many arguments against the possibility of a model of classical logic that discriminates proofs, and they can be reduced to a generalization of your remark: there is at most one arrow A->_|_ in any model of intuitionistic logic that has an initial object (a bottom). However, this only indicates that in intuitionistic logic, negation and falsity are not obvious to define.) With this explanation in mind I wish to go back to the following message: Uday S Reddy wrote : > Coming to classical logic per se, I believe it is ill-fit for describing > computer programs or "processes" as you call them. First of all, classical > logic doesn't have any well-developed notion of time or dynamics, and it has > a nasty existential quantifier which assumes that all things exist once and > for all. In computer systems, new things come into being all the time, well > beyond the time of the original development or deployment. We know how to > write computer programs that deal with that. Classical logic doesn't. (LEJ > Brouwer made this criticism a long time ago in the context of mathematics. > There it might have been just a philosophical problem. But in Computer > Science, it is a *practical* problem.) > > <ranting about logicians elided> > > - Girard has formulated Linear Logic, which broadens our idea of what kind > of "things" a logic can talk about. David Pym and Peter O'Hearn invented > Bunched Implication Logic, extending Linear Logic with a beautiful > model-theoretic basis. These logics applied to imperative programming > (which go by the name of "Separation Logic") are revolutionizing the > development of technology for imperative programs. > > It is time to leave behind the classical logic. In fact, we should have > done it a long time ago. Yet Girard, which Uday mention, and others, have theorized how classical logic can be given a nice notion of "dynamics", all the while being as strong as intuitionistic logic in terms of constructiveness over certain formulae. In the example above, a classical proof of P yields an intuitionistic one. There are restrictions on the shape of P (a datatype containing no arrow), but not on the theorems used to prove P. So we may argue that the constructive contents were already in the classical proofs involved. Constructiveness is of course relaxed compared to intuitionistic logic. We may use a direct analogy with programming languages that are not purely functional, but allow effects. Functional types are opaque, because it makes no sense to retrieve the source code of a function created at runtime, in the presence of call/cc, storage, I/O, etc. This does not make such programming languages non-constructive or lacking dynamics: the thing still computes values. This makes a nice refinement (along with other examples Uday mentions) of the intuitionist's take on constructiveness, which showed, more than twenty years ago already, that a computational interpretation of logic may give up referential transparency in favor of interactivity with the context/opponent. (On a side note, I know "logicians of philosophical inclination" that are very well aware of such developments regarding the issue of constructiveness.) Sergei SOLOVIEV wrote : > > To add a bit in support to Uday's remark about "presumption of > supremacy" of classical logic: > > In fact, it is well known that classical logic can be embedded in > intuitionistic logic > using, for example, negative interpretation (classical "exists" becomes > \not\forall\not etc.) > From the point of view of provability, the interpretation of a > classical theorem is provable > intuitionistically if and only if the original theorem was provable > classically. > So, what is bad rationally, if instead of respectable "exists" we shall > say "it is > not true that for all x does not exist..."? It is clear, that it is a > "bad publicity", > a less "convincing" way to say - bad for "supremacy", but it has nothing > to do > with scientific rationality itself. (Constructive mathematics is just > more subtle > concerning existence.) > I do not exactly understand the claim here. However, the particular translation used in my example is already "more subtle concerning existence" than the one sketched by Serguei. Moreover, negative interpretation does not reduce the problem of understanding the constructive contents of classical logic to the one of understanding intuitionistic logic, because problems are converted modulo some translation which is not compositional on proofs. Thus the issue becomes to understand the translations as much as it is to understand intuitionistic logic. Serguei's remark is against "presumption of supremacy" of classical logic, but it should not be seen as the other extreme: redundancy of classical logic with respect to intuitionistic logic. (It seemed to me that so far, the discussion were indeed in favour of plurality in logic.) Best regards, -- Guillaume Munch-Maccagnoni <[email protected]>
