On the unity of logic

AbstractNous présentons un calcul des séquents unifié, commun aux logiques classique, intuitionniste et linéaire. La principale nouveautéest que les logiques classique, intuitionniste et linéaire apparaissent comme des fragments, c'estádire comme des classes particuliéres de formules et de séquents. Par exemple la démonstration d'unénoncéintuitionniste pourra utiliser des lemmes classiques ou intuitionnistes sans limitation: simplement aprèsélimination des coupures, la démonstration se fera entièrement dans le fragment intuitionniste, ce qui est superficiellement assurépar la propriétéde la sous-formule (seulement des formules intuitionnistes sont utilisées) et plus profondément par un traitement très rigoureux des règles structurelles. Cette approche est radicalement différente de l'approche habituelle qui consiste tout bonnementàchanger la règle du jeu quand on veut changer de logique, c'estàdire de style de séquent: ici il n'y a plus qu'une seule logique, qui au grédes utilisation peut apparaître classique, intuitionniste ou linéaire