Résumé
This paper establishes the normalisation of natural deduction or lambda
calculus formulation of Intuitionistic Non Commutative Logic --- which involves
both commutative and non commutative connectives. This calculus first
introduced by de Groote and as opposed to the classical version by Abrusci and
Ruet admits a full entropy which allow order to be relaxed into any suborder.
Our result also includes, as a special case, the normalisation of natural
deduction the Lambek calculus with product, which is unsurprising but yet
unproved. Regarding Intuitionistic Non Commutative Logic with full entropy does
not have up to now a proof net syntax, and that for linguistic applications,
sequent calculi which are only more or less equivalent to natural deduction,
are not convenient because they lack the standard Curry-Howard isomorphism.