Une logique connexive est un système logique qui admet plusieurs théorèmes qui contredisent la logique classique, mais mobilisant une notion de l'implication qui se rapproche en certains points du langage ordinaire. Dans une logique connexive, il est absurde de considérer qu'une proposition puisse impliquer, ou être impliquée, par sa propre négation, ce qui s'appelle les thèses d'Aristote. Il est aussi généralement demandé que les propositions et impliquent la négation l'une de l'autre, cela s'appelle les thèses de Boèce. Les formulations contemporaines tendent également à demander la non-symétrie de l'implication, au sens où n'implique pas nécessairement , de sorte à la distinguer de l'équivalence logique..
Histoire Époque antique Dans lOrganon, Aristote développe divers raisonnements logiques. On retrouve quelques raisonnements usuels, tels que les raisonnements par l'absurde, usité par exemple ici :
En utilisation le style de Fitch pour la déduction naturelle, nous pourrions résumer ce bout de démonstration ainsi, en utilisant les règles de modus ponens et de modus tollens :
Dans sa démonstration, en particulier, Aristote affirme que la proposition serait absurde : .
Nous pouvons analyser cette inférence anachroniquement dans le système actuel de la logique classique, où (non-B implique B) est invalidée si l'on peut démontrer B, ce pour deux raisons. En logique classique, toute proposition implique un démontrable quelconque, à savoir . De même, la négation d'un démontrable quelconque implique toute proposition (ex falso quodlibet), à savoir . Dans les deux cas, on a le théorème classe . On appelle ce genre de phénomènes des .
Il est donc important de remarquer qu'Aristote utilise les thèses suivantes, qui admetteraient pourtant des contre-exemples en logique classique, qu'on appelle thèses d'Aristote, à savoir qu'il est absurde d'affirmer (non-A implique A), et qu'il est absurde d'affirmer (A implique non-A).
L'appellation est dérivée d'une remarque donnée par Sextus Empiricus :
La logique connexive s'inscrit toutefois, au moins au départ, dans un courant aristotélicien.
Époque médiévale L'époque médiévale a vu plusieurs développements en logique connexive, en passant de Boèce à Robert de Melun (†1167), en passant par Abélard.
Boèce a notamment donné son nom à deux thèses, qui sont aujourd'hui considérées comme nécessaires pour qualifier une logique de connexive. Celles-ci viennent de l'extrait suivant :
On peut ré-exprimer cela ainsi. :
Cela indique que Boèce considère comme contradictoires et . À noter que l'extrait d'Aristote précédent y ressemblait fortement, puisqu'il affirme qu'il n'est pas possible d'avoir et . Cet extrait de Boèce a été ensuite décliné de différentes manières, mais la formulation que nous retenons de nos jours est celle décrite précédemment, à savoir : les propositions et impliquent la négation l'une de l'autre.
Abélard souscrivait également à la logique connexive. Dans son Dialectica, celui-ci explique que les conditionnelles et ne peuvent être toutes deux vraies, sinon quoi nous pourrions décliner la proposition inconvéniente suivante : si quelqu'un est un homme, il n'est pas un homme. Par ailleurs, Abélard a lui-même donné son nom à deux thèses, l'un étant la deuxième d'Aristote, et l'autre étant la non-simultanéité de et , à savoir ce qu'on formalise de nos jours comme le schéma d'axiomes .
Robert de Mélun, inspiré d'Abélard, apporte également avec lui et un principe général, caractérisée par la phrase (trad. ). L'auteur anonyme de lArs Meliduna, basé sur les travaux de Robert de Mélun, donnait plutôt une interprétation faible de cette phrase, au sens (d'une impossibilité rien ne suit), tandis que les Meludinenses suivaient plutôt ().
Approches contemporaines La définition contemporaine en logique formelle d'une logique connexive est un système formel qui satisfait certaines propriétés spécifiques : Les thèses d'Aristote, les thèses de Boèce, et la non-symétrie de l'implication.
Les thèses d'Aristote réfèrent à deux schémas d'axiomes. L'une dit qu'on peut toujours nier la proposition, (non-A implique A) ; Il s'agit donc du schéma d'axiomes . L'autre dit qu'on peut toujours nier la proposition, (A implique non-A) ; Il s'agit du schéma d'axiomes .
Les thèses de Boèce réfèrent à deux autres schémas d'axiomes. D'une part, que A implique B, implique toujours la négation de, A implique non-B ; Il s'agit donc du schéma d'axiomes . D'autre part, que A implique non-B, implique toujours la négation de, A implique B ; Il s'agit donc du schéma d'axiomes .
Que l'implication soit demandée de ne pas être symétrique, signifie que de A implique B, on n'a pas nécessairement que B implique A. On la décrit par l'invalidation du schéma d'axiomes . Cela permet deux choses : D'une part, à distinguer l'implication de l'équivalence logique ; D'autre part, à assurer la cohérence du système.
Connexivité totale Estrada-González et Ramirez-Cámara identifient plusieurs désidératas.. Une logique connexive est abélardienne si elle vérifie les schémas d'axiomes suivants : ; . Elle est anti-paradoxe, au sens des paradoxes de l'implication matérielle, si les schémas d'axiomes suivants ne sont pas universellement valides : ; ; pour un contingent et un démontrable . Elle est Kapsner-forte si est insatisfaisable, et que et ne sont pas simultanément satisfaisables. Elle est simplificatrice si sont validés les schémas d'axiomes suivants : ; . Elle est conjonction-idempotente sont les schémas d'axiomes sont valides : ; .
Une logique connexive qui satisfait tous ces désidératas serait appelée totalement connexive. Cependant, aucun tel système n'a été trouvé jusqu'à aujourd'hui..
Sémantiques fonctionnelles Certaines sémantiques fonctionnelles ont été développées pour diverses logiques connexives, dont , , , et de nombreuses autres.. Les sémantiques décrites ici sont polyvalentes, avec au moins trois valeurs de vérité. Dans les sémantiques polyvalentes, une valeur désignée est une valeur de vérité qui, essentiellement, prend le rôle de la valeur dans la conséquence sémantique, de sorte que si toutes les prémisses ont une valeur désignée alors la conclusion a elle aussi une valeur désignée.
Système Développé par Heinrich Wansing en 2005, le système a été au départ conçu pour traiter la logique modale de façon connexive.. Son fragment propositionnel a été ensuite étudié à part comme socle de théorie de la preuve connexive propositionnelle.
Il s'agit d'une logique structurelle comme la logique classique, qui vérifie donc la règle d'axiome, la règle de coupure, la règle de permutation, la règle de contraction et la règle d'affaiblissement. Sur le plan inférentiel, si cette logique admet les mêmes règles d'introduction et d'élimination que la logique classique pour la conjonction, la disjonction, l'implication, on s'inspire de la théorie de la preuve de David Nelson pour développer des règles d'introduction et d'élimination pour la négation de chaque opération, à savoir la négation de la négation (double négation), la négation de la conjonction et la négation de la disjonction.. Toutefois, pour la négation de l'implication, les règles diffèrent de en cela qu'elles forcent la connexivité. :
Cette logique est toutefois übercohérente, ce qui signifie qu'il existe des paires de théorèmes contradictoires, deux formules universellement valides bien que l'une est la négation de l'autre.. On parle aussi de dialethéias, qu'on appelle aussi des vraies contradictions. C'est notamment le cas des théorèmes et de . Toutefois, la logique n'est pas triviale. En particulier, il en existe un modèle sain à quatre valeurs appelé , avec pour valeurs T, B, N et F, avec pour valeurs désignées B et T :
T B N F T T B N F B B B F F N N F N F F F F F F{| class="wikitable" style="text-align: center;" T B N F T T T T T B T B T B N T T N N F T B N F
| {| class="wikitable" style="text-align: center;"
! !! T !! B !! N !! F
! T | T || B || N || F
! B | T || B || N || F
! N | B || B || B || B
! F | B || B || B || B
{| class="wikitable" style="text-align: center;"
! !!
! T | F
! B | B
! N | N
! F | T
À noter toutefois que cette logique est paracomplète, ce qui signifie qu'elle n'a pas le principe du tiers exclu. En ajoutant la loi du tiers exclu, on obtient la logique de négation conditionnelle., dont un modèle fonctionnel à trois valeurs existe, avec pour valeurs T, B et F, tels que les valeurs T et B sont désignées :
T B F T T B F B B B F F F F F{| class="wikitable" style="text-align: center;" T B F T T T T B T B B F T B F
| {| class="wikitable" style="text-align: center;"
! !! T !! B !! F
! T | T || B || F
! B | T || B || F |- ! F | B || B || B
{| class="wikitable" style="text-align: center;"
! !!
! T | F
! B | B
! F | T
Références
Catégorie:Histoire de la logique Catégorie:Histoire de la philosophie Catégorie:Philosophie de la logique