Un système logique constructif qui interprète les connecteurs logiques en termes de provabilité ou de constructions, rejette la loi du tiers exclu non restreinte, et se formalise couramment par la déduction naturelle, les calculs de séquents, les algèbres de Heyting ou la sémantique de Kripke pour la vérité constructive.

Principe

La vérité est liée à l'existence d'une preuve ou d'une construction : une preuve de A∨B est soit une preuve de A soit une preuve de B accompagnée d'un indicateur, et une preuve de A→B est une méthode transformant toute preuve de A en preuve de B ; ¬A signifie qu'A conduit à une contradiction plutôt que d'affirmer qu'A est absolument faux.

Démonstration

En mathématiques constructives, affirmer l'existence d'un objet vérifiant P nécessite fournir une méthode pour construire cet objet ; par exemple, une preuve constructive de 'il existe n tel que P(n)' doit présenter un n précis et la vérification que P(n) tient.

Mauvaise application

Appliquer un raisonnement classique tel que l'usage d'une preuve par contradiction pour déduire l'existence sans construire de témoin (c.-à-d. déduire ∃x P(x) uniquement à partir de ¬∀x¬P(x)), ce qui enfreint les standards intuitionnistes et génère des affirmations d'existence non constructives.

Conséquence

Adopter la logique intuitionniste fait correspondre les preuves à des algorithmes ou constructions, utile pour l'extraction de programmes, la théorie des types et les mathématiques constructives, mais restreint certaines inférences classiques et exige des constructions plus explicites.

Inversion

Le renversement est la logique classique, qui accepte la loi du tiers exclu (A∨¬A) et permet des preuves d'existence non constructives via l'élimination de la double négation et d'autres principes classiques absents du raisonnement intuitionniste.

Limite

La logique intuitionniste régit le raisonnement constructif sur la vérité et la provabilité ; elle ne prescrit pas en soi la complexité computationnelle des constructions, et n'interdit pas toutes les utilisations du raisonnement par double négation dans des contextes où des principes constructifs supplémentaires les justifient.

Tension sémantique

Une tension existe avec la logique classique : certains théorèmes valides classiquement n'ont pas de preuve intuitionniste, ce qui crée un compromis entre le contenu constructif (algorithmes, témoins) et le pouvoir déductif plus large du raisonnement classique.

Synthèse

La logique intuitionniste conçoit la déduction comme production de constructions : connecteurs et quantificateurs se lisent en termes de manières de construire preuves ou témoins, fournissant une fondation proof-théorique où existence et implication portent un sens computationnel plutôt que de simples valeurs de vérité.