Aller au contenu principal
Il y a présentement des items dans votre panier d'achat.
Auteur et co-auteurs
Gwennaël Bricteux
UdeM - Université de Montréal
5a. Résumé

Un système de logique est composé, dans son ensemble, d'une grammaire, de règles de calcul et d'une méthode de démonstration. Le calcul logique, dans le formalisme des séquents, est consistant lorsque les coupures peuvent y être éliminées (Gentzen 1934-1935). Ce critère de l'élimination des coupures participe d'un critère plus général, qui conditionne également la structure de la grammaire et de la méthode de démonstration. Le critère de cohérence général des systèmes de logique est explicité par la théorie des catégories, dans laquelle l'élimination des coupures correspond en particulier à l'élimination de la composition (Lambek & Scott 1986, Došen 1999). La transformation d'une catégorie doit toutefois aussi préserver certaines propriétés essentielles de la composition. Le critère de cohérence général des catégories et ses réquisits particuliers correspondent alors à des critères de définissabilité grammaticale, articulée par l'éliminabilité et la conservativité de la définition; d'effectivité du calcul logique, définie par l'élimination des coupures et la propriété de sous-formule (dans le calcul des séquents); et de constructivité de la méthode de démonstration, dont le processus doit être fini et dans laquelle chaque opération doit avoir un sens déterminé. Ces critères logiques sont structurés de manière cohérente dans leur ensemble même, la limitation du formalisme étant définie de l'intérieur par son effectivité.