Cet article est indexé par les projets Philosophie, Sciences, Logique et Mathématiques.

Les projets ont pour but d’enrichir le contenu de Wikipédia en aidant à la coordination du travail des contributeurs. Vous pouvez modifier directement cet article ou visiter les pages de projets pour prendre conseil ou consulter la liste des tâches et des objectifs.

Évaluation de l’article « Logique intuitionniste »

Avancement	Importance	pour le projet
B	Moyenne		Philosophie (discussion • critères • liste • stats • hist. • comité • stats vues)
			Sciences (discussion • critères • liste • stats • hist. • comité • stats vues)
	À évaluer		Logique (discussion • critères • liste • stats • hist. • comité • stats vues)
			Mathématiques (discussion • critères • liste • stats • hist. • comité • stats vues)

Cet article ne comporte pas de liste de tâches suggérées. Vous pouvez saisir une liste de tâches à accomplir (par exemple sous forme d'une liste à puces), puis sauvegarder. Vous pouvez aussi consulter la page d'aide.

Ne serait-il pas mieux de mettre les régles de déduction naturelle dans l'article correspondant ? D'autant plus que ce dernier, est touffu, peu clair, ...

Laurent, suggére de mettre dans logique intuitionniste les motivations de Brouwer, et la nouvelle approche des mathématiques constructives.

Ce qui nous amenerait à parler des régles dans Déduction naturelle.

Marc 25 janvier 2006 à 12:44 (CET)Répondre

Je n'ai pas d'objection. Mais attendons que cet article évolue, vers plus de clarté. S'il y a redondance, on supprimera ici.

Pierre de Lyon 25 janvier 2006 à 15:34 (CET)Répondre

Cet article est-il encore une ébauche? Pierre de Lyon 14 mars 2007 à 22:59 (CET)Répondre

Personne n'ayant répondu à ma question, j'y ai répondu moi-même négativement et j'ai supprimé l'entête ébauche. Pierre de Lyon 7 novembre 2007 à 11:39 (CET)Répondre

Ai-je bien compris que les parties de ce jeu sont de longueur bornée, en fonction du damier de départ ? Auquel cas, tout est fini, et je ne vois pas comment la preuve d'existence d'une stratégie gagnante ne serait pas finalement constructive. Le fait qu'elle ne donne pas de réelle stratégie semble plutôt une question de complexité, et ça n'a pas à voir avec la logique intuitionniste. Proz (d) 20 mars 2009 à 23:51 (CET)Répondre

Tu as raison. J'ajouterais deux choses

1. On utilise le théorème de Brouwer pour démontrer l'existence d'une stratégie mixte, or dans le jeu de Hex, on ne s'intéresse qu'aux stratégies pures. Que ferait-on d'une stratégie mixte ? L'existence d'une stratégie s'appuie à mon avis plutôt sur le théorème de Zermelo sur les jeux.
2. On connait depuis Nash des versions constructives du théorème de Brouwer.

Pierre de Lyon (d) 21 mars 2009 à 08:50 (CET)^[1]Répondre

Je supprime le paragraphe en question, qui repose sur une confusion, même si la démonstration d'existence d'une stratégie gagnante pour le premier joueur décrite sur Hex (sachant que le jeu est déterminé) est bien un joli raisonnement par l'absurde (mais le jeu étant fini ...). Pour le reste j'avoue mon ignorance, je ne sais pas ce qu'est une stratégie mixte. Proz (d) 21 mars 2009 à 14:19 (CET)Répondre

Euh, je n'ai pas là de ref, mais le fait qu'il existe une démonstration non constructive qu'il y a une stratégie gagnante pour le jeu d'Hex (pour un des joueurs) est très connu (me demande si Gardner n'en parle pas dans un de ses livres). Bien sûr cela ne fait sens que si on considère un jeu infini OU (je ne sais) qu'il existe une stratégie gagnante pour tout jeu d'hex fini. --Epsilon0 ε₀ 21 mars 2009 à 16:37 (CET)Répondre

1. Une stratégie « mixte » est une stratégie qui est un combinaison de plusieurs stratégies « pures » en utilisant des probabilités.
2. D'après l'article Hex, ce jeu est fini.

Pierre de Lyon (d) 24 mars 2009 à 10:22 (CET)Répondre

Je ne vois pas pourquoi une démonstration de l'existence d'une stratégie gagnante serait nécessairement constructive dans le cas d'un jeu fini. Qui fait une confusion ? peut-être que le théorème du point fixe de Brouwer sert à autre chose que les stratégies mixtes (effacer les sources avant de regarder c'est pas malin). Peut-être que le principe du tiers exclu est utilisé en dehors du théorème de Brouwer. N'y aurait-il pas une nouvelle confusion ? Là encore effacer les sources sans les regarder n'est pas très subtil. Jean-Luc W (d) 31 mars 2009 à 12:41 (CEST)Répondre

Je ne vois pas comment on peut penser que j'ai pu écrire ce qui est au dessus sans aller lire au moins l'article Hex (fort intéressant au demeurant). Les "mystères" de la communication sur les pdd wikipédiennes, mais passons. Il m'a semblé clair qu'il y avait confusion entre des problèmes de décidabilité algorithmique et de complexité. La logique intuitionniste (le sujet de l'article !) ne dit rien en tant que telle sur la complexité. La seule référence extérieure (ce n'est sûrement pas une source de ce qui était écrit dans l'article) est disponible sur l'article Hex. Elle source bien (s'il en était besoin) qu'il s'agit de complexité et donne des détails (P-SPace complet, on est dans le cadre de la deuxième proposition d'epsilon0, un jeu fini de taille n en entrée, pour que ces choses aient un sens). Quand on ne manipule que des objets finis en nombre fini, tout est vérifiable algorithmiquement (théoriquement), le tiers-exclu se démontre intuitionnistiquement. Si on part alors de ce principe, la preuve va probablement donner un algorithme idiot qui consiste à tout simuler puis à agir en conséquence, ce qui est rapidement impraticable, mais ce n'est pas le sujet.

C' est différent pour l'exemple de l'article (dû je crois à Brouwer) : on ne peut pas décider algorithmiquement qu'un réel (calculable), est ou non rationnel, pas de tiers-exclu dans ce cas (pour les intuitionnistes). Proz (d) 2 avril 2009 à 00:58 (CEST)Répondre

En effet, des commentaires comme Auquel cas, tout est fini, et je ne vois pas comment la preuve d'existence d'une stratégie gagnante ne serait pas finalement constructive ne laisse pas penser que tu as bien lu ou bien compris l'article et ses sources. En 2009, on ne connait pas de preuve constructive de l'existence d'une stratégie gagnante. Le fait que le jeu soit fini ne change en rien cet état de fait.

Je crois que tu devrais relire ce qu'est la logique intuitionniste. Il y a une source dans l'article Théorème du point fixe de Brouwer. Ce que tu sembles ne pas comprendre, c'est la question majeure de Brouwer. Il refuse une preuve non constructive. Tu devrais lire ce qu'il raconte sur ses démonstrations topologiques. La preuve de Nash utilise deux fois le principe du tiers exclu et rend sa démonstration non constructive (rien à voir avec une question de complexité). Le jeu de Hex fait beaucoup plus sens que celui cité pour l'instant. Un lecteur aura bien du mal à comprendre pourquoi Brouwer refuse des preuves pourtant limpides comme celle présentée en exemple (qui fait passer Brouwer pour au mieux un pinailleur, au pire un abruti, ce qu'il n'était pas). Avec le jeu de Hex, on comprend pourquoi le principe du tiers exclu ne fournit qu'une réponse que très moyennement satisfaisante : un joueur ne peut rien en faire de la preuve mathématique.

Pierre de Lyon confond l'usage du théorème de Brouwer. La preuve de Nash est équivalente au théorème de Brouwer, mais n'a rien à voir avec une stratégie mixte.

Pierre de Lyon confond encore la nature de la preuve de Nash, qui n'a rien à voir avec Zermelo, mais avec le principe de la stratégie volée (une invention de Nash d'après les sources). Le tiers exclus n'est pas uniquement utilisé dans la preuve du théorème de Brouwer mais déjà dans dans l'argument de la stratégie volée. les travaux de Scarf ne change donc en rien le caractère non constructif des preuves connues.Jean-Luc W (d) 2 avril 2009 à 10:02 (CEST)Répondre

1. Puisque maintenant tu m'accordes que j'ai lu l'article, un petit effort de lecture supplémentaire et tu verras ci-dessus (message du 21 mars) que notre point de désaccord ne porte pas sur le fait qu'il s'agit d'un raisonnement par tiers exclu (par l'absurde ça revient au même).
2. La référence externe que tu avais ajouté à l'article est http://maarup.net/thomas/hex/ : le paragraphe "complexité" étudie la complexité théorique de la recherche d'une stratégie gagnante (ce qui n'a de sens que si un algorithme de recherche de stratégie en fonction d'une entrée de taille n donnée existe). Lire également la thèse en lien sur la page : p 27 "the theorem is only one of existence and makes no promise of a practical construction of the winning strategy" (ne pas oublier de lire "practical") et le chap 5 en particulier la p. 31.
3. Le fait (basique) que le tiers exclu est valide intuitionnistiquement pour le fini : tu as par exemple une citation de Kleene là : en:Law of excluded middle, une explication (avec référence à Brouwer) là : http://plato.stanford.edu/entries/logic-intuitionistic/ (article de en:Yiannis N. Moschovakis.
4. L'exemple est multi-cité sur le sujet (voir en:Law of excluded middle, qui cite entre autres en:Martin Davis). C'est un exemple pédagogique qui permet de comprendre simplement pourquoi on conteste le tiers-exclu d'un point de vue constructif.
5. Le théorème du point fixe de Brouwer : je suis arrivé sur le présent article (auquel je n'avais pas participé), par son intermédiaire. Les quelques lignes sur l'intuitionnisme sont largement des contre-sens (la note 6 en particulier). Comme c'est mineur dans l'article ça ne m'a pas paru urgent d'intervenir. L'article cité de Dubucs, est tout à fait intéressant, (pas vraiment exploité dans l'article).

Un exemple qui porte sur le fini ne peut être pertinent, les point 3 et 4 clôturent ce débat. Pour le point 5 ce n'est pas le lieu de poursuivre (et si l'échange, doit être sur ce ton, ça ne m'intéresse guère). Proz (d) 4 avril 2009 à 12:51 (CEST)Répondre

Bonjour, Je ne me suis pas plongé dans le thm de Nash ou ses généralisations ultérieures, donc je ne sais dans quel cas on se trouve :

• 1. Si le thm dit qu'on a une preuve non-constructive que pour une version finie donnée du jeu "1er joueur a une stratégie gagnante", alors on sait qu'il en existe une preuve constructive (par force brute exhaustive au pire).
  • Ceci est quelque chose qui est intéressant à mettre dans l'article, pour illuster : dans le cas fini, s'il existe 1 preuve non-constructive, il en existe une preuve constructive (et ce n'est pas vrai dans le cas d'un jeu infini.). En l'illustrant par l'exemple du jeu d'Hex qui est très connu.
• 2. Si le thm va plus loin et dit qu'on a une preuve non-constructive que pour toute version finie donnée du jeu "1er joueur a une stratégie gagnante" (ce qui me semble le cas)alors :
  • 2.1. pour tout n, il existe une preuve constructive, que "1er joueur a une stratégie gagnante" (toujours par force brute par exemple).
  • Mais on n'a pas forcément 2.2. Il existe une preuve constructive, que pour tout n, "1er joueur a une stratégie gagnante" . A moins que 2.1. --> 2.2. (cela ne me semble pas évident, mais c'est possiblement un thm classique de calculabilité, le savez-vous ?)
  • Si 2.1. n'implique pas 2.2. , là l'exemple du cas d'Hex est aussi intéressant à mettre dans l'article que le célèbre exemple : existent 2 irrationnels a et b tels que a^b est un rationnel.
• Dans tous les cas, quelque chose qui n'est pas anodin de mentionner (mais ce peut être fait rapidement), c'est que l'on peut démontrer à une époque donnée l'issue d'un jeu joué parfaitement en utilisant le tiers exclu, alors qu'à cette même date on ne peut le faire sans le tiers exclu vu la barrière combinatoire. ex : à ma connaissance pour le jeu d'échecs qui est fini (certaines règles de nullité l'impliquent) on ne sait l'issue (gain blanc, gain noir ou nulle) d'une partie parfaitement jouée des 2 côtés, ce qui fait que le thm de Nash concernant Hex est intéressant à cet égard (mais ça relève p.-e. plus de l'article sur la théorie des jeux).

Après peut bien sûr se poser une question de la complexité algorithmique (np, time, space) en fonction de la taille de l'entrée, mais là cela ne concerne pas la distinction constructif/ non-constructif.

--Epsilon0 ε₀ 2 avril 2009 à 22:10 (CEST)Répondre

D'un point de vue formel, l'énoncé est un énoncé d'arithmétique (tout se code par des entiers), le prédicat "s est une stratégie gagnante pour le jeu de taille n" est récursif (pour des raisons simples, primitif récursif par ex.). Comme il n'y a qu'un nombre fini (2 coups d'exponentielle en gros) calculable de stratégies, n étant fixé, le prédicat "le jeu de taille n admet une stratégie gagnante" est récursif également. Un tel prédicat P(n) équivaut à sa double négation (arguments développés ci-dessus en gros). La preuve se fait par l'absurde pour chaque n (on ne suppose pas que c'est le fait que pour toute taille de jeu le premier joueur n'a pas de stratégie gagnante qui mène à une contradiction) donc on a bien montré "Pour tout n P(n)" intuitionnistiquement.

De plus, même si c'était le cas, pour un énoncé P(n) décidable (donc équivalent à sa double négation), on montre facilement que "non non Pour tout n P(n)" équivaut à "Pour tout n P(n)" intuitionnistiquement. Tu montres donc que "Pour n P(n)" est prouvable en arithmétique intuitionniste ssi il l'est en arithmétique classique (on peut aller jusqu'à pour tout il existe ..., en fait mais il faut d'autres arguments).

Pour que 2.1 n'entraîne pas 2.2, il faut être dans une théorie où tu n'as pas de preuve classique non plus, tu es exactement dans des énoncés Pi^0_1 du type Gödel (th. valide intuitionnistiquement d'ailleurs), ça dépend de la théorie, et ici c'est hors de propos. Proz (d) 4 avril 2009 à 13:20 (CEST)Répondre

Proz a raison, j'ai tort. L'argument est simple : le tiers exclu est autorisé pour les ensembles finis dans la logique intuitionniste. La raison est fort bien expliquée dans en:Law of excluded middle. Jean-Luc W (d) 4 avril 2009 à 13:07 (CEST)Répondre

Merci Proz pour ces explications très claires, mon doute est totalement levé et tu as raison, comme bien souvent ;-). --Epsilon0 ε₀ 4 avril 2009 à 20:35 (CEST)Répondre

En fait, les logiciens qualifient de « décidable » un prédicat P pour lequel on peut prouver ${\displaystyle \forall x,P(x)\vee \neg P(x)}$. Ce que Proz vient de dire, c'est que tous les prédicats sur les ensembles finis sont décidables. Pierre de Lyon (d) 6 avril 2009 à 11:33 (CEST)Répondre

