TypiCal

Le thème central de cet exposé prend ces racines dans une question philosophique : quelle est la signification des constants logiques ? Ou encore, et avec plus d’ambition : y a-t-il un critère pour identifier les ‘bonnes’ constants logiques ?

Une réponse possible à ces questions peut être trouvée dans la maxime wittgensteinienne selon laquelle ‘la signification est l’usage (dans le langage)’ ; en l’appliquant au cas des constants logiques cela conduit à l’idée que leur signification est donnée par leurs règles d’inférence (position inférentialiste). Mais, ainsi formulée, cette idée est encore trop naïve, comme cela a été montré par A. Prior, grâce au connecteur pathologique tonk. Ce connecteur est défini par des règles d’inférence apparemment légitimes, mais qui, ajoutées à celles des connecteurs logiques standards, amène à l’inconsistance du système. Une manière d’éviter des connecteurs pathologiques de ce type est d'exiger la propriété de l’élimination des coupures. Toutefois, rajouter cette propriété à notre cahier des charges pour l’identification des bonnes constants logiques nous dit seulement comment éviter certaines constants pathologiques, mais elle n’explique pas la cause de la pathologie. C’est seulement en passant par une traduction de tonk dans une système d’inférence modulo certaines règles de réécriture (i.e. dans la déduction modulo) que cette explication devient possible.

Enfin, à l’aide de cette approche via règles de réécriture, j’essayerai de montrer comme même l’élimination des coupures n’est pas une condition suffisante pour l’identification des bonnes constants logiques. Ce type d’investigation me permettra aussi de regarder de plus près certaines conditions imposées sur le système de réécriture utilisés en déduction modulo (notamment la propriété de non-confusion des connecteurs).