Théorèmes de complétude standard forts pour les logiques de Lukasiewicz modales S5

Nous étudions l'expansion modale S5 de la logique basée sur la t-norme de Lukasiewicz. Nous exhibons un calcul propositionnel finitaire et montrons qu'il est finitement fortement complet par rapport à cette logique. Ce calcul propositionnel est ensuite étendu avec une règle infinitaire pour atteindre la complétude forte. Ces résultats sont dérivés des propriétés des MValgebras monadiques : représentations fonctionnelles d'algèbres simples et finiment sous-directement irréductibles, ainsi que de la propriété d'encastrabilité finie. Nous montrons également des théorèmes de complétude similaires pour l'extension de la logique basée sur des modèles avec un univers borné.