Je ne me mêlerai certes pas du jeu de Hex ; cependant, concernant les ensembles finis, j'ai trouvé ceci dans archive.numdam.org dans un travail consacré à Heyting:

« ….and (4) if recursion theory is interpreted classically, certain intuitionistic distinctions, but not all, have their counterpart in recursion theory, if we translate effective by recursive. A simple illustration of the fourth remark : intuitionistically, not every subset of a finite set can be proved to be decidable ; classically every subset of a finite set is recursive. » Je ne sais pas si ça a à voir avec ce que vous dites. --Michel421 (d) 1 novembre 2009 à 18:59 (CET)Répondre

Il s'agit d'ensembles d'entiers. Ca signifie me semble-t-il que l'on peut définir un sous-ensemble d'un ensemble fini (au sens intuitionniste) par des moyens non constructifs, en utilisant un prédicat non décidable : dans ce cas l'appartenance ne serait pas décidable. En fait il est faux de dire ex abrupto que le tiers exclu est autorisé pour les ensembles finis en logique intuitionniste, il faut encore que les objets eux-mêmes soient finis (pas seulement l'ensemble) ce qui est le cas dans l'exemple en cause ici (le bon argument utilise la complexité logique des prédicats en cause). Mais quand tu définis un sous-ensemble d'un ensemble fini tu peux introduire de l'infini (dans la preuve d'appartenance à ce sous-ensemble, en le faisant dépendre d'un prédicat sur les entiers qui n'est pas décidable). La notion d'ensemble et surtout de sous-ensemble utilise l'extensionnalité, or l'égalité extensionnelle n'a aucune raison d'être décidable, donc il faut être prudent avec ces notions pour l'intuitionnisme. Proz (d) 1 novembre 2009 à 20:20 (CET)Répondre

Afin de bien situer de quoi on parle, il me parait intéressant de proposer une bibliographie.

Deux livres généraux de cours sur la théorie des jeux, où sont définis, entre autres, les concepts de stratégie mixte et d'équilibre de Nash

1. M. J. Osborne. An Introduction to Game Theory, Oxford, 2004.
2. M. J. Osborne et A. Rubinstein. A Course in Game Theory, The MIT Press, Cambridge, Massachusetts, 1994.

auquel il faut ajouter l'article de Zermelo de 1913: On an Application of Set Theory to the Theory of the Game of Chess in Rasmusen E., ed., 2001. Readings in Games and Information, Wiley-Blackwell: 79-82.

Il s'agit d'une théorie plus récente où ce qui est mis en évidence est l'aspect algorithmique des jeux avec une focalisation sur le théorème de Brouwer constructif.

1. Contantinos Daskalakis, Paul W. Golberg et Christos H. Papadimitriou. The complexity of computing a Nash equilibrium. Communications of the ACM, 52(2):89--97, 2009. Un article tout récent qui fait une excellente synthèse du sujet par leurs initiateurs, avec une très bonne présentation du théorème de Brouwer constructif.
2. Noam Nisan, Tim Roughgarden, Eva Tardos, and Vijay V. Vazirani, Algorithmic Game Theory. Cambridge University Press, New York, NY, USA, 2007. une somme complète sur le sujet.
3. David S. Johnson, The NP-completeness column: Finding Needles in Haystacks, ACM Transactions on Algorithms, 3(2), 2007

Pierre de Lyon (d) 6 avril 2009 à 11:25 (CEST)Répondre

Si je suis lecteur de Wiki et que je me pose la question « étant donné E⊂X, y a-t-il un procédé de construction de l'ensemble des éléments de X qui n'appartiennent ni à E ni à C_XE ? » est-ce que l'article me fournit tous les éléments qui me permettraient de dire oui, de dire non, ou de dire pourquoi la question n'a pas de sens ?--Michel421 (d) 25 octobre 2009 à 00:04 (CEST)Répondre

Si je l'ai bien comprise, il me semble que cette question n'a pas de sens. De même qu'on ne peut pas tout démontrer en math, on ne peut pas tout mettre dans un article. --Pierre de Lyon (d) 25 octobre 2009 à 13:42 (CET)Répondre

Alors, partons sur quelque chose de plus simple: est-ce qu'en logique intuitionniste il peut arriver que E ≠ C_xC_xE ? Normalement oui, car la double négation non[non x∈E] n'entraîne pas x∈E. J'ai cependant du mal à imaginer à quoi pourrait ressembler [C_xC_xE] - E (on parle d'ensembles infinis). --Michel421 (d) 27 octobre 2009 à 09:54 (CET)Répondre

Soit P un prédicat, on dit que P est décidable si pour tout x on a P(x) ∨ non P(x). Si E est défini par un prédicat décidable alors oui E=C CE. (N.B. Je ne sais pas ce que signifie le souscrit x). Si P n'est pas décidable, il existe des x pour lesquels on ne pas dire si ils appartiennent à E ou non. On ne pourra pas démontrer « pour tout x∈X, non non P(x) ⇒ P(x) »--Pierre de Lyon (d) 28 octobre 2009 à 21:52 (CET)Répondre

Merci pour la réponse. "X" est placé en indice pour indiquer que c'est du complémentaire par rapport à X qu'il s'agit. --Michel421 (d) 29 octobre 2009 à 09:52 (CET)Répondre

Section approche formelle, je lis "si pour tout monde ${\displaystyle m'}$ tel que ${\displaystyle m\leq m'}$ on a si ${\displaystyle m\Vdash \psi }$ alors ${\displaystyle m\Vdash \theta }$.", je crois que les deux derniers m sont des m', c'est la seule chose qui a du sens, si quelqu'un peu confirmer se serait sympa, mais comme j'ai peu de doute j'édite.

--Arthur MILCHIOR (d) 7 mai 2010 à 18:25 (CEST)Répondre

Le document commence avec une présentation des fondements de l’exclusion du tiers-exclus. Je me demande s’il n’y aurait pas une erreur dans la présentation : « Si ${\displaystyle {\sqrt {2}}^{\sqrt {2}}}$ est rationnel,  » ne devrait-il pas être « Si ${\displaystyle {\sqrt {2}}^{\sqrt {2}}}$ est irrationnel,  » ? En tous cas, ce serait nécessaire pour que ce soit cohérent avec l’énoncé. Dans tous les cas (non mathématicien), cette présentation ne me parait pas aisément compréhensible. --Hibou57 (d) 7 juin 2010 à 20:07 (CEST)Répondre

@Anne Bauval: merci pour les tentatives de rendre la motivation de l’exclusion du tiers-exclus plus claire, mais je ne la trouvais pas encore suffisamment claire. Après m’être soigneusement (enfin, du mieux que j’ai put) penché sur la question, j’ai tenté d’ajouter encore quelques éléments à la formulation. Pouvez-vous vérifier ? Merci. J’espère ne pas être trop ennuyeux avec mon insistance sur ce point, mais c’est que l’exclusion du tiers-exclus semblant si importante dans cette logique, je trouve important d’en faire un aspect compréhensible. Si mes modifications sont fausses, ce sera en tous les cas le signe que je ne l’ai pas encore compris. Merci et bonne journée.

--Hibou57 (d) 8 juin 2010 à 16:10 (CEST)Répondre

Ue phrase extraite du document : « Rappelons qu'en déduction naturelle ${\displaystyle \Gamma \vdash \varphi }$ doit se lire ... ». Mais cela n’est dit nul part auparavant, donc ce n’est pas un rappel. Manque t-il quelque chose ou faut-il re-éditer la formulation ? Dans le doute, je préfère poser la question.

--Hibou57 (d) 7 juin 2010 à 20:28 (CEST)Répondre

Le document contient la phrase : « est le fait que chaque connecteur (${\displaystyle \vee ,\wedge ,\bot }$)… ». Mais ${\displaystyle \bot }$ n’est pas un connecteur, il est le symbole de la contradiction. N’y a-t-il pas confusion avec ${\displaystyle \vdash }$, qui lui est par contre effectivement utilisé comme un connecteur ? Comme je ne suis pas particulièrement spécialiste de la logique intuitionniste, j’hésite à corriger moi-même.

--Hibou57 (d) 7 juin 2010 à 20:35 (CEST)Répondre

Oui, c’est certain, il y a une erreur ici, et c’est en fait ${\displaystyle \Rightarrow }$ et non même pas ${\displaystyle \vdash }$, comme cela est confirmé par les règles d’introduction et d’élimination des connecteurs. Je corrige. Si je fait erreur avec cette modification, il n’y aura qu’à revenir en arrière, mais c’est une certitude pour moi qu’il y a une erreur.

--77.198.58.167 (d) 7 juin 2010 à 21:45 (CEST)Répondre

${\displaystyle \bot }$, ou "bottom" ou le Faux (comme le Vrai) est un connecteur, c'est un connecteur 0-aire et d'ailleurs il se retrouve, au moins en logique classique, parmi les 4 connecteurs unaires (vrai, faux, position et négation), 16 connecteurs binaires, etc. ${\displaystyle \vdash }$ est le symbole de la déduction, il se comporte si on veut comme le connecteur qu'est l'implication, sauf qu'on n'est pas dans le langage mais dans le métalangage. --Epsilon0 ε₀ 8 juin 2010 à 11:07 (CEST)Répondre

D’accord, mais comme il ne semble pas exister de symbole explicite pour le Vrai, je pense que c’est complet. Comme personne n’a annulé la modification (c’était moi sous 77.198.58.167, je me suis trouvé déconnecté accidentellement), je pense qu’elle était juste. À moins que personne ne l’ai contrôlé (oops, je voudrais être sûr)… Merci pour le complément d’explication ; et c’est donc un connecteur 0-aire. OK.

--Hibou57 (d) 8 juin 2010 à 15:06 (CEST)Répondre

Si on a besoin d'un symbole pour le vrai on en invente un ou on utilise T, comme true et l'inverse du bottom ${\displaystyle \bot }$, ce qui est le plus usuel avec le V francophone. --Epsilon0 ε₀ 8 juin 2010 à 15:25 (CEST)Répondre

J’étais bien intéressé par ce sujet que j’avais déjà abordé à d’autres occasions sans en connaitre le nom véritable. Pourtant, j’ai décidé de ne plus éditer le sujet ici, et de le poursuivre sur un autre site. J’en donnerai les raisons un autre jour sur ma page de discussion (ça me fatigue ces problèmes que wikipédia a avec le monde extérieur, et son mépris même des sources, ça ne s’arrête pas au nofollow, c’est encore plus grave que je ne le pensais). Malgré tout, si j’ai fait des erreurs, n’hésitez pas pour autant à me le dire quand-même sur ma page de discussion.. — Le message qui précède, non signé, a été déposé par Hibou57 (d · c · b)

Dans "aspect formel" je préfère la définition de modèle comme un triplet ${\displaystyle <U,R,I>}$ où R est un pré-ordre. J'ai donc remplacé ordre par préordre dans l'article.

Il est prouvé dans la référence "Introduction à la logique" que la validité pour les modèles pré-ordonnés est équivalente à celle des modèles ordonnés. De plus dans ce même livre, il est aussi prouvé que si la formule A a un modèle, elle a un modèle fini dont les états sont des sous-ensembles de sous-formules de A, ce qui prouve la décidabilité de la logique intuitionniste propositionnelle. Liviusbarbatus (d) 20 mai 2011 à 09:50 (CEST)Répondre

Je pense qu'il ne faut pas parler de logique modale dans la sémantique mais juste de modèle de Kripke pour les raisons suivantes ː

• ça fait beaucoup de notions à ingurgiter (on vient à peiner de définir la syntaxe et un système de preuve que l'on va déjà plonger ce langage dans un autre ː)... non, non, non)
• j'ai rajouté une sous-section plus tard où je donne la traduction en logique modale explicitement

Bientôt, je vais retravailler la section "sémantique" en ː

• donnant une explication intuitive des mondes possibles dans ce contexte (les étapes dans une démonstration)
• peut-être donner un exemple (quelqu'un en a un sous la main issu de la littérature ?)

--Fschwarzentruber (discuter) 15 avril 2016 à 01:17 (CEST)Répondre

Je suis tout-à-fait d'accord qu'il ne faut pas parler de logique modale. Outre que ça introduit un concept de plus, parler de logique modale ex abstracto n'a pas de sens, car la (une?) logique modale est une extension par une (des) modalité(s) d'une autre logique, or cette autre logique peut être classique ou intuitionniste et l'on fait alors une pétition de principe. OK pour participer à la restructuration de cette section. Quel type d'exemple désires-tu? Je veux bien en proposer un. --Pierre de Lyon (discuter) 15 avril 2016 à 11:54 (CEST)Répondre

Excellent ǃ Alors je propose d'avoir l'exemple tout simple de Semantical Analysis of Intuitionistic Logic I, Saul A. Kripke. Je vais l'ajouter là. Puis je te laisse la main sur la restructuration de la section.--Fschwarzentruber (discuter) 15 avril 2016 à 16:59 (CEST)Répondre

Je te laisse la main. On peut peut-être ajouter aussi un exemple où on voit une structure d'arbre.--Fschwarzentruber (discuter) 15 avril 2016 à 17:08 (CEST)Répondre

Bonjour, je ne comprends pas une phrase de l'article, peut être est ce du à mon faible niveau:

"Kurt Gödel a montré que l'on pouvait représenter la logique classique dans la logique intuitionniste, corroborant le fait que la logique intuitionniste n'est pas une logique à part, mais fait bien partie de la Logique"

Je ne comprends pas bien le sens: Cela veut il dire qu'on peut déduire les mêmes théorèmes finalement en logique intuitionniste qu'en logique classique?

Merci.

--Nicobzz (d) 13 juillet 2011 à 05:46 (CEST)Répondre

Si on prend une formule valide de la logique classique et qu'on la transforme en saturant toutes ses sous formules et elle-même par des doubles négations (exemple : A ou non A transformée en non(non[non non A ou non non non A]) ) on obtient une formule valide de la logique intuitionniste. Pour une transformation un peu plus subtile voir la section Inclusion de la logique classique dans la logique intuitionniste. En ce sens on peut simuler la logique classique dans la logique intuitionniste et la logique classique apparaît comme un cas particulier de la logique intuitionniste ... ce qui est normal car elle a des axiomes en moins et via affirme moins, sachant que le langage est le même. --Epsilon0 ε₀ 13 juillet 2011 à 14:05 (CEST)Répondre

Donc il est possible de traduire un raisonnement par l'absurde de logique classique en logique intuitionniste ? Ou plutôt, cela signifie-t-il que pour toute démonstration par l'absurde, il existe nécessairement une démonstration qui n'utilise pas le raisonnement par l'absurde ? Dans ce thème de l'inclusion, le cas du raisonnement par l'absurde devrait être spécialement traité dans l'article. --Jean-Christophe BENOIST (d) 13 juillet 2011 à 14:14 (CEST)Répondre

Le raisonnement par l'absurde est : non(A) |- Faux, donc A, ou si on préfére |- non(non A) --> A. On ne l'a pas en logique intuitionniste pour toute formule, mais si A est non B, cela nous donne non(non (non B) --> non B qui, sauf erreur, est valide en logique intuitionniste. Donc le raisonnement par l'absurde marche en logique intuitionniste pour certaines formules, mais pour pour toutes. Et à ta question cela signifie-t-il que pour toute démonstration par l'absurde, il existe nécessairement une démonstration qui n'utilise pas le raisonnement par l'absurde ?, la réponse est non : ces 2 logiques sont bien distinctes. Mais intuitivement (si je puis me permettre) on peut côté intuitionniste voir la logique classique comme une logique peu subtile qui s'applique à des formules très particulières. --Epsilon0 ε₀ 13 juillet 2011 à 15:35 (CEST)Répondre

Oups; je m'aperçois que j'avais inversé mentalement l'ordre d'inclusion entre les deux logiques quand j'ai fait ma remarque. A ma décharge, c'est la phrase rapportée par Nico "Kurt Gödel a montré que l'on pouvait représenter la logique classique dans la logique intuitionniste, corroborant le fait que la logique intuitionniste n'est pas une logique à part, mais fait bien partie de la Logique" qui m'a induit en erreur. Si la "logique intuitionniste fait partie de la Logique" (sous-entendu classique) alors l'ordre d'inclusion devrait être LI inclus dans LC. Mais en fait, LC est inclus sans LI. Donc la phrase citée ne me parait pas justifiée : la LI étant plus "vaste" que la LC, elle peut être tout à fait "autre" et ne "fait partie" d'aucune autre logique. --Jean-Christophe BENOIST (d) 13 juillet 2011 à 16:04 (CEST)Répondre

J'ai modifié la phrase de l'introduction en espérant que ce soit plus clair en Kurt Gödel a montré que l'on pouvait représenter la logique classique dans la logique intuitionniste et ceci bien que l'ensemble des formules valides de la logique intuitionniste soit strictement inclus dans l'ensemble des formules valides de la logique classique. Ceci car c'est bien LI qui est incluse dans LC et non l'inverse : on passe de LI à LC en rajoutant des axiomes non déductibles des autres. Mais c'est vrai qu'alors ce codage de LC dans LI paraît très étonnant (je ne vois pas d'équivalent pour exemple dans le domaine que tu connais bien des automates/ machine de Turing). --Epsilon0 ε₀ 13 juillet 2011 à 16:22 (CEST)Répondre

voilà,c ce que je me disais je ne comprenais que LC soit inclus dans LI alors que LC a plus d axiomes. Nicobzz

L'article s'appelle "Logique intuitionniste" et ne parle que d'elle. Donc j'aime le titre. Mais le paragraphe introductif et la section "Approche informelle" parle d'intuitionnisme. Quid de faire une introduction qui présente la logique intuitionniste et qui parle d'intuitionnisme. Puis la première section peut s'appeler "Intuitionnisme". Je n'aime pas le titre "Approche informelle"... il n'y a jamais eu d'approche informelle. C'est bizarre. En plus, la section contient des formules. J'ai même supprimé des symboles peu connus par le lecteur non connaisseur comme la négation etc. Qu'en pensez-vous ? --Fschwarzentruber (discuter) 12 avril 2016 à 19:39 (CEST)Répondre

Il est vrai que le paragraphe "approche informelle" appartient plus à intuitionnisme qu'à cet article. Et on peut en effet donner une approche "intuitive" de l'intuitionnisme.--Jean-Christophe BENOIST (discuter) 12 avril 2016 à 20:30 (CEST)Répondre

La section (que j'ai déplacé dans la section "Comparaison") est bien sauf que ː

• Elle parle surtout de loi de Morgan etc. → il faut un titre plus clair. On compare ici les validités (ou les théorèmes)
• Je trouve que ça serait plus simple avec un tableau comme j'ai fait pour la section "Syntaxe" (qui manquait car ce n'était pas clair comment lire les formules de la logique intuitionniste en lisant l'article). Je vois bien un tableau avec deux colonnes. Le monde classique et le monde intuitionniste.

Qu'en pensez-vous ?--Fschwarzentruber (discuter) 12 avril 2016 à 21:26 (CEST)Répondre

La sous-section "Exemples de différences avec la logique classique" est assez complète mais confuse. Je n'ai pas encore supprimé la sous-section. Je préfère avoir votre avis. Au lieu de cela, je vous propose un tableau (placé dans la sous-section).

"Les opérations ne sont pas définies l’une par rapport à l’autre (voir plus loin), et ne sont définies qu’en elles-mêmes." => j'ai rajouté une section non-interdéfinissabilité dans "Syntaxe". C'est un point trop important ː il vaut mieux annoncer la couleur au début. " ne sont définies qu’en elles-mêmes." n'est pas très clair.

J'ai présenté la lecture intuitive dans la syntaxe (appelée "interprétation" dans l'article). Je n'aime pas trop le mot "interprétation" car cela fait penser aux modèles. Là aussi, savoir lire les formules d'une logique intuitivement, c'est hyper crucial et ça vient trop tard dans l'article.

On ne peut pas conclure que A \Leftrightarrow \lnot \lnot A est vrai. => vrai... au sens valide. La sous-section utilise trop souvent le mot "vrai" pour "prouvable".

Je trouve les exemples avec des nombres réels très confus. La logique intuitionniste ne parle pas de nombres réels. Je préfère des exemples plus "simplets".

Le découpage en sous-section est flou. Par exemple, "conjonction" ou "disjonction" parle tous les deux de "ou" et de "et".

--Fschwarzentruber (discuter) 15 avril 2016 à 00:39 (CEST)Répondre

Je ne comprends rien aux tableaux, qui n'expliquent rien et disent des choses fausses. Je serais même pour supprimer l'ensemble de la section intitulée Exemples de différences avec la logique classique sauf le premier paragraphe qui est essentiel. La différence entre la logique classique et la logique intuitionniste ne réside pas dans le fait que la première aurait à voir avec le « vrai » tandis que la seconde aurait à voir avec le « démontrable ». Il y a un système de déduction en logique classique donc une notion de démontrable. Il y a des modèles en logique intuitionniste donc une notion de validité donc de « vérité ». --Pierre de Lyon (discuter) 15 avril 2016 à 16:47 (CEST)Répondre

Est-ce qu'en 2016, la modalité « nécessité » ou « nécessairement » (écrite □) ne devrait pas être renommée « constructivement » ? Je trouve que nécessité fait un peu ringard. --Pierre de Lyon (discuter) 15 avril 2016 à 13:03 (CEST)Répondre

□A se lit "nécessairement A est vraie" en logique modale aléthique. J'ai l'impression que les gens disent aussi "nécessairement A est vraie" (histoire de dire quelque chose) quand l'opérateur □ est abstrait. Ici, je suis d'accord avec vous ː □ n'est pas abstrait. Dans la traduction de la logique intuitionniste en logique modale S4, □A se lit, "A est prouvable" (cf. http://plato.stanford.edu/entries/goedel/#IntProLogIntS4). Je pense qu'on devrait dire ça. J'ai placé la traduction vers la fin de l'article. Je pense que la sémantique de la logique intuitionniste peut être expliquée sans faire référence à la logique modale (par soucis de simplicité). --Fschwarzentruber (discuter) 15 avril 2016 à 13:43 (CEST)Répondre

J'ai ajouté un bandeau travail inédit au paragraphe la question du tiers-exclus. Cependant, ça n'est pas seulement inédit, c'est aussi faux. Ce n'est pas la négation qui est différente en logique intuitionniste par rapport à la logique classique, ce sont tous les connecteurs et j'aurais envie de dire, tous les connecteurs sauf la négation. Je propose que ce paragraphe soit supprimé, sauf si quelqu'un souhaite le maintenir. Dans ce cas cette personne devra en améliorer la rédaction pour le rendre compréhensible et le sourcer. --Pierre de Lyon (discuter) 15 avril 2016 à 16:17 (CEST)Répondre

J'ai lu le paragraphe la question du tiers-exclus et je n'y comprends rien. Il y a trop de phrases vagues comme "après tout, des similitudes syntaxiques n’indiquent pas nécessairement des similitudes sémantiques" ou "son interprétabilité est faible.". Je préconise ː

• comme vous dîtes, la suppression de ce paragraphe (en plus l'explication du tiers-exclu est CRUCIALE et est faite dans l'introduction... il vaut mieux laisser la fin de l'article pour des choses plus spécialisées)
• améliorer éventuellement l'explication du début
• améliorer la section "Syntaxe" (la logique intuitionniste propositionnelle et la logique classique propositionnelle ont exactement la même syntaxe)
• améliorer les lectures intuitives données dans la section "Syntaxe" (je ne suis pas d'accord que la négation est la même en classique et intuitionniste car elle est définie comme une macro à partir de l'implication qui est différente... mais oui, cette macro est la même)

--Fschwarzentruber (discuter) 15 avril 2016 à 16:30 (CEST)Répondre

Il n'y a pas de notion de temps dans les modèles de Kripke de la logique intuitionniste. Comme il est dit c'est une modèle de mondes possibles. Je propose donc d'enlever toute référence au temps. --Pierre de Lyon (discuter) 18 avril 2016 à 10:25 (CEST)Répondre

Je cite Saul Kripke (https://www.princeton.edu/~hhalvors/restricted/kripke_intuitionism.pdf) où il y a écrit p. 98 ː

• "has been verified at the point H in time". has not been verified"
• "Now given a point in time G"
• "for an arbitrary long time without gaining any new information"

C'est une explication intuitive cependant qui aide à comprendre la sémantique je trouve et je suis assez d'accord avec Kripke. A discuter. ː) Bonne journée à toi. --Fschwarzentruber (discuter) 18 avril 2016 à 10:47 (CEST)Répondre

Oui mais Kripke écrivait il y a un demi siècle. En 2016, il a beaucoup coulé d'eau sous les ponts. C'est précisément, parce que ça ne m'aide pas à comprendre que je propose d'enlever cette référence au temps. --Pierre de Lyon (discuter) 18 avril 2016 à 10:57 (CEST)Répondre

De ce que j'en ai compris, cette relation de préordre, pour Kripke, c'est le "temps" dans le sens où, si m --> m', l'(unique) agent a fourni des efforts pour aller de m à m' et a obtenu plus d'informations. On ne peut pas perdre d'informations (si p vrai dans m, alors p vrai dans m'). Donc pour moi, ça m'aide à comprendre. Mais, là où je vous rejoins, c'est que ça peut induire en erreur d'autres personnes. Et de deux, même si Kripke est l'inventeur des modèles de Kripke, il n'a pas forcément raison et ce n'est pas forcément l'unique façon de voir ces modèles. Personnellement, je suis pour parler du temps mais sous la forme "Pour Kripke, "... "Kripke pense que..." (et la référence) afin d'être le plus impartial possible. Bonne journée.

--Fschwarzentruber (discuter) 18 avril 2016 à 14:24 (CEST)Répondre

En principe il faudrait, pour trancher ce genre de questions, se référer à une source qui présente et commente les modèles de Kripke (une source secondaire), que sur Kripke lui-même (source primaire). Plus généralement, le paragraphe "Modèle de Kripke" manque de sources (secondaires !) et de vérifiabilité, au moins sur la démarche et la manière de présenter ces modèles, ce qui est précisément l'objet de votre débat. Cordialement --Jean-Christophe BENOIST (discuter) 18 avril 2016 à 17:46 (CEST)Répondre

Je suis complétement d'accord pour rajouter des sources secondaires. Bonne journée.--Fschwarzentruber (discuter) 18 avril 2016 à 17:51 (CEST)Répondre

Le livre de Karim Nour et al Introduction à la Logique, Théorie de la démonstration (2001) dit, je cite (p. 159) ː "l'ensemble |K| (des mondes) modélisent le temps, <= l'ordre sur le temps et alpha |= A signifie que A est vraie à l'instant alpha." --Fschwarzentruber (discuter) 18 avril 2016 à 21:47 (CEST)Répondre

Je serais favorable qu'on garde la notion de temps comme une possibilité d'interprétation laissée à l'appréciation du lecteur qui trouve cela utile comme aide à sa compréhension des modèles de Kripke (c'est personnellement mon cas et j'ai la même référence que ci-dessus), sans que cela soit pour autant indispensable. Theon (discuter) 19 avril 2016 à 17:12 (CEST)Répondre

Personnellement, je comprends mieux aussi avec le temps. Et c'est même du temps branché (c'est à dire qu'il y a plusieurs futurs possibles selon comment l'agent fournit l'effort pour "apprendre de nouvelles informations". Mais je comprends Pierre Lescanne et wikipedia ne doit pas prendre parti ː s'il existe des références où le temps n'est pas mentionné, on peut aussi le mentionner.--Fschwarzentruber (discuter) 19 avril 2016 à 18:17 (CEST)Répondre

Je pense que la phrase « il pleut ou il ne pleut pas » est désastreuse comme exemple, d'autant plus qu'elle figure au tout début de l'article. En effet, elle est décidable. N'importe qui de sensé qui se promène pourra répondre « Oui il pleut » ou « Non il ne pleut pas ». Donc le tiers exclu peut être appliqué à une telle proposition. En revanche une phrase comme « Omar m'a tuer ou Omar ne m'a pas tuer » ou « Christian Ranucci a tué Marie-Dolorès Rambla ou Christian Ranucci n'a pas tué Marie-Dolorès Rambla » sont certes plus polémiques, mais ne sont pas décidables et seraient des exemples plus convaincants. L'intime conviction n'est pas la décision. --Pierre de Lyon (discuter) 11 mai 2016 à 12:21 (CEST)Répondre

On peut trouver un phrase plus anodine Dan Cole a marqué un essai ou Dan Cole n'a pas marqué d'essai. --Pierre de Lyon (discuter) 11 mai 2016 à 12:25 (CEST)Répondre

Je suis favorable pour le remplacement de l'exemple. --Fschwarzentruber (discuter) 11 mai 2016 à 12:35 (CEST)Répondre

Moi aussi, mais je me pose des questions. Je me demande si la faiblesse de ces exemples ne vient pas du fait qu'il s'agit d'un événement individuel, unique, qui peut être - plus ou moins aisément, mais ce n'est pas fondamental - falsifiable/vérifiable. "Omar m'a tuer" ne me semble pas fondamentalement différent de "il peut ou pas", ce n'est qu'une question de difficulté de vérification. Un bon exemple d'énoncé qui peut être indécidable serait-il pas plutôt "le soleil se lève tous les jours", qui référence un nombre infini d'événements ? L'indécidabilité ne concerne-t-il pas toujours, directement ou indirectement, une classe infinie d'objets ? L'indécidabilité du problème de l'arrêt, de P=NP etc.. sont tout à fait de ce genre. Même l'indécidabilité de l'axiome du choix concerne un ensemble infini d'ensembles non vides. --Jean-Christophe BENOIST (discuter) 11 mai 2016 à 13:16 (CEST)Répondre

C'est aussi mon point de vue, que l'indécidabilité concerne seulement des exemples mathématiques. J'ai cité des exemples liés à la décision d'un juge ou d'un arbitre, pour respecter le désir de l'auteur de cette phrase de donner un exemple de la vie courante (peut-être une fausse vie courante ). --Pierre de Lyon (discuter) 11 mai 2016 à 13:58 (CEST)Répondre

Pour construire l'exemple, il nous faut une conjecture non prouvée C. "C ou non C" fait office d'exemple.

* Ainsi, C = "il pleut" est un peu tiré par les cheveux car il faut que la personne n'est pas regardé par la fenêtre... (bref, l'exemple n'est pas convaincant du tout).

* Je pense qu'un exemple juridique n'est pas si mal. Si une affaire juridique C, comme C = "Christian Ranucci n'a pas tué Marie-Dolorès Rambla" n'est pas élucidée, alors C n'est pas prouvable jusqu'alors, "non C" non plus. Du coup, "C ou non C" fait office d'exemple.

* Dans une version antérieure, il y avait l'exemple ""Il existe des nombres irrationnels a et b, tels que a^b est un nombre rationnel"". Il repose sur le tiers-exclu "sqrt 2 ^{sqrt 2}" rationnel ou sqrt 2 ^{sqrt 2}" irrationnel". Mais l'humanité a démontré que "sqrt 2 ^{sqrt 2}" irrationnel" donc l'exemple n'est pas génial.

* Mais :), http://plato.stanford.edu/entries/logic-intuitionistic/#RejTerNonDat donne l'exemple C = "il existe une infinité de nombres premiers jumeaux". Qu'en pensez-vous ?

--Fschwarzentruber (discuter) 11 mai 2016 à 14:16 (CEST)Répondre

Mathématique, sourçable, c'est tout bon. Ou la conjecture de Syracuse ? mais on n'a pas répondu à mon interrogation si l'indécidabilité concerne toujours des classes infinies d'objets. C'est le cas pour C envisagé en tout cas. --Jean-Christophe BENOIST (discuter) 11 mai 2016 à 14:55 (CEST)Répondre

OK pour la conjecture des nombres jumeaux ou pour celle de Syracuse. D'autre part, (en agitant les mains) si l'égalité sur un ensemble satisfait le tiers-exclus, alors la dite égalité est décidable ; or les ensembles finis sont décidables, donc pour qu'il n'y ait pas de tiers exclus, il faut que les ensembles soient infinis. Voir par exemple le Coq'art page 286.--Pierre de Lyon (discuter) 12 mai 2016 à 14:53 (CEST)Répondre

Merci pour la réponse, il me semblait bien. Cordialement --Jean-Christophe BENOIST (discuter) 12 mai 2016 à 16:04 (CEST)Répondre

« il pleut ou il ne pleut pas » est essentiellement indécidable car prouver cela c'est (formellement) : déterminer en toute circonstance s'il peut ou non. Rien n'est décidable si les objets dont il est question n'ont pas un caractère inductif. Pas de définition inductive de la pluie ; donc, pas de preuve possible.   <STyx @ (en long break)

Le 3ème § de la section histoire ("Elle a été ensuite formalisée, sous le nom de logique intuitionniste") est mal rédigé:

• Il y a un "Godel et Kolmogorov." qui n'est relié à rien; je présume que l'auteur voulait dire "Elle a été ensuite formalisée, sous le nom de logique intuitionniste, par ses élèves V. Glivenko et Arend Heyting ainsi que Kurt Gödel et Andreï Kolmogorov." (ces 2 sus-mentionnés ne sont pas des élèves de Brouwer).
• La section sur l'implication matérielle serait sans doute mieux à une autre place (peut-être après le 1er § de cette section).

--Duboismathieu gaas (discuter) 31 décembre 2017 à 00:06 (CET)Répondre

vu par Theon   <STyx @ (en long break) 8 janvier 2018 à 18:12 (CET)Répondre

 STyx : Vous avez fait une correction avec le commentaire « La logique implicative "minimale" : non-sens : c'est aussi stupide que de parler de serpent tétraplégique ». Vous avez ajouté un lien en anglais qui n'est pas la traduction de ce qui est écrit en français. Pourriez-vous nous expliquer votre point de vue sur la page de discussion ? --Pierre de Lyon (discuter) 10 janvier 2018 à 18:27 (CET)Répondre

• "minimal" c'est un terme (trop) vague. Si on entend par là "langage minimal", alors "implicatif minimal" est un pléonasme (mais bon, c'est le même problème que pour le mot "fonction" : on en vient à parler de "fonction partiel" parce que le mot "fonction" est trop souvent (toujours! en informatique) employer pour désigner une '"application"); si l'on comprend "sans l'exfalso" alors voici une excellente analogie : logique = animal, ⊥ = pattes, donc implicatif=sans patte ; exfalso =l'usage des pattes, donc : minimal=tetraplegique.
• euh ! tu veux dire  : Vous avez ajouté un lien en anglais qui serait la traduction de ce qui n'est écrit pas en français : logique implicative.   <STyx @ (en long break) 11 janvier 2018 à 15:13 (CET)Répondre

Dans Introduction à la logique - Théorie de la démonstration, de Nour, et al., ils mentionnent bien la logique minimale p. 147. Je propose de ne pas supprimer brutalement la mention "logique minimale", mais de dire "Certains auteurs (ref à Nour et al.), ça s'appelle "logique minimale", puis "pour d'autres auteurs (mettre une ref), elle est appelée logique implicative". Bonne soirée. Fschwarzentruber (discuter) 11 janvier 2018 à 18:11 (CET)Répondre

D'accord avec logique minimale ! ... mais pas avant d'avoir introduit ⊥ sinon cela n'a pas de sens .   <STyx @ (en long break) 11 janvier 2018 à 19:24 (CET)Répondre

L'article est mal structuré ! La partie contructive (i.e. la correspondance de Curry-Howard) n'est pas exposée ! Vue la complexité du sujet une section "Introduction" (un résumé introductif comme dans tout article ou livre scientifique). Cela permettrait de mettre en évidence l'essentielle de la section. Par exemple : « Les Logique intuitionniste#Modèles de Kripke fournissent un moyen infaillible de démontrer qu'une proposition n'est pas démontrable ». Cela permettrait aussi de replacer ce que j'ai mis en commentaire ... avec des liens interne cette fois.

• Logique intuitionniste#Syntaxe du langage de la logique intuitionniste ne parle nullement de syntaxe ; mais de sémantique. !
• Logique intuitionniste#Non-interdéfinabilité des opérateurs à supprimer : c'est vague, mal dit, et fait doublon (voire "triplon" :) ) avec le reste
• Logique intuitionniste#Traduction en logique modale classique a plus sa place dans Logique intuitionniste#Sémantique de la logique intuitionniste
• Logique intuitionniste#Inclusion de la logique classique dans la logique intuitionniste : je préfère "non-non-traduction" ... mais bon
• Logique intuitionniste#Exemples de différences avec la logique classique : pfff! des tonnes ... et cela fait doublon ! ... pourquoi pas une simple liste de tautologies indécidables

A rajouter

• Théorème de Glivenko
• Heyting
• « Notons à ce propos qu'il existe, entre la logique intuitionniste et la logique classique, une infinité de logiques intermédiaires, plus fortes que la logique intuitionniste et plus faibles que la logique classique. » : à développer !
• Il faudrait également formuler (plus clairement que moi) des choses comme « pierce, tiers-exclu, ¬¬P→P, ..., (${\displaystyle ((p\Rightarrow q)\Rightarrow r)\Rightarrow ((q\Rightarrow p)\Rightarrow r)\Rightarrow r}$, einstein : (P→Q)∨(Q→P) ??) sont equivalentes/interchangeables »

etc.   <STyx @ (en long break) 11 janvier 2018 à 18:57 (CET)Répondre

D'accord à peu près avec tout. Mais la section Syntaxe présente bien la syntaxe, c'est-à-dire les constructions du langage et comment on les lit à haute voix en français. La sémantique est donnée dans la section "Sémantique". Fschwarzentruber (discuter) 11 janvier 2018 à 19:02 (CET)Répondre

le "Syntaxe du" est superflu (la syntaxe traite, à mon sens, de l'agencement des symboles) ... et le tableau donne "le sens de ..." (donc sémantique) et se contente de remplacer "vrai" par "prouvable" ... Enfin, il y a Logique intuitionniste#Relations avec la logique classique ou l'on compare encore abondamment les deux logiques.   <STyx @ (en long break) 11 janvier 2018 à 19:18 (CET)Répondre

Je propose de supprimer la section « Quelques validités » à laquelle je ne comprends rien. --Pierre de Lyon (discuter) 22 mars 2019 à 09:26 (CET)Répondre

Je ne suis pas emballé par les explications de cette section. Par contre, il me paraît utile de garder la liste des exemples de la première colonne, qui permet d'illustrer la différence entre logique classique et intuitionniste. Il conviendrait alors de voir quelle forme prendraient les deux colonnes de droite : les conserver en reformulant certaines explications ? les supprimer en les remplaçant par un commentaire ? Theon (discuter) 23 mars 2019 à 07:58 (CET)Répondre

Le tableau, que j'ai mis du temps à comprendre, explique, ou tente d'expliquer, pourquoi

• quand dans la colonne 1 on a une formule de la forme A <==> B, A ==> B marche (colonne 2) et B ==> A marche (colonne 3).
• quand dans la colonne 1 on a une formule de la forme A ==> B, A ==> B marche (colonne 2) et B ==> A ne marche pas (colonne 3) … alors qu'il marche en logique classique.

Bref je trouve que ce tableau est une bonne idée mais manque de présentation et pêche un peu par ses explications. Qu'on le garde en l'améliorant ou pas, le point le plus important, me semble t-il, est de marquer les validités classiques qui ne sont pas intuitionnistes, soient, en creux dans ce tableau :

• ${\displaystyle \lnot \lnot A\Rightarrow A}$
• ${\displaystyle \lnot (A\land B)\Rightarrow (\lnot A)\lor (\lnot B)}$
• ${\displaystyle (A\Rightarrow B)\Rightarrow ((\lnot A)\lor B)}$ <-- En passant, je ne savais pas que ce n'était pas intuitionniste. Pouvez-vous confirmer ?
• ${\displaystyle \lnot (\forall xA(x))\Rightarrow \exists x(\lnot A(x))}$

--Epsilon0 ε₀ 24 mars 2019 à 00:34 (CET)Répondre

 Epsilon0 : c'est immédiat, on obtient (EM) en prenant A=B ;)   <STyx @ (en vadrouille) 24 mars 2019 à 04:47 (CET) Oui ;-) merci. (EM = excluded middle) --Epsilon0 ε₀ 24 mars 2019 à 11:45 (CET) Répondre

• Je suis pour un tableau ... mais pas celui-là. ${\displaystyle \vdash A\Rightarrow B}$ est une relation ordre ${\displaystyle A\geq B}$ entre formules closes. On n'a plus 2 classes d'equ. (comme en logique classique) ni 3 ... mais une infinité ! Ce qui m'interresse ; ce serait de faire une ébauche de cette hiérarchie (notamment ⊥>(EM)=(Pierce)=(NNPP)>(weak excluded middle)> etc. >⊤= etc.). cf. en:Intermediate logic
• appeler "explication" une reformulation de l'énoncé, quelle foutaise ! Je propose un fichier coq pour ce qui est prouvable directement (ie. sans M. de Kripke) et des colonnes pour la désignation/lien, valeur de Heyting.

Voilà un extrait d'une de mes vieilleries   <STyx @ (en vadrouille) 24 mars 2019 à 04:47 (CET)Répondre

(*
-  1: [ P \/ ~ P ]  (EM)=(E3)
-  2: [ ~~P -> P ]  (NNPP)
-  3: [ (~P -> P) -> P ]
-  4: [ (~Q -> ~P) -> (P -> Q) ]
-  5: [ ((P -> Q) -> P) -> P ]  (Pierce)
-  6: [ ~~(P \/ ~ P) ]
-  7: [ (P -> Q) -> ( Q \/ ~P ) ]
-  8: [ ~~(P \/ ~ P) -> (P \/ ~P) ]
-  9: [ ~ P \/ ~~P ] (EM ~P) (weak excluded middle) (principle of testability) (Jankov logic (KC))
- 10: [ (~Q -> P) -> (Q -> P) -> P ]
- 11: [ (~Q -> P) -> (~~Q -> P) -> P ]
- 12: [ ~~(~~P -> P) ]
- 13: [ (P -> Q) \/ (Q -> P) ]  (Einstein) (Gödel–Dummett)
- 14: [ (~Q ↔ P) -> (Q ↔ ~P) ]
- 15: [ ( ( (((P->Q) -> P) -> P) -> R ) -> ((P->Q) -> P) -> P ) -> ((P->Q) -> P) -> P  ]  (Pierce Pierce)
- 16: [ ((P->Q) -> R) -> ((Q->P) -> R)  -> R ]
- 17: [ P \/ ~ P \/ (P <-> forall Q:Prop, Q \/ ~ Q) ] (E4)
- 18: [ (~~ (~~P -> P)) ->  ~~P -> P ] (NNPP NNPP)
- 19: [(~P->Q)->(~Q->P)] undecidable
- 20: [~(P/\Q)->(~P\/~Q)] undecidable
- 21: [P->~P->Q] true
- 22: [ ((~P -> Q) -> ~P) -> ~P ]  (Pierce ~)
- 23: [ ((~~P -> P) -> (P\/~P)) -> (~P\/~~P) ]  (Scott axiom)
- 24: [ (~P -> (Q\/R)) -> ((~P->Q)\/(~P->R)) ]  (Kreisel-Putnam axiom)
- 25: [ (~Q -> P) -> ((P->Q)->P)->P ]  (Smetanich axiom)
- 26  [ (P -> Q) -> (~P \/ Q) ]

Equivalences établies :
 - true:  6 == 12 == 21 == 22 (démontrables en logique intuitionniste)
   (note (theorem de Glivenko) : toute tautologie classique de la forme [~F] est démontrable en log. int.)
 - undecidable: 1 == 2 == 3 == 4 == 5 == 7 == 8 == 10 == 14 == 18 == 26 (valeur de Heyting 1/2)
 - undecidable : 13 == 16
 - undecidable: 9 == 11  (valeur de Heyting 1)
 - 1-> 13 -> 9
 - 5 -> 15
 - 17 -> 9
*)

• Je viens de découvrir coq online ;)) ! Pour de vrais explications, il suffit de tester ... par exemple ceci :   <STyx @ (en vadrouille) 24 mars 2019 à 16:43 (CET)Répondre

Require Import Coq.Unicode.Utf8.
Definition excluded_middle : Prop := ∀ P:Prop, P ∨ ¬ P.
(** [¬¬]-elimination ([NNPP]) *)
Definition NNPP:Prop := ∀ P:Prop, ¬¬P → P.

(** preuve initiale (human style) *)
Lemma NNPP_em__ :  NNPP → excluded_middle.
Proof.
unfold NNPP.
intros NNPP P.
assert( H: (¬¬(P ∨ ¬P) → (P ∨ ¬P)) →  (P ∨ ¬P) ).
intro HP. apply HP. intro NPP.
assert ( H': ¬P → ¬¬¬P ).
intros NP NNP. apply NNP. exact NP.
apply H'. clear H'.
intros P_. apply NPP. apply or_introl. exact P_.
intro NP. apply NPP. apply or_intror. exact NP.
apply H. apply NNPP.
Qed.
(** On obtient un terme (utiliser [Print NNPP_em__.]) assez immonde, 
du au fait que l'on raisonne naturellement "des hypothèses au but" 
à l'aide de lemmes intermédaires (tactique [assert]).
Après suppression des [let], remise en ordre (béta-reduction), et omission des types ; 
cela donne : *)
Definition NNPP_em_ :  NNPP → excluded_middle :=
fun NNPP P => NNPP (P ∨ ¬P) (fun NEM => (NEM (or_intror (fun P_ => NEM (or_introl P_))))).
(** ... qui est le resultat de la preuve finale (coq (/CoC) style) suivante : *)
Lemma NNPP_em :  NNPP → excluded_middle.
Proof. unfold NNPP. intros NNPP P. apply NNPP. intro NEM. apply NEM. right. intro P_. apply NEM. left. exact P_. Qed.
(** donc, si l'on admet que [excluded_middle] n'est pas démontrable, [NNPP] ne l'est pas non plus *)

 Remsirems : Pour décider de la rationalité de la constante d'Euler Mascheroni, il faut ou bien une démonstration constructive de sa rationalité, ou bien une démonstration constructive de son irrationalité. Il faudrait reformuler l’introduction dans ce sens, si vous le souhaitez. Pour l’instant la formulation actuelle est préférable. --Pierre de Lyon (discuter) 30 juin 2019 à 12:23 (CEST)Répondre

 PIerre.Lescanne : Je ne suis pas sûr de comprendre votre point de vue. Le problème de la formulation actuelle n'est pas qu'elle manque de clarté; c'est qu'elle est fausse! En effet, affirmer qu'il n'est pas démontrable (constructivement s'entend) que « la constante d'Euler-Mascheroni est rationnelle ou la constante d'E.-M. est irrationnelle », c'est affirmer qu'il n'existe pas, dans l'absolu, ni de démonstration qu'elle soit rationnelle, ni de démonstration qu'elle soit irrationnelle. Or tout ce que nous savons, c'est que, à l'heure actuelle, nous n'avons trouvé de démonstration ni dans un sens ni dans l'autre: mais nous n'avons aucune preuve que nous ne pourrons jamais en trouver…!

Ce qui est vrai, c'est que pour une proposition générique ${\displaystyle P}$, on ne peut pas montrer en logique intuitionniste la proposition ${\displaystyle (P\ {\text{ou}}\ \neg P)}$. Mais la phrase précédente est un théorème, et pas juste une conséquence directe des règles de l'intuitionnisme: j'entends par là qu'il y a une preuve (pas facile au demeurant) qu'aucun raisonnement intuitionniste ne permettra de conclure à ${\displaystyle (P\ {\text{ou}}\ \neg P)}$…

Cependant, lorsqu'on considère une proposition ${\displaystyle P}$ fixée (disons, « ${\displaystyle 1+1=2}$ », il se peut très bien que ${\displaystyle (P\ {\text{ou}}\ \neg P)}$ soit prouvable (en l'occurrence c'est le cas, puisqu'on a une preuve de ${\displaystyle P}$. Dans le cas de la constante d'E.-M., on ne sait pas si notre ignorance sur la rationalité ou non de ${\displaystyle \gamma }$ provient de ce que c'est un indécidable (autrement dit, on n'a pas trouvé de preuve parce qu'il n'y en existe pas) ou de ce qu'on n'a simplement pas encore assez bien cherché…

La formulation de l'introduction actuelle pourrait être valide si on remplaçait la rationalité de la constante d'E.-M. par une affirmation connue pour être indécidable. Le problème, c'est que les indécidables de la logique classique ne sont pas nécessairement indécidables en logique intuitionniste, de sorte que je n'ai aucun exemple à proposer…

Au vu de ce qui précède, je vous recommande donc de ré-intégrer mes modifications, quitte à les amender sous une forme que vous trouviez plus claire. Mais en tout état de cause, on ne peut pas laisser une affirmation fausse sur WP au motif qu'elle serait plus facile à comprendre qu'une affirmation erronée…

Cordialement, Remsirems (discuter) 30 juin 2019 à 16:31 (CEST)Répondre

Je pense qu'il faut une source. Gilles Dowek donne l'exemple "le général a tué le chauffeur ou le général n'a pas tué le chauffeur" p. 81 dans Gilles Dowek - la logique, aux éditions Poche - Le Pommier!. Y-a-t-il une source pour l'exemple de la constante d'E.-M ? Merci et bonne soirée. Fschwarzentruber (discuter) 30 juin 2019 à 21:14 (CEST)Répondre

Vous dites « Ce qui est vrai, c'est que pour une proposition générique P, on ne peut pas montrer en logique intuitionniste la proposition ( P ou ¬ P ). Mais la phrase précédente est un théorème, et pas juste une conséquence directe des règles de l'intuitionnisme: j'entends par là qu'il y a une preuve (pas facile au demeurant) qu'aucun raisonnement intuitionniste ne permettra de conclure à ( P ou ¬ P )… » ; Pourriez-vous être plus précis, je ne comprends pas ce que vous voulez dire. Plus précisément qu'entendez-vous par

• phrase précédente
• pas facile au demeurant.

--Pierre de Lyon (discuter) 30 juin 2019 à 21:51 (CEST)Répondre

Pierre de Lyon. « Phrase précédente » désignait l'affirmation suivante: « Pour ${\displaystyle P}$ une proposition dont on ne sait rien, si ce n'est que c'est une proposition, il n'existe pas de preuve en logique intuitionniste de ${\displaystyle (P\ {\text{ou}}\ \neg P)}$ ».

Il est important de réaliser que l'inexistence affirmée par la phrase ci-dessous n'est pas facile à montrer! En effet, le simple fait qu'on n'ait pas le droit d'utiliser l'axiome « ${\displaystyle P\ {\text{ou}}\ \neg P}$ » en tant que règle de la logique n'exclut pas, à priori, qu'on puisse quand même le démontrer par le biais d'un raisonnement plus compliqué! Il se trouve cependant que, dans le cas d'une proposition ${\displaystyle P}$ générique, il est bel et bien exact qu'aucun raisonnement de logique intuitionniste, aussi alambiqué soit-il, ne permettra jamais de montrer ${\displaystyle (P\ {\text{ou}}\ \neg P)}$. Mais la preuve de cette affirmation est trop compliquée pour être donnée dans ces quelques lignes…

Maintenant, si on considère une proposition ${\displaystyle P}$ particulière, comme « la constante d'E.-M. est rationnelle », il y a à priori plusieurs cas possibles:

• On sait prouver (en logique intuitionniste) ${\displaystyle P}$, ou on sait prouver ${\displaystyle \neg P}$, et donc on sait prouver ${\displaystyle (P\ {\text{ou}}\ \neg P)}$;
• On sait qu'il existe une preuve en logique intuitionniste de ${\displaystyle (P\ {\text{ou}}\ \neg P)}$, mais on ne connait néanmoins pas, à l'heure actuelle, cette preuve (ce cas est paradoxal, mais il se produit, par exemple, si ${\displaystyle P}$ est l'affirmation « le ${\displaystyle 10^{10^{10}}}$-ième chiffre de ${\displaystyle \pi }$ est un ‘7’ » : dans ce cas, un calcul suffisamment long permettra de savoir quel est le chiffre en question et donc d'avoir une preuve intuitionniste, soit de ${\displaystyle P}$, soit de ${\displaystyle \neg P}$ ; mais personne n'a jamais mené à bien ce calcul qui est bien au-delà de nos moyens actuels.
• On ignore, à l'heure actuelle, si la proposition ${\displaystyle (P\ {\text{ou}}\ \neg P)}$ est prouvable en logique intuitionniste ou non (c'est la situation, autant que je sache, concernant la rationalité de la constante d'Euler-Mascheroni);
• On a une preuve qu'aucun raisonnement de logique intuitionniste de permettre jamais de conclure à ${\displaystyle P}$ ni à ${\displaystyle \neg P}$, et donc (il se trouve que c'est équivalent en logique intuitionniste) qu'aucun raisonnement de logique intuitionniste ne permettra jamais de montrer ${\displaystyle (P\ {\text{ou}}\ \neg P)}$;
• Non seulement on est dans le cas précédent, mais en plus, notre preuve est valide dans le cadre de la logique intuitionniste : ce qui signifie alors qu'on dispose d'une preuve, en logique intuitionniste, de ${\displaystyle \neg (P\ {\text{ou}}\ \neg P)}$. (Attention, je ne suis pas 100 % sûr de moi sur ce dernier item).

Idéalement, il faudrait remplacer la rationalité de la constante d'E.-M. par une proposition rentrant dans un des deux derniers cas ci-dessous. Mais je pense que l'introduction y perdrait en clarté… Il me semble donc plus pertinent d'écrire quelque chose comme « alors qu'il est trivial, pour la logique classique, que l'affirmation “γ est rationnelle ou γ est irrationnelle” est correcte, en logique intuitionniste au contraire, il est tout à fait envisageable qu'une telle proposition soit fausse ! (et de fait, à l'heure de 2013, on ne connait en tout cas aucune preuve intuitionniste de “γ est rationnelle ou γ est irrationnelle“) ».

Cordialement, Remsirems (discuter) 30 juin 2019 à 22:54 (CEST)Répondre

Tout d'abord, en logique intuitionniste, on sait (c'est assez facile à (méta)démontrer une fois que l’on a la correction de la logique par les modèles de Kripke) que P ∨ ¬P n'est pas un théorème, ou dit autrement, qu'il n'y a pas de démonstration de P ∨ ¬P. En effet, il y a un modèle de Kripke qui ne valide pas P ∨ ¬P.

Il me semble que vous ne connaissez pas un point fondamental de la logique intuitionniste concernant le connecteur ∨. En logique intuitionniste, pour que l'on ait une démonstration de P ∨ Q, il faut que l’on ait une démonstration de P ou que l’on ait une démonstration de Q. Si nous appliquons cela à la proposition REM qui signifie que la constante Euler-Mascheroni est rationnelle et à sa négation, pour avoir une démonstration de REM ∨ ¬ERM, il faut que l'on ait ou bien démonstration de REM ou bien une démonstration de ¬ERM, or le 3 juillet 2019, nous n'avons aucune de ces deux démonstrations. Donc nous n'avons pas de démonstration de ERM ∨¬ERM. --Pierre de Lyon (discuter) 3 juillet 2019 à 08:47 (CEST)Répondre

 PIerre.Lescanne : En effet, je ne suis pas expert du domaine… Mon point principal était simplement de souligner que l'affirmation « la rationalité de la constante d'Euler-Mascheroni n'est pas démontrable en logique intuitionniste » n'est pas un résultat des mathématiques d'aujourd'hui et ne pouvait donc pas figurer dans l'introduction d'une page Wikipédia. La nouvelle version de la page, en revanche, règle ce souci de façon parfaitement satisfaisante. Merci donc pour votre aide ! :-) Cordialement, Remsirems (discuter) 3 juillet 2019 à 18:09 (CEST)Répondre

Bonjour,

je voudrait soulever ce qui me semble une erreur et qui amène à des difficulté de compréhension voir à des contres sens :

Il est écrit dans le paragraphe Syntaxe du langage de la logique intuitionniste > Syntaxe de la logique intuitionniste propositionnelle, dans le tableau que "A est prouvable" alors que "non-A est contradictoire". Cela me pose un problème, car il n'est pas évident (voir faux) que "être-contradictoire" est la négation d'"être prouvable". Aussi bien que qu'un énoncé qui n'est pas prouvable n'est pas nécessairement une contradiction, inversement, une proposition non-contradictoire n'est pas nécessairement prouvable. Le problème que je soulève n'est pas à proprement parler un problème de logique intuitionniste mais plutôt un problème de sémantique : Sur l'équivalence et les lien qu'entretiennent les mots "prouvable" et "contradictoire". D'autant plus, que l'on passe par simple négation, d'un mot se référant à une possibilité "prouvABLE" à un mot se référant à une particularité "contradictoire" (contredisable s'il se référait à une possibilité).

Je ne sais pas si c'est une simple erreur de traduction de texte universitaire (ou de livre sur le sujet) ou bien qu'il s'agisse d'une erreur de compréhension, ou enfin qu'il s'agit d'une erreur dans la théorie intuitionniste.

Quoiqu'il en soit, je pense que cela mérite un éclaircissement, et si jamais une correction.

Cordialement Sptc Fa — Le message qui précède, non signé, a été déposé par Sptc Fa (d · c · b), le 7 août 2020 à 16:28 (CEST)Répondre

Une petite correction d'abord : non-A signifie que "A est contradictoire" (et non pas que non-A est contradictoire). Sur le fond de ta question, elle reflète parfaitement la différence entre logique classique et logique intuitionniste, et tu l'as en fait parfaitement saisie. Ainsi, tu dis que « Aussi bien que qu'un énoncé qui n'est pas prouvable n'est pas nécessairement une contradiction, inversement, une proposition non-contradictoire n'est pas nécessairement prouvable ». L'article, quant à lui, dit dans la partie du tiers exclu, que « (A ou non-A) est un théorème de la logique classique, mais pas de la logique intuitionniste. Dans cette dernière, elle signifierait que nous pouvons prouver A ou prouver non-A (i.e. prouver A ou prouver que A est contradictoire), ce qui n'est pas toujours possible ». Ainsi, en logique intuitionniste, le fait que A soit non-contradictoire ne suffit pas à pouvoir le prouver, et le fait que A ne soit pas prouvable ne suffit pas à justifier que A conduit à une contradiction, ce qui correspond bien à ce que tu dis. L'alternative ou bien A est prouvable, ou bien A est contradictoire, n'est pas vérifiée en logique intuitionniste. Theon (discuter) 8 août 2020 à 07:43 (CEST)Répondre

Bonjour. Je reviens sur les échanges relatifs à l'affirmation "une proposition comme « la constante d'Euler-Mascheroni est rationnelle ou la constante d'Euler-Mascheroni n'est pas rationnelle » n'est pas démontrée de manière constructive car la tautologie classique « P ou non P » (tiers exclu) n'appartient pas à la logique intuitionniste" qui apparait dès le RI. Et je prie les contributeurs ayant déjà parcouru ce chemin de m'excuser si je repasse sur leurs pas.

Cet exemple présenté comme illustratif de la différence entre logique classique et logique intuitive appelle, je pense, les remarques suivantes:

1) Il me parait incorrect d'affirmer que cette la proposition n'est pas démontrée de façon constructive "car la tautologie classique « P ou non P » n'appartient pas...", mais il me semblerait plus correct de dire que "puisqu'aucune des deux affirmations qu'elle contient n'est (à ce jour) démontrée de façon constructive, cette affirmation ne l'est pas en logique intuitionniste qui IMPOSE de construire la démonstration de l'un (ou de l'autre) membre de la proposition".

2) l'exemple donné mériterait d'être repris dans la suite de l'article, notamment pour illustrer pourquoi le raisonnement suivant n'est pas acceptable en logique intuitionniste :

P1 : la constante EM existe, et c'est un nombre réel (si P1 n'est pas "prouvable", toute discussion sur les propriétés éventuelles de EP a-t-elle un sens, et lequel?)

P2 : tout nombre réel est soit rationnel, soit irrationnel (s'agissant de la définition des nombres réels, est-il besoin de "construire" une preuve de P2?)

P3 : "donc" EM est soit rationnelle soit irrationnelle. (P3 est-elle ainsi "prouvée"?)

Si j'ai bien compris les définitions, exemples et raisonnements donnés dans l'article, c'est le passage "automatique" de P1+P2 à P3 qui est refusé par la logique intuitionniste : ceci ne mériterait il pas une explication?

Ceci permettait aussi, je crois, de bien illustrer la différence entre vrai/faux (logique classique) et prouvable/non prouvable/non prouvé/faux.

Par ailleurs, en lisant l'article sur la constante EM, je vois qu'il a été prouvé que l'une au moins des constantes EM ou EG est irrationnelle. Ceci pourrait il fournir un autre exemple pour expliquer comment interpréter (différemment) l'affirmation suivante "au moins l'une des deux constantes d'Euler–Mascheroni et d'Euler–Gompertz est irrationnelle" en logique classique et en logique intuitionniste? Olinone (discuter) 14 juin 2025 à 12:57 (CEST)Répondre

Je comprends que la logique intuitionniste soulève beaucoup de problèmes, mais je pense qu'il serait contre-productif, autrement dit, il ne serait pas didactique, de s’appesantir sur la constante d'Euler-Mascheroni, car incidemment cela soulève beaucoup de problèmes, comme :

• Qu'est-ce qu'un nombre réel, en logique intuitionniste ?
• Qu'est-ce qu'un nombre irrationnel, en logique intuitionniste  ?

Pierre Lescanne (discuter) 15 juin 2025 à 10:54 (CEST)Répondre

Non, ce n'est pas ça. C'est que P2 n'est pas vraie en logique intuitionniste. On ne peut pas montrer qu'un réel quelconque est rationnel ou ne l'est pas. On ne peut même pas montrer qu'un réel quelconque est égal ou différent de 0. Mais je suis d'accord qu'il ne faut pas trop s'appuyer sur cet exemple. JeanCASPAR (discuter) 15 juin 2025 à 23:40 (CEST)Répondre

Utilisateur:PIerre.Lescanne et Utilisateur:JeanCASPAR, merci de vos réponses, qui m'amènent aux remarques et propositions suivantes.

1) arguments concernant l'exemple relatif à la constante EM : soit cet exemple est pertinent et il faut le rendre compréhensible, soit il ne l'est pas (ou il est trop compliqué) et il faut en trouver un autre. Mais il me parait indispensable de donner dans l'article un (ou même plusieurs) exemple(s) illustrant la différence fondamentale (et, troublante, c'est sûr) entre logiques classique et intuitionniste : le fait qu'en logique intuitionniste (P ou non P) n'est pas une tautologie. Et d'essayer aussi de montrer que, dans certains cas, on peut cependant prouver (P ou non P) (cf Q1 ci-dessous).

2) Je pense qu'il serait possible de rendre cette différence plus compréhensible en prenant l'exemple de 2 propositions qui, à première lecture, paraissent très semblables :

