[FOM] the essences of (nonclassical) logics (it was: mismatch)

[Alessio Guglielmi]

Hello,

just a couple of quick comments (I have to think a bit more before 
commenting on the interesting account of Basic Logic).

At 16:04 +0200 17.6.03, Giovanni Sambin wrote:
>At 4:23 +0200 15-06-2003, Alessio Guglielmi wrote:
>>The biggest advantage that deep inference brings into the picture 
>>is top-down symmetry for derivations.
>
>In Basic Logic, all inference rules come in symmetric pairs: for 
>example, &-formation is perfectly symmetric to v-formation.

They're left-right symmetric, not top-down symmetric (if I'm not 
mistaken). I don't know of any top-down symmetric formalism (except 
for the Calculus of Structures), and top-down symmetry is a key for 
flattening down the meta level into the object one, so to speak.

>At 14:22 +0200 16-06-2003, Alessio Guglielmi wrote:
>>The fact that linear logic deals with `resources' is totally 
>>irrelevant in my opinion.
>
>I do not agree, even perhaps against Girards' opinion. But it seems 
>that Guglielmi himself doesn't agree with himself, given his next 
>explanation in his section "Linear logic and computer science".

No contradiction. I was saying that resources are irrelevant when 
applying linear logic to the task of better understanding classical 
logic. In that case, what matters (to me) is the possibility of 
getting rid of bureaucracy, of having more combinatorial freedom in 
analysing proofs, etc.

In the different context of foundations for computer science, then of 
course resources are very much relevant.

Or perhaps are you implying that, at the bottom, the two realms of 
foundations of mathematics and computer science will coincide? This 
would be extremely surprising to me, I wouldn't bet on that, but 
perhaps it would be nice.

-Alessio