17 Jan 19:13 2007

### Units and second order in linear logic

```
Hello Frogs,

There are again some thoughts on the problem of the identity of proofs.
This time they concern second order linear logic.

It is well-known that the units 1, 0, one, bot of linear logic, can be
expressed by using second order quantifiers (and multiplicative
connectives).

We have:

0   = \forall a.a
top = \exists a.a

1   = \forall a.-a # a
bot = \exists a.-a * a

(where the # is the par, and the * is the tensor of linear logic, and -a
is the negation of a.)

The question that arises now is the following:

(*)   Should these logical equivalences also be isomorphisms
in a category theoretical axiomatization of the logic?