Q1 : tout entier naturel est pair ou impair

Q2 : tout nombre réel est rationnel ou irrationnel

Q1 comme Q2 sont évidemment "vraies" en logique classique.

Q1 est "prouvable" en logique intuitionniste car il existe au moins un mode opératoire (la division par 2 et l'examen du reste, par exemple) qui permet de vérifier, pour tout entier naturel, s'il est pair ou impair.

En revanche Q2 ne l'est pas car il n'y a pas (à ma connaissance ? à ce jour ? ou même a-t-on prouvé qu'une telle méthode ne peut exister ?) de méthode calculatoire qui permette de déterminer, pour tout réel quelconque, s'il est rationnel ou s'il est irrationnel.

3) Sur les 2 questions posées par Pierre Lescanne : en lisant (attentivement ...et avec un peu de peine car tout cela n'est pas "trivial", au moins pour moi...) les sources en ligne sur les fondements de la logique intuitionniste, il me semble que les 2 questions posées (reflétant celles posées au sujet des propriétés P1 et P2 de ma première intervention) ne me semblent (plus) poser problème. P1 est prouvable. P2 et P3 ne le sont pas.

Merci d'avance de vos retours. Cordialement. Olinone (discuter) 16 juin 2025 à 07:33 (CEST)Répondre

Un exemple classique et sans doute plus pertinent que la constante EM, c'est de regarder si une machine de Turing s'arrête ou non. L'arithmétique de Heyting HA ne prouve pas « pour toute machine de Turing M, M s'arrête ou ne s'arrête pas » mais il y a évidemment des machines précises pour lesquelles l'arithmétique de Heyting prouve la terminaison ou la non-terminaison ; en fait, il y a même des machines M telles que HA ne montre pas que M s'arrête ou non (en prenant M une machine qui cherche une contradiction dans HA). Plus généralement, HA montre « P ou non P » seulement si HA montre « P » ou HA montre « non P ». L'article est un peu confus, c'est ma faute, je me suis laissé confondre par les différents sens de « décidable », je devrais reprendre l'article un jour.

Mais d'un autre côté, je pense que l'exemple avec un machine de Turing est un peu moins abordable que celui avec la constante EM : tous les étudiants en math connaissent la constante EM, alors qu'il y a moins de chance qu'ils connaissent la définition d'une machine de Turing, ils risquent de devoir lire un article en plus pour comprendre et ça risque de les divertir de ce qu'ils cherchent. Je ne sais pas si c'est suffisamment important pour ça.

Je suis résolument contre un exemple détaillé avec des nombres réels, parce qu'il faudrait alors introduire plein de définitions pour expliquer le contexte (les réels de Cauchy et de Dedekind ne coïncident pas en logique intuitionniste, il faut une relation d' « appartness », il y a différentes notions d'égalité, etc.). Mais ça peut être mentionné comme un exemple peu détaillé, comme l'est actuellement la constante EM ; et contrairement à la constante EM on sait que « pour tout x, x est rationnel ou non » n'est pas vrai intuitionnistiquement (mais je pense qu'utiliser « x égal 0 ou x est différent de 0 » est encore plus clair). Pour en apprendre plus sur l'analyse constructive, tu peux regarder en:Constructive analysis, et je pense que tu verras pourquoi je ne pense pas qu'un exemple avec des nombres réels doit être formel. JeanCASPAR (discuter) 16 juin 2025 à 10:17 (CEST)Répondre

@JeanCASPAR@Olinone. Je vois que JeanCASPAR et moi sommes sur la même longueur d'onde. Dès qu'on veut expliquer à un large public formé pas seulement d'étudiants en maths, mais aussi d'étudiants en philosophie (par exemple) ce qu'est la logique intuitionniste, il ne faut pas rentrer dans des détails techniques. Pierre Lescanne (discuter) 16 juin 2025 à 17:32 (CEST)Répondre

@JeanCASPAR et Pierre Lescanne ,

J'avoue que vos retours me surprennent un peu, et ce à plusieurs titres :

1) mes remarques et suggestions visaient explicitement à permettre une meilleure compréhension de la différence (ou au moins d'une des différences) entre logiques classique et intuitionniste par des lecteurs peu familiers avec la logique mathématique, voire plus généralement avec les mathématiques. Quoi de mieux que de prendre un cas concret et de l'utiliser pour une telle approche didactique, visant justement les lecteurs non spécialistes de la logique intuitionniste (qu'ils soient matheux ou non d'ailleurs)?

2) je pense que les exemples que je propose (cf Q1/Q2) sont mieux à même de "parler" à ces lecteurs que EM ou, a fortiori, la machine de Türing. Il est en effet peu risqué d'affirmer que les notions de nombres entiers et de réels sont nettement plus répandues que ne le sont celles de constante EM ou de machine de Türing... Si vous admettez cette affirmation, peut être alors sont-ce les exemples proposés (Q1 et Q2) qui vous paraissent peu opportuns? (cf discussion ci-dessous)

