[FOM] Girard's new program

[Alessio Guglielmi]

At 9:57 -0400 17.6.03, Alasdair Urquhart wrote:
>"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.
>
>[...]
>
>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.)

Yes. Counting how many times one uses "x+0 = x" is (rightly) 
considered irrelevant when communicating a mathematical result, so 
classical logic provides an adequate level of abstraction.

On the other hand, it might be necessary to count axioms if one wants 
to decide whether two (fully formalised) proofs of Fermat's last 
theorem are the same (open problem in proof theory). In this case the 
adequate level of abstraction could be a `substructural' logic.

I still don't believe that linear logic is such a logic, for 
technical reasons and also because it comes out of research that, as 
far as I understand, doesn't directly address most of the `problems' 
of classical logic (it would be an unlikely coincidence if it worked 
fully). However, linear logic does address *some* of the problems, 
for example non-confluence of normalisation, and also for this reason 
I believe that it has a lot to teach us in view of a better proof 
theory of classical logic.

-Alessio