Logique non classique

Logiques constructives

Les logiques constructives sont des logiques qui satisfont les propriétés de disjonction et d'existence (en). La première décrit que tout théorème disjonctif ${\displaystyle A\lor B}$ est tel que ${\displaystyle A}$ est un théorème ou ${\displaystyle B}$ est un théorème. La second décrit que pour tout théorème existentiel ${\displaystyle (\exists x)P[x],}$ on peut construire ${\displaystyle x_{0}}$ tel que ${\displaystyle P[x_{0}]}$ est un théorème.

La logique intuitionniste en est un exemple majeur. Toute logique sous-intuitionniste est constructive. Un exemple de logique sous-intuitionniste est logique minimale.

Logiques sous-structurelles

Les logiques sous-structurelles sont des logiques dans lesquelles certaines règles structurelles ne s'appliquent pas. On parle parfois de logiques à ressources, comme en logique linéaire.

En particulier, nous retrouvons deux sous-familles :

• Les logiques non-contractives, où la règle de contraction ne s'applique pas. Nous y retrouvons notamment la logique linéaire et la logique affine (en).
• Les logiques non-monotones, où la règle d'affaiblissement ne s'applique pas. Nous y retrouvons notamment la plupart des logiques pertinentes, ainsi que la logique linéaire.

Logiques paracohérentes

Les logiques paracohérentes sont des logiques où le principe d'explosion ne s'applique pas. On retrouve notamment la logique minimale, les logiques pertinentes et les logiques übercohérentes.

Deux exemples de logiques paracohérentes majeures sont FDE, qui a pour particularité de n'avoir aucun théorème, et la logique des paradoxes LP de Graham Priest.

Logiques sociatives

Les logiques sociatives sont des logiques qui tentent d'établir un critère de lien entre prémisse et conséquent dans tout théorème conditionnel.

Nous retrouvons notamment deux sous-familles spécifiques :

• Les logiques pertinentes, dont le critère est initialement la propriété de partage des variables, en imposant également que le syllogisme disjonctif ne s'applique pas, pour éviter le principe d'explosion.
• Logiques connexives, dont le critère est lié à la déduction d'implications niées, via des règles contra-classiques appelées thèses d'Aristote et thèses de Boèce.

Logiques avec plus d'expressivité que la logique du premier ordre

• Logique d'ordre supérieur, où la quantification porte aussi sur des fonctions et des prédicats.
• logique infinitaire, avec des énoncés infiniment long et/ou des preuves infinies.

Logiques avec un vocabulaire enrichi par rapport à la logique classique

• Logiques modales, toute une famille de logiques ajoutant au langage initial des opérateurs comme possibilité et nécessité.
  • Logique déontique, relative au droit et ce qui est permis ou interdit.
  • Logique épistémique qui introduit des agents ayant telle ou telle connaissance.
• Logique temporelle, qui introduit une notion de temporalité sur la validité des énoncés.

Logiques contra-classiques

Les logiques contra-classiques sont des logiques qui admettent des règles qui rentrent en conflit avec la logique classique, dans le sens qu'étendre la logique classique avec certaines de ces règles conduit à la logique triviale. Par exemple :

• Les logiques connexives admettent en particulier comme axiome contra-classique les thèses de Boèce, ${\displaystyle (A\to B)\to \neg (A\to \neg B)}$ et ${\displaystyle (A\to \neg B)\to \neg (A\to B),}$ de sorte que si l'implication vérifie la règle de détachement, alors toute théorie permettant de prouver ${\displaystyle (A\to B)}$ et ${\displaystyle (A\to \neg B)}$ simultanément est incohérente.
• La logique des termes d'Aristote est contra-classique, notamment par la relation de subalternation qui conduit en particulier à déduire (quelque A est B) à partir de (tout A est B), la formalisation classiciste de cette règle conduisant à la règle contra-classique ${\displaystyle ((\forall x\in P,x\in Q)\to (\exists x\in P,x\in Q))}$.
• La logique abélienne est une logique admettant pour modèles algébriques les groupes abéliens ordonnés par un treillis, aussi appelés ℓ-groupes. La logique abélienne admet ainsi, en particulier, l'axiome contra-classique de relativité, ${\displaystyle ((A\to B)\to B)\to A,}$ qui généralise la loi d'élimination de la double négation ${\displaystyle \neg \neg A\to A\mathbin {\stackrel {\rm {def}}{=}} ((A\to \bot )\to \bot )\to A.}$
• Les logiques übercohérentes, qui admettent au moins deux théorèmes tels que l'un est la négation de l'autre, sont également contra-classiques à cause du principe d'explosion en logique classique.