3) l'ensemble des réels (ou des entiers) et la logique intuitionniste : je ne comprends pas comment on peut d'une part prendre un exemple concernant un nombre réel (ce qui est le cas de l'article), puis considérer (cf réponse de JeanCASPAR) qu'il vaudrait mieux éviter de tels exemples (et la lecture de l'article en anglais, au passage très mal sourcé, n'éclaire en rien ce sujet)! Si le problème vient de la définition de R (ou de N) dans le cas intuitionniste, voilà bien un "détail technique" (cf réponse de Pierre Lescanne) qu'on pourrait "enjamber" dans l'article, quitte à mentionner en note que "la définition de cet ensemble en logique intuitionniste dépasse le cadre de cet article" et, si possible trouver une source pour expliciter ce sujet. Ou alors on crée un paragraphe donnant, à titre d'exemple, la construction de N ou R en logique intuitionniste et les différences avec celle réalisée en logique classique...

4) sur quoi peuvent porter les propositions P? Le texte utilise plusieurs formules comme "il existe x tel que", "pour tout élément x", "objet", etc. qui semblent désigner des "choses" sur lesquelles les propositions s'appliquent. Comme il s'agit d'un article de mathématiques, le lecteur peut assez naturellement penser que ces "choses" peuvent être des nombres, d'autant que certains exemples discutent le cas x>1, ou x<0, etc. Certains paragraphes sont plus explicites d'ailleurs quant à cette possibilité : par exemple "double négation" ou encore "disjonction". Donc l'article contient déjà des utilisations d'exemples sur R...alors pourquoi s'en priver pour expliquer simplement (et pourquoi pas dès le RI, sans la justifier alors) l'une des différences importantes entre les 2 logiques?

