Logique catégorique

La logique catégorique est la branche des mathématiques dans laquelle les outils et les concepts de la théorie des catégories sont appliqués à l'étude de la logique mathématique . Elle est également remarquable pour ses liens avec l'informatique théorique . En termes généraux, la logique catégorique représente à la fois la syntaxe et la sémantique par une catégorie , et une interprétation par un foncteur . Le cadre catégorique fournit un riche contexte conceptuel pour les constructions logiques et théoriques des types . Le sujet est reconnaissable sous ces termes depuis 1970 environ.

L’approche catégorielle de la logique repose sur trois thèmes importants :

Sémantique catégorique

La logique catégorique introduit la notion de structure valorisée dans une catégorie C avec la notion classique de structure de la théorie des modèles apparaissant dans le cas particulier où C est la catégorie des ensembles et des fonctions . Cette notion s'est avérée utile lorsque la notion de modèle de la théorie des ensembles manque de généralité et/ou est peu pratique. La modélisation de RAG Seely de diverses théories imprédicatives , telles que le Système F , est un exemple de l'utilité de la sémantique catégorique.

Il a été constaté que les connecteurs de la logique pré-catégorique étaient mieux compris en utilisant le concept de foncteur adjoint , et que les quantificateurs étaient également mieux compris en utilisant les foncteurs adjoints.

Langues internes

Cela peut être vu comme une formalisation et une généralisation de la preuve par la chasse aux diagrammes . On définit un langage interne approprié nommant les constituants pertinents d'une catégorie, puis on applique la sémantique catégorique pour transformer les assertions d'une logique sur le langage interne en énoncés catégoriques correspondants. Cela a été particulièrement efficace dans la théorie des topos , où le langage interne d'un topos ainsi que la sémantique de la logique intuitionniste d'ordre supérieur dans un topos permettent de raisonner sur les objets et les morphismes d'un topos comme s'il s'agissait d'ensembles et de fonctions. Cela a été efficace dans le traitement des topos qui ont des « ensembles » avec des propriétés incompatibles avec la logique classique . Un bon exemple est le modèle de calcul lambda non typé de Dana Scott en termes d'objets qui se rétractent sur leur propre espace de fonctions . Un autre est le modèle de Moggi -Hyland du système F par une sous-catégorie interne complète du topos effectif de Martin Hyland .

Constructions de modèles à terme

Dans de nombreux cas, la sémantique catégorique d'une logique fournit une base pour établir une correspondance entre les théories de la logique et les instances d'un type approprié de catégorie. Un exemple classique est la correspondance entre les théories de la logique équationnelle βη sur le calcul lambda simplement typé et les catégories fermées cartésiennes . Les catégories issues des théories via des constructions de modèles de termes peuvent généralement être caractérisées jusqu'à l'équivalence par une propriété universelle appropriée . Cela a permis de prouver les propriétés métathéoriques de certaines logiques au moyen d'une algèbre catégorique appropriée . Par exemple, Freyd a donné une preuve des propriétés de disjonction et d'existence de la logique intuitionniste de cette manière.

Ces trois thèmes sont liés. La sémantique catégorique d'une logique consiste à décrire une catégorie de catégories structurées qui est reliée à la catégorie des théories de cette logique par une adjonction, où les deux foncteurs de l'adjonction donnent d'une part le langage interne d'une catégorie structurée, et d'autre part le terme modèle d'une théorie.