[FOM] Girard's new program

[Alasdair Urquhart]

Many thanks to Alessio Gugliemi and Andre Scedrov
for their very clear and informative postings,
that go a long way to answering my original queries.

If I might summarize Alessio's last posting, it seems
to me that he argues in favour of linear logic as an 
interesting calculus which may have serious applications
in computer science and the analysis of algorithms.
The comparison with Kleene's calculus of regular
expressions comes to mind (in fact, there is even a kind
of formal analogy, since Kleene's calculus contains an
operation representing iteration).  The program of linear
logic has aroused considerable enthusiasm among mathematicians
and computer scientists in Europe, but not nearly as much
in North America.  This, however, is a sociological fact, 
from which I wouldn't draw any logical conclusions.

This view of linear logic as an interesting calculus somewhat
resembling ordinary logic, however, does not argue for
its acceptance as a logical language (I am recalling Jean van Heijenoort's
classic article on "Logic as calculus and logic as language").
If we are to accept linear logic as a good way to formalize 
mathematical proofs, then we would have to say things
like:

"If you assume "x+0 = x" 347 times, and .... then Fermat's Last Theorem
follows."

But mathematicians don't talk this way!  Of course, you could
always use the ! operator to avoid the problem, but then
it's not easy to see why you don't just adopt classical
logic (or intuitionistic logic) directly.

This brings me to Andre's posting, which answers my question 
in a different way, one that does defend Girard's new program
of ludics as having foundational significance (as Girard himself
argues very strongly).  Here the aim seems to be to find a deeper
layer of logical analysis behind the apparently arbitrary
("bureaucratic") structures of ordinary proof theory.
If I might draw a philosophical analogy, the program has a rough
kinship with Wittgenstein's view of language in the Tractatus
Logico-Philosophicus.  The view in that work is that ordinary 
language conceals a logical substructure of immense intricacy,
the "elementary logical particles" of ordinary discourse.  Wittgenstein's
aim is to discover the "essence" of language. 

If we think of linear logic as a representation of the logical
substructure of mathematics ("the logic behind logic" to employ
an early phrase of Girard), then it is not at all vulnerable
to the rather obvious objection that I made to its application
as a logic.  (My objection would be akin to somebody saying that when
we order a coffee in Starbucks, we don't say anything about
protons and electrons.)  

So far, I think it is fair to say that linear logic as a calculus
has been quite successful, but the larger foundational aims
have yet to be realized.  However, I haven't studied the
more recent literature that earlier posters referred me to,
so I'll stop here.

Alasdair