Logique minimale

En logique mathématique, la logique minimale est une logique qui diffère de la logique classique par le fait qu'elle n'inclut ni le tiers-exclu ni le principe d'explosion. Elle a été créée par Ingebrigt Johansson. Les trois types de logiques mathématiques (logique minimale, logique intuitionniste et logique classique) sont différentes de par leur façon de traiter la négation et la contradiction dans le calcul des propositions ou le calcul des prédicats. Dans une certaine mesure, la logique minimale n'aborde pas le concept de contradiction et représente une logique sans véritable négation. La logique minimale est une logique très réduite ("minimale") qui ne contient qu'un seul et unique connecteur : l'implication (noté →). Elle est construite de façon à être une logique la plus réduite possible, comme base de construction commune à plusieurs autres, permettant ainsi de mieux étudier l'essence des propositions logiques et les notions de démonstrations et de théorème. La logique minimale, amputée du traitement de la négation, n'est pas si éloignée de la logique classique ou de la logique intuitionniste. On montre en effet que pour toute formule A, il existe une formule A' équivalente à A en logique classique, telle que A est prouvable en logique classique si et seulement si A' est prouvable en logique minimale. A' est obtenue au moyen de la traduction de Gödel, définie inductivement comme suit : pour toute formule atomique différente de Autrement dit, la traduction de Gödel d'une formule consiste à ajouter des doubles négations devant les formules atomiques, les disjonctions et les quantificateurs existentiels. Cela signifie qu'en logique classique, il suffit de faire appel à des raisonnements par l'absurde seulement devant des formules atomiques, des disjonctions ou des quantificateurs existentiels. Par exemple, le tiers exclu est un théorème de la logique classique, mais pas de la logique minimale. Par contre, la formule est démontrable en logique minimale.