[FOM] About linear logic (was Re:Mismatch)

[Alessio Guglielmi]

Hello,

this is a reply to Harvey Friedman's posting on FOM (see 
<http://www.cs.nyu.edu/pipermail/fom/2003-June/006833.html>), where 
he answers my `mismatch' email and raises some important questions, 
especially about linear logic. I'm sending this also to the Proof 
Theory list because I believe that there are people there, not on 
FOM, who disagree on what I'm saying here, or wish to integrate it.

Let me first make clear my humble opinion on linear logic. Linear 
logic, for me, is simply a mathematical object; in particular, it is 
an interesting proof theoretical object. I don't believe that linear 
logic has a direct relevance for the foundations of mathematics, and, 
at least as it stands now, it is not foundational for computer 
science. So, for me linear logic is different than intuitionistic 
logic, or relevance logic: these logics come with a philosophy, they 
aim at being foundational. Linear logic is just an algebraic theory.

On the other hand, I believe that linear logic might have a 
beneficial indirect effect on the foundations of mathematics, and 
could be further developed to become a foundation for computer 
science.

LINEAR LOGIC AND MATHEMATICS

I'd say that proof theory is still seriously underdeveloped, as 
witnessed by the fact that we are still not able to answer the 
question: `When are two different mathematical proofs essentially the 
same?' (it's not even clear how to define being `essentially the 
same'); and supposing we know that: `Given two proofs, can we decide 
that they are the same?'.

One of the reasons for our inability is that proof theory is 
currently suffocated by bureaucracy, meaning that proofs are 
cumbersome objects, which leave us very little freedom of 
manipulation and analysis.

Linear logic brings into the picture at least two important 
novelties: a more refined notion of implication, which leads to a 
more refined analysis of proofs, and proof nets, which is a new 
syntax with much less bureaucracy than the sequent calculus. The fact 
that linear logic deals with `resources' is totally irrelevant in my 
opinion.

So, my hope is that linear logic can help proof theory develop in a 
way beneficial to classical logic, and so to the foundations of 
mathematics. In other words, having to deal with a laboratory-monster 
logic is important for proof theory, in order to strengthen the 
methods for the normal patient.

This picture is confirmed by recent work in proof theory. What we do 
with the Calculus of Structures is an example 
<http://www.ki.inf.tu-dresden.de/~guglielm/Research>: properties 
first conjectured and proved for linear logic then turned out to be 
true (and elegant) also for classical logic. Another example is 
research by Fuehrmann and Pym, recently advertised on the PT list 
<http://www.cs.bath.ac.uk/~pym/oecm.pdf>, where they attack the 
problem of proof equivalence by taking inspiration from linear 
logic's research.

In my everyday work, when I have an idea that could be true for 
classical logic, I immediately test it also on linear logic, and the 
perspective that linear logic offers is almost infallibly very 
interesting.

LINEAR LOGIC AND COMPUTER SCIENCE

What could be foundational for computer science? My (very naif!) 
philosophy on the subject is the following.

Mathematics has a foundational language: it's the language that 
mathematicians speak and write. It's been developed in the millennia 
as a specialisation of the human language and benefits from devices 
like books and computers for the permanent storage of information. It 
relies on the fact that when one says or proves something, this will 
never be forgotten, because the information tends to stay in the 
brain, and certainly stays in books. In the last century this 
language has been studied by logic and we're rather happy. Not 
everything is known about this language (see above) but we don't see 
a need for changing the language, because we, human beings, didn't 
change.

Human communication is slow, mono-channel, and it relies on a huge 
database of shared information. A distributed computer is quite the 
opposite: fast multi-channel communication and very little shared 
information. After a message is sent, it's also forgotten. So, one 
could say, and I would agree, that the logic of the computer must be 
different, whatever that is.

Linear logic can be viewed as an attempt at capturing message passing 
(or, if you wish, `resources'). Only time will tell whether this will 
be successful and useful. I'm a bit skeptical, because I don't see 
much hard evidence of this, and also because it looks to me a bit 
naif to start from the logic side of the thing.

I'd say that a more promising approach would be first to agree on the 
language, or class of languages, one wants to model (I'd bet on 
process algebras a la Milner). Then a good idea seems to be trying to 
match process algebras and logics *derived and inspired* from linear 
logic, but I see too many problems in using linear logic as is. Just 
to mention one, there is no clear way of expressing sequential 
composition of processes in linear logic. Now, if there is a 
fundamental notion in algorithms and recipes, this is: `first beat 
the egg, then pour the milk', ...

In conclusion, I'd stress my opinion that in no case linear logic is 
to be considered on the same level of classical logic. It's a `logic' 
in the sense that it's the study of a language, but this doesn't 
mean, for example, that we have to ask for it an intuitive, 
philosophically convincing semantics as we do for classical logic. As 
for most mathematical *objects*, the models of classical logics are 
weird, exotic structures.

* * * * *

Having said all this, I'll briefly answer those of your questions and 
remarks I feel confident with:

1   There are complete semantics for linear logic and fragments of 
it, including model theoretic semantics. One such semantics is `phase 
semantics', which you can find in [1, 2]. The literature is rather 
exterminate, I'd leave it to others more knowledgeable than me 
pointing you in the right direction. Let me only mention that the 
prevailing interest in semantics for linear logic is more in 
(denotational) semantics of proofs, not of formulae. In this sense, 
model theory is not where most of the research goes.

2   For understanding my posting, it is sufficient to know the syntax 
of linear logic in the sequent calculus, which again you can find in 
[1], but you might find [2] more concise. This is very elementary: 
you just have to read a sequent system. If you want to go deeper, I'd 
suggest you try and prove cut elimination for the system. Another 
good, quick introduction to some ideas of linear logic is in [3]. In 
any case, linear logic in my `mismatch' posting was only supposed to 
be an example illustrating a more general point about proof theory.

3   I'd expect FOM subscribers to consider linear logic an important 
mathematical idea, not necessarily a foundational one, and not to 
expect semantics for it in the same spirit of semantics for classical 
logic, because there isn't such a need.

-Alessio


[1] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 
50:1-102, 1987.

[2] The Linear Logic Pages: <http://iml.univ-mrs.fr/~lafont/linear/>

[3] Jean-Yves Girard, Yves Lafont and Paul Taylor. Proofs and types. 
Cambridge University Press, 1989.