Cordialement. Olinone (discuter) 16 juin 2025 à 19:31 (CEST)Répondre

Je pense qu'il ne faut pas détailler un exemple mentionnant les nombres réels (mais on peut tout à fait l'utiliser de façon informelle, sans préciser les définitions). Mais si tu comptes utiliser l'exemple plus en détail que ce n'est le cas actuellement pour la constante EM, comment comptes-tu éviter de détailler ? C'est surtout ça mon problème. JeanCASPAR (discuter) 16 juin 2025 à 21:37 (CEST)Répondre

Je propose les actions suivantes :

1) dans le RI, supprimer l'exemple "EP" , et en donner un autre (par exemple Q2) : je vais faire une révision du RI en ce sens, n'hésitez pas à réagir !

2) dans le corps de l'article, créer un chapitre dédié, après celui titré "Histoire", qui illustrerait certaines différences entre logiques classique et intuitionniste en utilisant le moins possible de (voire aucune) symbolique abstraite. Y seraient abordés notamment , sur la base d'exemples, les différences entre vrai/faux et prouvable/non prouvable/contradictoire. Parmi les exemples donnés, on retrouverait celui donné dans le RI, en une version plus explicitée. Et Q1 qui, par contraste, montre que si le principe du tiers exclu n'appartient pas à la logique intuitionniste, il est quand même possible DANS CERTAINS CAS, de prouver "P ou non P" en logique intuitionniste.

