L'idée originelle de la logique intuitioniste

ideosphe
ideosphe
dans Fondements et Logique
Edit sur le titre intuitionniste avec trois n n'est pas passé

Bonjour

Je n'ai pas compris l'idée philosophique qui a amené la logique intuitionniste. Pourriez-vous me donner cette idée qui en fût la genèse ?
Merci d'avance.

Réponses

  • christophe c
    christophe c
    Historiquement, c'est + ou - dû au fait qu'il existe des preuves très courtes d'existence d'entiers (par exemple), dont on a aucune idée de la manière de les borner. Sans même parler du fait qu'on prouve certaines existences sans aucune information sur l'objet, même dans le domaine purement fini.

    Par exemple, tu prouves en 5 lignes qu'il existe une stratégie infaillible aux échecs, mais ça ne te le donne pas.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Champ-Pot-Lion
    Champ-Pot-Lion
    La preuve d'une stratégie infaillible aux échecs (modulo les matchs nuls) est intuitionniste, n'est-ce pas ? On a un algorithme qui, avec suffisamment de puissance de calcul, trouve cette stratégie optimale.
  • Foys
    Foys
    On doit pouvoir démonter le théorème de Zermelo (sur l'existence d'une stratégie optimale à des jeux comme les échecs) de manière intuitionniste: c'est juste une récurrence sur la taille de l'arbre. Ce n'est pas un bon exemple.

    Considérons un nombre comme $\sqrt{2}$ et envisageons son développement en base 10.
    Que penser des deux énoncés suivants?
    (I) Parmi les chiffres de 1 à 9 il y en a au moins un qui apparaît une infinité de fois dans le développement en base 10 dudit nombre.
    (II) Essayer parmi les chiffres de 1 à 9, d'en fournir un qui ait à coup sûr cette propriété.

    On voit bien qu'il est beaucoup plus difficile de répondre à (II) que de s'assurer de (I) (qui provient de ce que sinon ,il n'yaurait qu'un nombre fini de chiffres après la virgule pour $\sqrt{2}$, or on sait que ce n'est pas le cas puisque $\sqrt{2}$ est irrationnel).

    La logique intuitionniste a été inventée à la base par Brouwer pour que quand on prouve l'eistence d'un objet, on l'exhibe (et effectivement c'est le cas en arithmétique intuitionniste-dite de Heyting: si on peut démontrer un énoncé du type $\exists xP(x)$, alors on peut construire un nombre explicite $N$ tel qu'on puisse aussi démontrer $P(N)$).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Foys
    Foys
    Brouwer était en fait réfractaire à l'idée que l'on puisse être sûr que la conjecture de Fermat était vraie ou bien fausse, sans pour autant pouvoir la trancher à l'époque.

    D'où l'idée de ne pas accepter des énoncés comme $A \vee \neg A$ sauf si on est capable de prouver $A$, ou bien on est capable de prouver $\neg A$ (Il a surtout eu en retour beaucoup d'incompréhension mais après l'avènement de l'informatique et de disciplines comme la correspondance de Curry-Howard, l'intuitionnisme a connu un regain d'intérêt).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • christophe c
    christophe c
    @CPL: j'essayais de répondre de la manière la plus ciblée possible à la question HISTORIQUE posée. On prouve CLASSIQUEMENT en quelques lignes qu'on peut prouver intuitionnistement cette existence. Mais la preuve intuitionniste est ultra longue. Ça permet d'avoir "un sens accepté". Enfin tout dépend comment on exprime le problème. Foys signalé ded exemples où l'énoncé intuitionniste n'a même pas la valeur de vérité totalement vraie ou totalement faux.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Champ-Pot-Lion
    Champ-Pot-Lion
    Christophe, est-ce que la preuve standard de "pour tout jeu à deux joueurs, information partielle, etc., il existe une stratégie gagnante pour l'un des deux" est intuitionniste ? J'imagine que oui, c'est un algorithme tout-à-fait explicite, sans oracle. Il suffit alors d'appliquer cette preuve aux échecs. Si ensuite on "exécute l'algorithme" (par élimination de coupures j'imagine), on trouve une preuve démesurément longue puisque c'est l'algorithme effectif pour les échecs, d'accord, mais on n'est pas obligé de le faire.

    Pour comparer, dans la preuve non intuitionniste de "il existe deux nombres irrationnels $a$ et $b$ tels que $a^b$ est rationnel", si on veut transformer ça en algorithme, on doit utiliser un "oracle" qui dit si un nombre est rationnel ou non.
    (La preuve : Supposons que $\sqrt{2}^{\sqrt{2}}$ soit irrationnel. Dans ce cas, $\left(\sqrt{2}^{\sqrt{2}}\right)^{\sqrt{2}} = 2$, qui est rationnel, convient.)
  • christophe c
    christophe c
    Non elle ne l'est pas, c'est juste A ou nonA pour les énoncés dans un modèle fini. Après tout dépend comme tu traduis le truc évidemment. Sauf erreur. Mais en tout cas quznd je t'ai répondu je ne confondais pas la complexité avec la longueur des preuves intuitionnistes.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 19

AmadouRescassolVassilliabiguine_equationzeste +14 Invités