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

Alessio Guglielmi Alessio.Guglielmi at inf.tu-dresden.de
Tue Jun 17 17:22:06 EDT 2003

```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
```