Par ailleurs, je reste intrigué par les réticences que tu exprimes quant à l'utilisation d'exemples mentionnant les nombres réels : "il ne faut pas détailler", "utiliser de façon informelle", etc. Pourrais tu les expliciter, et notamment ce que tu entends par "détailler"?

Cdlt. Olinone (discuter) 17 juin 2025 à 08:04 (CEST)Répondre

Les réels intuitionnistes, ne sont pas les réels constructifs (comme je le mentionnais plus haut). Je pense que les réticences sont là (cf ma première intervention). Pierre Lescanne (discuter) 18 juin 2025 à 16:56 (CEST)Répondre

Comme indiqué dans le sujet précédent de cette pdd, je propose de créer un nouveau chapitre juste après le chapitre "Histoire".

Le but est, avant d'entrer dans des développements parfois assez complexes et utilisant, pour beaucoup, une symbolique très spécialisée, de donner aux lecteurs non spécialistes un aperçu "qualitatif" des différences entre les 2 logiques (classique et intuitionniste) basé sur des exemples.

Titre : "Logique classique et logique intuitionniste : principales différences et exemples informels de conséquences"

Contenu (à des mises en forme près) :

"Deux différences principales existent entre logiques classique et intuitionniste :

• la logique intuitionniste rejette le principe du "tiers exclu" : dans cette logique, il ne suffit pas d'avoir démontré qu'une proposition est "fausse" pour que la proposition inverse soit réputée "vraie". Les intuitionnistes évitent d'ailleurs d'utiliser l'opposition vrai/faux : ils utilisent les notions de "prouvable" et de "contradictoire".
• en logique intuitionniste une proposition est dite "prouvable" si et seulement si on peut exhiber un processus calculatoire tel que, appliqué à chaque élément de l'ensemble sur lequel porte la proposition et sans utiliser le principe du tiers exclu, il produise le résultat annoncé par la proposition.

Les exemples suivants illustrent certaines des conséquences et des différences induites entre les deux types de logiques :

Proposition 1 (P1): "tout nombre réel est soit rationnel soit irrationnel". Cette proposition, trivialement vraie en logique classique, n'est pas prouvable en logique intuitionniste. En effet, pour qu'elle soit prouvable, il faudrait avoir un processus calculatoire qui permettrait, appliqué à n'importe quel entier, de démontrer, sans utiliser le principe du tiers exclu, soit qu'il est rationnel, soit qu'il est irrationnel. Or, dans l'état actuel des connaissances mathématiques, un tel processus n'existe pas.

Proposition 2 (P2): "tout nombre entier est soit pair soit impair". Cette proposition, trivialement vraie en logique classique et apparemment assez semblable à P1, est, contrairement à P1, prouvable en logique intuitionniste. En effet, il existe au moins un processus qui permet de prouver, pour chaque entier n, qu'il est pair, ou qu'il est impair : par exemple, on le divise par "2" et si le reste est "0" on a prouvé que n est pair, et si le reste est "1" on a prouvé que n est impair.

Plus généralement, plusieurs des démonstrations admises en logique classique ne sont pas admises en logique intuitionniste. Par exemple, une démonstration classique de l'irrationalité de ${\displaystyle {\sqrt {2}}}$ est la suivante : supposons que ${\displaystyle {\sqrt {2}}}$ soit rationnel, donc ${\displaystyle {\sqrt {2}}}$= a/b (a et b entiers premiers entre eux). Donc a²=2xb², ce qui est impossible. Donc ${\displaystyle {\sqrt {2}}}$ n'est pas rationnel, donc (en logique classique) ${\displaystyle {\sqrt {2}}}$ est irrationnel. La logique intuitionniste refuse cette dernière conclusion : la méthode calculatoire utilisée a bien prouvé que ${\displaystyle {\sqrt {2}}}$ n'est pas rationnel, mais a dû utiliser le tiers exclu pour affirmer que ${\displaystyle {\sqrt {2}}}$ est irrationnel. Les intuitionnistes diront donc que la proposition "${\displaystyle {\sqrt {2}}}$ est rationnel " est contradictoire, mais, pour eux, ceci ne suffit pas à prouver la proposition inverse : "${\displaystyle {\sqrt {2}}}$ n'est pas rationnel".

Merci d'avance de vos avis. Olinone (discuter) 17 juin 2025 à 15:18 (CEST)Répondre

Cela risque de faire un peu doublon avec Logique intuitionniste#Relations avec la logique classique, non ?

Plusieurs remarques :

