In categorial semantics, formulas are interpreted as multivariant functors and proofs as dinatural (or, more precisely, extranatural) transformations between such functors. In this context the correct notion of universal quantification is not the usual one (intersection) but the notion of "end". From a proof-theoretic viewpoint, dinaturality and extranaturality correspond to permutative principles (i.e. the fact that closed proofs are invariant, modulo normalization, with respect to a class of permutations). However this fact, which holds at the propositional and first-order level, fails for second order logic (i.e. System F), due to the fact that the rules of second order quantification do not correspond to the definition of an end. As a consequence, System F is not fully dinatural.

In order to explore a notion of proof invariant with respect to all permutations arising from dinaturality/extranaturality I will consider proof-nets for two main reasons: first, proof-nets were invented to obtain proofs invariant with respect to permutation of rules; second, cut-elimination in proof-nets closely corresponds to composition of dinatural/extranatural transformations (as it appears clearly in Eilenberg-MacLane coherence theorems for monoidal categories). I will introduce a new notion of proof-net for second order logic reflecting these categorial intuitions. Such proof-nets will be shown to be invariant with respect to all permutations arising from dinaturality.