• Pour la première différence : pour moi, les logiciens classiques font aussi une différence entre vrai et prouvable : le premier se réfère à un modèle, le deuxième à un système formel. La différence, c'est que si "il est contradictoire que A soit contradictoire", je ne peux pas en déduire une preuve de A.
• Pour la seconde : "processus calculatoire", ce n'est pas propre à la logique intuitionniste. Le principe de Markov est constructif et correspond à un processus calculatoire, mais n'est pas valide en logique intuitionniste selon toutes les écoles. Une des caractéristiques importantes, c'est la propriété de la disjonction et de l'existence : si ${\displaystyle \vdash A\lor B}$ alors ${\displaystyle \vdash A}$ ou ${\displaystyle \vdash B}$, et si ${\displaystyle \vdash \exists x,P}$, alors j'ai un terme t explicite tel que ${\displaystyle \vdash P[x:=t]}$ (d'ailleurs, le principe de Markov ne casse pas cette propriété). D'ailleurs, il y a même des interprétations calculatoires de la logique classique.
• Pour P1 : ce n'est pas "en l'état actuel de nos connaissances mathématiques" (contrairement à l'exemple sur la conjecture de Goldbach dans Constructivisme (mathématiques)), on sait qu'aucun tel algorithme n'existe.
• Pour P2 : je remplacerais le "il existe au moins un algorithme" par "il existe un algorithme", voire "il y a un algorithme", je trouve le "au moins un" de mauvais goût.
• Pour l'exemple avec ${\displaystyle {\sqrt {2}}}$ : c'est un raisonnement parfaitement valide en logique intuitionniste : il s'agit de montrer un énoncé de la forme ${\displaystyle \neg P}$, on suppose donc ${\displaystyle P}$ et on arrive à une contradiction, ce qui nous donne une preuve de ${\displaystyle \neg P}$. Un exemple valide serait de supposer ${\displaystyle \neg \forall n,u_{n}=0}$ et d'en déduire ${\displaystyle \exists n,u_{n}=1}$ avec ${\displaystyle u_{n}}$ une suite binaire (cela correspond peu ou prou au principe limité d'omniscience (en:Limited principle of omniscience), qui n'est pas valide en logique intuitionniste, mais qui admet une interprétation calculatoire évidente (on lance un programme qui teste ${\displaystyle u_{n}}$ pour chaque ${\displaystyle n}$ et renvoie le premier tel que ${\displaystyle u_{n}=1}$, ce programme terminant puisque ${\displaystyle \neg \forall n,u_{n}=0}$)). Un exemple sur les nombres réels serait difficile à comprendre, mais par exemple ${\displaystyle \neg (x\leq 0)\to x>0}$ est faux en logique intuitionniste. Ou alors prendre un exemple quelconque de loi de De Morgan non vérifiée. Mais ça ferait doublon avec ce qu'il y a en bas.

JeanCASPAR (discuter) 19 juin 2025 à 00:01 (CEST)Répondre

Merci de ta réponse, et je suis convaincu que nous allons trouver des moyens d'améliorer l'article ensemble!

Je reprends certaines de tes remarques et suggestions:

1) "Pour P1 : ce n'est pas "en l'état actuel de nos connaissances mathématiques" (contrairement à l'exemple sur la conjecture de Goldbach dans Constructivisme (mathématiques)), on sait qu'aucun tel algorithme n'existe". Si c'est vrai et sourcé (merci de mentionner la source), c'est très bon : on a donc un exemple où on sait que "P ou non P" ne peut être prouvé en logique intuitionniste. Et on pourrait mentionner quelque part dans l'article l'autre cas où on ne sait pas (encore?) s'il est prouvable ou non.

2) "les logiciens classiques font aussi une différence entre vrai et prouvable" . C'est peut être vrai...mais ce que je dis n'est pas contradictoire (sic!) : j'affirme seulement que les intuitionnistes évitent ces termes (ce qui, en toute logique (sic) , n'implique rien sur ce que font les non intuitionnistes). Par ailleurs, nombre de publications et plusieurs passages de l'article "opposent" intuitionniste et classique justement par ce point. Si tu penses que c'est mal dit, n'hésite pas à proposer mieux.

3) ""processus calculatoire", ce n'est pas propre à la logique intuitionniste". Cf remarque précédente : je ne dis pas que la logique classique ne l'impose jamais, je dis que la logique intuitionniste l'impose toujours.

4) Preuve de l'irrationnalité de la racine carrée de 2 : là je suis surpris (mais n'affirme pas avoir raison, et c'est bien pour cela que j'ai mis ma proposition de texte en pdd et non directement dans l'article). Par quel raisonnement, dans ce cadre précis, les intuitionnistes admettraient-ils que ceci a prouvé que "racine de 2 est irrationnel" ? La méthode classique que je mentionne démontre bien que (vocabulaire intuitionniste) l'affirmation "racine de 2 est rationnel" est contradictoire. Par quel raisonnement, dans ce cadre précis, les intuitionnistes admettraient-ils que ceci a prouvé que "racine de 2 est irrationnel" ? Aurais-tu une explication, ou, mieux encore, une référence qui éclairerait ce sujet? Pour préciser mo interrogation : le raisonnement examiné commence par "supposons que x soit rationnel". Tout raisonnement basé sur cette brique ne peut conclure QUE sur cette affirmation (en logique intuutionniste). Olinone (discuter) 19 juin 2025 à 10:21 (CEST)Répondre

1) Je n'ai pas de sources directes, mais il est bien connu qu'il est cohérent de supposer que toutes les fonctions réelles sont continues (il y a plein de sources dans ce post MSE : https://math.stackexchange.com/questions/176279/all-real-functions-are-continuous ; n'importe laquelle devrait faire l'affaire). Or si on peut décider si un réel est rationnel ou non, on peut facilement définir l'indicatrice de ${\displaystyle \mathbb {Q} }$, hors cette fonction (même en logique intuitionniste) n'est pas continue : contradiction. Je suis d'accord qu'on peut aussi mentionner la conjecture de Goldbach plus bas dans l'article. On peut aussi mentionner un exemple indépendant de l'axiomatique, même classique, par exemple l'énoncé "HA est cohérente" regardé dans HA.

2) 4) et quelque chose que je n'ai pas remarqué avant. Je propose de laisser tomber complètement la distinction vrai/faux et prouvable/contradictoire : l'une est une notion sémantique, l'autre liée à un système formel, mais ce sont les mêmes choses derrière : il faudrait certes dire systématiquement prouvable/contradictoire, mais c'est lourd, et c'est exactement la même chose en logique classique. En revanche, tu dis ceci "dans cette logique, il ne suffit pas d'avoir démontré qu'une proposition est "fausse" pour que la proposition inverse soit réputée "vraie"". C'est très exactement l'inverse. Dire "A est faux" c'est pareil que dire "A => faux" c'est pareil que dire "non A". En revanche, ce n'est pas parce qu'il est faux de dire qu'une proposition est fausse que cette proposition est vraie pour autant. Je propose de remplacer le premier point par ceci :

• la logique intuitionniste rejette le principe du tiers exclu ou la démonstration par l'absurde, qui lui est équivalente : dans cette logique, il ne suffit pas d'avoir démontré qu'une proposition n'est pas fausse pour qu'elle soit réputée vraie.

3) "je ne dis pas que la logique classique ne l'impose jamais", si, il y a un si et seulement si :p. Je propose cela :

• la logique intuitionniste est une logique constructive : on peut interpréter chaque preuve comme un processus calculatoire, au travers de l'interprétation BHK ; en particulier, d'une preuve de ${\displaystyle A\lor B}$ on peut extraire l'information de quelle proposition ${\displaystyle A}$ ou ${\displaystyle B}$ est vraie, et d'une preuve de ${\displaystyle \exists x.P}$ on peut extraire un témoin ${\displaystyle t}$ tel que ${\displaystyle P[x:=t]}$.

4) cf. message d'en bas.

JeanCASPAR (discuter) 19 juin 2025 à 22:03 (CEST)Répondre

Je reviens sur le sujet "racine de 2" pour bien préciser mon point: je n'affirme pas qu'il est impossible de prouver, en logique intuitionniste, que racine de 2 est irrationnel. Mon point est de dire que la méthode classique mentionnée et utilisée pour ce faire ne le permet pas. Et d'ailleurs mon texte devrait être plus précis sur ce point comme par exemple : "Les intuitionnistes diront donc que la démonstration a bien établi que "racine de 2 est rationnel " est contradictoire, mais n'a pas prouvé que : " racine de 2 est irrationnel"." Olinone (discuter) 19 juin 2025 à 17:13 (CEST)Répondre

@Olinone pour être plus clair, utilisons des formules. Si ${\displaystyle x\in \mathbb {Q} }$ est la formule « ${\displaystyle x}$ est rationnel », la formule « ${\displaystyle x}$ est irrationel » s'écrit ${\displaystyle (x\in \mathbb {Q} )\to \bot }$. Donc pour prouver cette formule, il faut supposer que ${\displaystyle x}$ est rationnel et arriver à une contradiction. C'est exactement ce que fait cette preuve. En fait, la proposition « ${\displaystyle x}$ est irrationnel » est définie comme étant l'affirmation que « ${\displaystyle x}$ est rationnel » est contradictoire. JeanCASPAR (discuter) 19 juin 2025 à 19:26 (CEST)Répondre

Je pense avoir (enfin?) compris. Ton raisonnement tient...dès lors qu'on admet que par définition "x est irrationnel", veut dire "il n'existe aucun a, b tels que x=a/b", ce qui veut exactement dire "x n'est pas rationnel". Alors la démonstration classique tient même en logique intuitionniste. Du coup la question est : la définition de "x est irrationnel" est-elle (obligatoirement) celle utilisée ici? (j'avoue que ma compréhension de la construction intuitionniste des rationnels et des réels est trop lacunaire pour que j'avance une réponse à cette question!). Olinone (discuter) 20 juin 2025 à 08:07 (CEST)Répondre

Je ne maîtrise pas du tout les réels intuitionnistes donc je ne saurais pas trouver de référence à ce sujet, mais je ne vois pas ce qu'on pourrait avoir comme autre définition. Je peux essayer de chercher. JeanCASPAR (discuter) 20 juin 2025 à 09:29 (CEST)Répondre

Je pense que ce n'est pas une bonne idée de d'utiliser des expressions comme « Un intuitionniste pense que ... tandis qu'un logicien classique pense que ... ». Il n'y a pas de telles personnes et c'est plutôt un langage de journaliste. Pierre Lescanne (discuter) 19 juin 2025 à 09:57 (CEST)Répondre

Je précise (vous rassure ?): je ne suis pas journaliste ! Si cette forme parait impropre, je peux remplacer partout "les intuitionnistes" par "en logique intuitionniste" et "les non intuitionnistes" par "en logique classique". Je souligne cependant que certaines publications, peu suspectes d'être "journalistiques", utilisent bien le terme "mathématicien non intuitionniste", par exemple celle-ci. Cordialement. Olinone (discuter) 19 juin 2025 à 17:20 (CEST)Répondre

J'ai une autre critique contre cette formulation : la logique intuitionniste n'est pas particulièrement pratiquée par les intuitionnistes (courant philosophique et mathématique), c'est un système formel intéressant en tant que tel pour plein de gens qui ne sont pas forcément intuitionnistes. Je pense qu'il vaut mieux ne pas « personnaliser » le texte. JeanCASPAR (discuter) 19 juin 2025 à 22:07 (CEST)Répondre

Ok, donc il serait peut être utile de préciser le titre de l'article en : "Logique intuitionniste (mathématiques)" Olinone (discuter) 20 juin 2025 à 10:51 (CEST)Répondre

Non, je ne pense pas, les mots entre parenthèses, c'est pour les noms ambigus. Il faudrait peut-être préciser dans le RI que c'est le système formel basé sur le courant philosophique, le paragraphe histoire le fait bien. JeanCASPAR (discuter) 21 juin 2025 à 11:24 (CEST)Répondre

Bon, il y a tant à faire sur l'article et argumenter sur son titre ne fait pas forcément partie des premières priorités! Donc je laisse tomber ce sujet et éviterai d'employer dans le texte des formules "personnalisant" les affirmation/positions de telle ou telle approche. Je souligne cependant que, mis à part une très petite partie du chapitre "histoire" , TOUT le reste est strictement consacré à la logique intuitionniste en mathématiques...Cdlt. Olinone (discuter) 21 juin 2025 à 19:10 (CEST)Répondre

En ligne avec les sujets discutés récemment sur cette pdd, je propose de revoir le RI de l'article pour le rendre intelligible pat tout lecteur (attentif mais pas forcément matheux), n'y utiliser aucun symbole logique, et illustrer certaines affirmations par un exemple (repris de la suggestion de nouveau chapitre faite ci-dessus).

Le texte proposé est le suivant :

"La logique intuitionniste est une logique qui diffère de la logique classique par le fait que la notion de vérité est remplacée par la notion de preuve constructive, et que la tautologie classique « P ou non P » (tiers exclu) ne peut être utilisée. La logique intuitionniste considère notamment que la proposition « ne pas être faux » n'est pas équivalente à la proposition "être vrai". Certaines méthodes de démonstration et leurs résultats, valides en logique classique, ne le sont donc pas en logique intuitionniste. Par exemple, la proposition "tout nombre réel est soit rationnel, soit irrationnel", trivialement vraie en logique classique, n'est pas, dans l'état actuel des connaissances mathématiques, prouvable en logique intuitionniste.

Développée à partir de la fin des années 1910, la logique intuitionniste a depuis eu une influence importante sur le développement des logiques constructives et de l'informatique théorique." Merci d'avance de vos avis. Olinone (discuter) 17 juin 2025 à 18:37 (CEST)Répondre

Même remarque que plus haut sur le « dans l'état actuel des connaissances mathématiques », très bien sinon. Je rajouterais une mention du fait qu'on refuse aussi la démonstration par l'absurde. JeanCASPAR (discuter) 19 juin 2025 à 22:54 (CEST)Répondre

Après diverses recherches, j'ai trouvé (Van Dalen 2004 p 30) un exemple illustratif de différence interprétative liée au tiers exclu : l'affirmation "L'hypothèse de Riemann est vraie ou fausse" est valide en logique classique et pas en logique intuitionniste, car aucune preuve n'a été apportée (à ce jour) que cette hypothèse soit vraie, et aucune non plus qu'elle soit fausse. Certes l'hypothèse de Riemann porte sur des objets assez complexes, mais, indépendamment du contenu de cette hypothèse, ce qui est "simple " à comprendre grâce à cet exemple, c'est qu'en logique intuitionniste, une telle affirmation, pour être acceptée doit être soutenue par une preuve de "A est vrai" ou de "non A est vrai". Nous pourrions donc prendre cet exemple? Plus puissant encore serait l'exemple "tout réel est soit rationnel soit irrationnel" car, d'après toi, il y aurait une preuve que cette affirmation ne peut pas être démontrée en logique intuitionniste. As-tu accès à une telle démonstration? Olinone (discuter) 21 juin 2025 à 19:21 (CEST)Répondre

Comme je l'ai dit plus haut, je n'ai pas trouvé de telle démonstrations dans la littérature, mais ce n'est pas très compliqué à démontrer, cf. le 1) de Spécial:Diff/226635405. JeanCASPAR (discuter) 21 juin 2025 à 23:28 (CEST)Répondre

D'après les règles de WP, si nous devions utiliser l'exemple "tout réel est rationnel ou irrationnel" pour dire que c'est "vrai" en logique classique et non prouvable en logique intuitionniste, il serait impératif de fournir une référence (et pas seulement une démonstration) de cette importante affirmation. Olinone (discuter) 22 juin 2025 à 08:35 (CEST)Répondre

Ah, j'ai enfin trouvé une source. Page 5 de cet article : https://doi.org/10.1016/S0304-3975(98)00285-0. Il y a plein d'autres exemples d'ailleurs. JeanCASPAR (discuter) 22 juin 2025 à 14:31 (CEST)Répondre

Il faudrait donc renvoyer à analyse constructive, plutôt que le traiter ici. Pierre Lescanne (discuter) 22 juin 2025 à 14:58 (CEST)Répondre

Merci Jean! Voici donc une preuve de cette très forte affirmation. Je vais revoir ma proposition de RI en ce sens, et inclure la référence. Olinone (discuter) 23 juin 2025 à 07:08 (CEST)Répondre

Voici donc le nouveau RI que je propose :

"La logique intuitionniste est une logique qui diffère de la logique classique par le fait que toute affirmation doit être démontrable par une preuve constructive. Cette logique rejette le principe classique de tiers exclu, selon lequel "P ou non P" est toujours vrai, ainsi que les démonstrations par l'absurde. La logique intuitionniste considère notamment que la proposition « ne pas être faux » n'est pas équivalente à la proposition "être vrai". Certaines affirmations et démonstrations, valides en logique classique, ne le sont donc pas en logique intuitionniste. Par exemple, la proposition "tout nombre réel est soit rationnel, soit irrationnel", trivialement vraie en logique classique, n'est pas prouvable en logique intuitionniste^[1].

Développée à partir de la fin des années 1910 par les mathématiciens néerlandais Luitzen Egbertus Jan Brouwen et Aren Heyting, la logique intuitionniste a eu une influence importante sur le développement des logiques constructives puis de l'informatique théorique." Olinone (discuter) 23 juin 2025 à 07:27 (CEST)Répondre

J'aime bien! Mais il ne faut pas de références dans le RI, il faut en parler plus bas dans le texte. JeanCASPAR (discuter) 23 juin 2025 à 10:22 (CEST)Répondre

On y va donc, en réservant l référence au corps du texte. Olinone (discuter) 23 juin 2025 à 11:44 (CEST)Répondre

RI modifié comme discuté Olinone (discuter) 23 juin 2025 à 14:20 (CEST)Répondre

Dans la section "relations avec la logique classique/exemples/quelques validités" un tableau donne des "explications" pour certaines relations d'implication (colonne de droite du tableau). Certaines de ces explications me paraissent soulever question :

1) "être grand et petit est contradictoire" : encore faudrait-il définir sur quel ensemble cette proposition est faite, et quelle est la définition de "grand" et "petit" dans cet ensemble. Par exemple si l'ensemble considéré est constitué de disques verts et de disques rouges, ayant tous le même rayon, et si "grand/petit" se réfère à ce rayon (ou à la surface de ces disques) alors comment définir "grand vs petit" pour aboutir à l'affirmation "être grand et petit est contradictoire" ? Et une autre définition n'aboutirait elle pas à un autre résultat ? Donc ne faudrait-il pas trouver un autre exemple explicatif? Dans le cas des disques mentionnés ci dessus, "être vert et rouge" est, par exemple, sans doute "contradictoire".

2) richesses et pauvreté : on lit " « pour tout x, x est pauvre » est contradictoire (car je vois qu'il existe des richesses)". Cette explication est plus intrigante encore que celle mentionnée ci-dessus. Non seulement il faudrait définir riche vs pauvre (comme grand vs petit), mais que cette définition implique ou contienne un "loi" imposant que "s'il existe des richesses, alors il est impossible (contradictoire) que tous les x soient pauvres". Je prends un exemple : une population vit sur un île, sur un total pied d'égalité. Un explorateur découvre cette île et le très bas niveau de vie de cette population : d'après ses critères les habitants sont "tous pauvres". Ce même explorateur découvre un trésor sur l'île qui SI il était distribué à la population rendrait les habitants, selon ses critères, tous riches. Mais tant que cette distribution n'est pas réalisée, il y a à la fois une grande richesse sur l'île et une population pauvre... Ne faudrait-il pas trouver un autre exemple explicatif ?

3) pluie et se faire mouiller : cet exemple est encore plus intrigant que les deux précédents. Il semble admettre comme "évident" que le fait de se faire mouiller en sortant (constatation sensorielle que je ne conteste pas) "prouverait" qu'il pleut. Or il y a, dans la vie réelle, bien d'autres possibilités amenant à se faire mouiller en sortant : passer sous un arrosage automatique en activité, tomber dans une rivière, etc. Donc la conséquence (être mouillé) n'implique pas nécessairement un cause donnée (il pleut) : il faut une définition plus complète de l'univers dans lequel le raisonnement s'applique pour pouvoir assurer que "si je sors et que je suis mouillé, c'est qu'il pleut". Ne faudrait-il pas, ici aussi, un autre exemple explicatif? Olinone (discuter) 18 juin 2025 à 12:05 (CEST)Répondre

Je suis d'accord. On peut proposer ça :

1) Si on sait que ${\displaystyle A}$ et ${\displaystyle B}$ ensembles sont contradictoires, on ne peut pas isoler si l'une ou laquelle des deux est contradictoire.

2) Si on sait que ${\displaystyle \forall xA}$ est contradictoire, on ne peut isoler un élément précis qui ne vérifie pas ${\displaystyle A}$.

3) Si on sait que le fait que ${\displaystyle A}$ soit contradictoire est contradictoire, on ne peut pas en extraire une preuve de ${\displaystyle A}$.

Et d'ailleurs, les autres explications des réciproques sont vaseuses aussi.

Pour ${\displaystyle (\neg A\lor B)\to (A\to B)}$, la réciproque est fausse puisque si on sait qu'une preuve de ${\displaystyle A}$ permet d'obtenir une preuve de ${\displaystyle B}$ aussi, cela ne permet pas de déterminer si ${\displaystyle A}$ est contradictoire ou s'il existe une preuve de ${\displaystyle B}$.$

Il faudrait rajouter une ligne pour ${\displaystyle (A\to B)\to (\neg B\to \neg A)}$ : si ${\displaystyle A\to B}$, ${\displaystyle \neg B}$ et ${\displaystyle A}$ alors j'ai ${\displaystyle B}$, donc j'ai ${\displaystyle \bot }$ grâce à ${\displaystyle \neg B}$. Ça c'est pour l'implication, mais la réciproque est fausse puisque si j'ai une preuve de ${\displaystyle A}$ et si je sais que si ${\displaystyle B}$ est contradictoire alors ${\displaystyle A}$ aussi, je ne peux qu'obtenir une preuve de ${\displaystyle \neg \neg B}$ au mieux, pas une preuve de ${\displaystyle B}$.

Pour ${\displaystyle \neg A\leftrightarrow \neg \neg \neg A}$, je pense qu'il vaut mieux renoncer à expliquer le sens derrière. En tout cas l'explication actuelle n'explique rien. Ça donnerait quelque chose comme ça : "si on sait que ${\displaystyle \neg \neg \neg A}$, c'est-à-dire qu' « il est contradictoire que le fait que A soit contradictoire est contradictoire », alors ...", je ne pense qu'on peut arriver à quelque chose, mais si tu as une meilleure idée, pourquoi pas. On peut simplement dire que le sens directe est une instance de ${\displaystyle A\to \neg \neg A}$, et le sens réciproque une instance de ${\displaystyle (A\to B)\to (\neg B\to \neg A)}$, combinée avec ${\displaystyle A\to \neg \neg A}$. JeanCASPAR (discuter) 19 juin 2025 à 23:22 (CEST)Répondre

Je propose de compléter le chapitre syntaxe par un sous chapitre axiomatique qui expliquerait le rejet du tiers exclu, et en donnerait une des raisons/illustrations (l'exemple "tout réel est rationnel ou irrationnel" avec sa référence). Le texte serait le suivant :

"Axiomatique

La logique classique est basée sur trois axiomes, ou principes, hérités de la logique d'Aristote :

• axiome d'identité : "Ce qui est est". Soit, en syntaxe logique : ${\displaystyle A\Leftrightarrow \ A}$
• axiome de non-contradiction : "Il est impossible qu’une seule et même chose soit, et tout à la fois ne soit pas, à une même autre chose, sous le même rapport"^[2]. Soit, en syntaxe logique : ${\displaystyle \lnot (A\land \lnot A)}$
• axiome du tiers exclu : "Il n’est pas possible davantage qu’entre deux propositions contradictoires, il y ait jamais un terme moyen". Soit, en syntaxe logique : ${\displaystyle A\lor \lnot A}$

La logique intuitionniste accepte les deux premiers axiomes, mais rejette le troisième : en logique intuitionniste, cet axiome reviendrait à affirmer que pour toute proposition ${\displaystyle A}$ on pourrit trouver une preuve de ${\displaystyle A}$ ou une preuve de ${\displaystyle \lnot A}$, ce qui est faux : par exemple, la proposition "tout nombre réel est rationnel ou irrationnel" est trivialement vraie en logique classique (principe du tiers exclu), mais n'est pas prouvable en logique intuitionniste^[3]."

Merci de vos avis.

Olinone (discuter) 23 juin 2025 à 16:46 (CEST)Répondre

Qu'étudions-nous ?

Nous sommes ici pour étudier une branche de la logique mathématique du XX^e siècle et du XXI^e siècle. Il ne faut donc, à mon avis, pas parler d’Aristote dans cet article, car Aristote n'est pas lié à la naissance de la logique intuitionniste, ni à la naissance de la logique formelle dont est issue la logique intuitionniste contemporaine. Je ne vois pas plus de trace de ce Grec, que des Indiens et des Chinois. Je pense par contre que les lecteurs attendent qu'on leur parle des mathématiciens du début du XX^e siècle qui en ont vraiment été les acteurs. Ceux qui s'intéressent aux liens historiques ente la logique aristotélicienne et la logique formelle contemporaine devraient être renvoyés vers l’article Histoire de la logique

Devons nous intéresser en priorité à ce que la logique intuitionniste n'a pas ?

Nous devons nous intéresser à ce qu’elle a.

1. Elle privilégie les démonstrations, dont elle fait des objets de 1^re classe pour accepter un fait.
2. Elle est constructive.
3. Elle exhibe un objet quand elle affirme qu'il existe.

Il ne faut pas parler de ce qu'elle n'a pas, car, à y bien penser, il manque, à la logique classique beaucoup de concepts, pourtant fort utiles.

Ne risquons-nous pas de rebuter une partie de notre lectorat ?

J'identifie nos lecteurs comme des scientifiques, par exemple en études d'informatique, de maths, de sciences des données ou de sciences de l’ingénieur. Je crains qu'Aristote ne les branche pas beaucoup . Pierre Lescanne (discuter) 24 juin 2025 à 12:30 (CEST)Répondre

Merci de votre réponse, qui m'amène à formuler les remarques et propositions suivantes :

1) Aristote : la plupart des ouvrages consacrés à la logique (formelle, classique, intuitonniste, constructive...), lorsqu'ils abordent, ne serait-ce que fugitivement, l'histoire de la Logique, mentionnent Aristote, mais aussi Platon, ou encore Kant, Descartes, etc. Je ne pense pas qu'une seule mention d'Aristote serait plus "rebutante" que les mentions de Brouwer, Heyting, Kolmogorov et alii. L'intérêt que j'y vois est d'indiquer "en passant" que la logique intuitionniste rejette une partie des raisonnements logiques qui avaient "tenu" de l'Antiquité au début du 20ème siècle. Mais je suis prêt à laisser tomber cette (micro) référence antique ! Rebondissant sur l'aspect "rebutant", je me permets de faire remarquer que la lecture des chapitres "Règles de déduction naturelle" et "Sémantique de la logique intuitionniste" demande une réelle attention et leur compréhension de (très) solides bases logico-mathématiques.

2) "Qu'étudions-nous?" Je ne saisis pas bien le sens de cette question. D'après ce que je comprends, un article de WP, de mathématiques comme d'histoire ou encore de sociologie, n'a pas vocation à être un "cours" ni une "étude" sur le sujet traité mais, comme indiqué régulièrement sur la discussion Le Thé du portail Mathématiques (et d'autres), de faire un point (sourcé) des connaissances relatives à ce sujet, en l'exposant de manière didactique et le formulant de la façon la plus accessible possible. Il est certain qu'en maths il n'est pas toujours évident de trouver l'équilibre en exactitude et lisibilité !

3) "ce qu'elle a ou n'a pas" : l'approche que je propose, pour l'article ici discuté, et que j'explicite dans cette réponse, est de faire chaque fois que possible la comparaison entre un "objet" de la logique classique (affirmation, démonstration, résultat) et son "pendant" en logique intuitionniste : il ne s'agit donc pas de dire ce qu'ont (ou n'ont pas) ces logiques, mais en quoi elles se différencient. Je pars en effet du postulat que la plupart des lecteurs seront bien plus familiers avec la logique classique qu'avec tout autre, ce qui devrait leur permettre de comprendre/apprécier le "jeu des différences" qui leur est proposé. Et, qui sait, aiguiser leur curiosité puis les amener à lire d'autres articles ou les sources mentionnées.

4) Vous suggérez d'utiliser ces attributs pour qualifier la logique intuitionniste :

1. Elle privilégie les démonstrations, dont elle fait des objets de 1^re classe pour accepter un fait.
2. Elle est constructive.
3. Elle exhibe un objet quand elle affirme qu'il existe.

Je suis tout à fait d'accord et vais essayer de les introduire (sauf si vous voulez le faire vous-même). Par ailleurs, avez vous des remarques (hormis la référence à Aristote) sur le fond de ma proposition de paragraphe sur les axiomes ? Olinone (discuter) 25 juin 2025 à 07:28 (CEST)Répondre

Je réponds à certains points.

1) Un renvoi à l’article Histoire de la logique, en précisant la section, suffirait peut-être. Sinon, l'article risquerait d'être hors sujet.

2) OK pour un point sourcé de la logique intuitionniste en 2025, or je crains qu'une phrase comme « Il n’est pas possible davantage qu’entre deux propositions contradictoires, il y ait jamais un terme moyen » ne soit pas vraiment didactique. En revanche pour l’informatique d'aujourd'hui, il faut parler d'assistant de preuve.

3) « faire chaque fois que possible la comparaison entre un "objet" de la logique classique et son "pendant" en logique intuitionniste ». Pourquoi seulement pour la logique classique ? En plus ça ne marchera pas, dans le cas où la logique intuitionniste a des objets que la logique classique n'a pas, je pense aux comportements différenciés des connecteurs et des quantificateurs de la logique intuitionniste. Pierre Lescanne (discuter) 25 juin 2025 à 12:23 (CEST)Répondre

Concernant 3), je signale qu'il y a une section intitulée Relation avec la logique classique. Pierre Lescanne (discuter) 25 juin 2025 à 12:46 (CEST)Répondre

Vu la section en question, que je propose d'ailleurs de "remonter" pour les raisons indiquées plus bas dans cette pdd. Olinone (discuter) 4 juillet 2025 à 08:15 (CEST)Répondre

Sur le point 3), je crois que le texte est explicite : les connecteurs sont formellement les mêmes (et, ou, implication, existence, etc.), mais ont des interprétations différentes, que le texte souligne désormais. Si ceci n'est pas suffisant, n'hésitez pas à compléter/modifier. Olinone (discuter) 4 juillet 2025 à 08:14 (CEST)Répondre

Suite aux discussions précédentes, et en cohérence avec l'approche que je propose d' mettre en avant, autant que possible, des éléments de comparaison classique/intuitionniste pour faciliter la compréhension des lecteurs non spécialistes, j'ai entamé une révision du plan en remontant la quasi-totalité du chapitre "relations classique/intuitionniste" pour la mettre juste après "syntaxe". Ce choix prend également en compte le fait que cette section peut être lue (et , je l'espère, comprise), sans avoir lu (ni compris peut-être) les chapitres suivants, plus ardus ( "déduction naturelle" et "sémantique"). Olinone (discuter) 4 juillet 2025 à 08:11 (CEST)Répondre