tiers exclu
Répondre à la discussion
Affichage des résultats 1 à 17 sur 17

tiers exclu



  1. #1
    ilelogique

    tiers exclu


    ------

    Bonjour
    Wikipédia affirme sur la page du tiers exclu que celui-ci équivaut au raisonnement par l'absurde,
    je vois bien que le tiers exclu est nécessaire pour faire une preuve par l'absurde mais le contraire est-il si sûr ? comment on le prouve ?
    Mais surtout svp : on dit souvent que nier le tiers exclu a pour conséquence que toutes les preuves sont constructives, savez-vous comment on prouve ça svp ?
    Est-ce qu'on ne devrait pas appeler "constructivistes" les "intuitionnistes" ?
    merci,

    -----
    S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une

  2. #2
    Médiat

    Re : tiers exclu

    Il y a plusieurs courants constructivistes (tous reposent sur la logique intuitionniste), l'intuitionnisme (Brouwer) est l'un de ces constructivismes
    Je suis Charlie.
    J'affirme péremptoirement que toute affirmation péremptoire est fausse

  3. #3
    ilelogique

    Re : tiers exclu

    ok donc l’intuitionnisme est un des courants constructivistes lesquels reposent tous sur la logique intuitionniste (donc, visiblement il ne faut pas confondre l'intuitionnisme avec la logique du même nom). Mais pour mes 2 autres questions svp ? Merci.
    S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une

  4. #4
    GBZM

    Re : tiers exclu

    Bonsoir
    En logique intuitionniste on démontre (raisonnement par l'absurde pour ) à partir de l'hypothèse (tiers exclus pour ).
    est un théorème en logique intuitionniste. Donc à partir de l'hypothèse (raisonnement par l'absurde pour ) on déduit (tiers exclus pour ).
    Il y a une petite subtilité parce qu'on ne peut pas déduire le tiers exclus pour () de l'hypothèse du raisonnement par l'absurde pour ().

  5. A voir en vidéo sur Futura
  6. #5
    Deedee81
    Modérateur

    Re : tiers exclu

    Salut,

    Attention de ne pas tout mélanger. Il existe des logiques multivaluées (donc pas avec tiers exclu) et la démonstration par l'absurde reste possible (aménagée, évidemment, mais le principe reste le même : faire une hypothèse, découvrir une contradiction, et conclure). Et ce qu'on peut faire avec les démonstrations dépend évidemment du choix des axiomes.

    De même, il ne suffit pas de nier le tiers exclu pour que toutes les preuves soient constructives. On peut très bien même dans ce cas avoir une preuve d'existence sans construction explicite.

    Bien noter qu'il existe toutes sortes de logiques multivaluées (logiques modales, logique floue et même en informatique comme pour le prolog où une variable peut être vraie, fausse ou "non définie")

    C'est juste une remarque générale car il est clair que la question concerne la logique intuitionniste auquel il y a eut réponse
    "Il ne suffit pas d'être persécuté pour être Galilée, encore faut-il avoir raison." (Gould)

  7. #6
    GBZM

    Re : tiers exclu

    Citation Envoyé par Deedee81 Voir le message
    faire une hypothèse, découvrir une contradiction, et conclure
    Supposer A, en déduire l'absurde et conclure à non A, ce n'est pas techniquement un raisonnement par l'absurde.
    Le raisonnement par l'absurde, c'est supposer non A, en déduire l'absurde, et conclure à A. Ceci revient à prendre comme axiome.

    des logiques multivaluées (donc pas avec tiers exclu)
    Une logique multivaluée peut avoir le tiers exclu : par exemple si elle est à valeurs dans une algèbre de Boole.
    Dernière modification par GBZM ; 20/09/2023 à 08h47.

  8. #7
    Deedee81
    Modérateur

    Re : tiers exclu

    Citation Envoyé par GBZM Voir le message
    Supposer A, en déduire l'absurde et conclure à non A, ce n'est pas techniquement un raisonnement par l'absurde.
    C'est pour ça que j'ai dit "aménagé" Mais j'ai peut-être un peu abusé.

    Citation Envoyé par GBZM Voir le message
    Une logique multivaluée peut avoir le tiers exclu : par exemple si elle est à valeurs dans une algèbre de Boole.
    Ah oui, bien vu, là pour le coup c'est moi qui ait fait une confusion. Je devrais être plus prudent dans ce forum
    "Il ne suffit pas d'être persécuté pour être Galilée, encore faut-il avoir raison." (Gould)

  9. #8
    ilelogique

    Re : tiers exclu

    ok merci GBZM, très intéressant ! (j'ai mis un peu de temps...)

    donc le tiers exclu (TE) ne se déduit pas du raisonnement par l'absurde (RA) en logique intuitionniste ; mais peut-être que oui en logique classique ?

    Wikipédia n'est donc pas juste, ou je me trompe ?

    Et puis quid de mon autre question svp ? Le côté forcément constructiviste de la logique intuitionniste ? Car s'il me semble qu'en théorie des types on raisonne plus en termes de "il existe une preuve de F" plutôt que F est vraie dans tel modèle (hou la, est-ce que je dis est "vrai" ?...), ce qui permet de répondre à ma 2e question, mais est-ce aussi le cas pour la logique intuitionniste en général ?

    Alors ok Deedee81 répond à ma 2e question : nier le TE n'implique pas que les preuves soient constructives, merci.

    Mais je croyais que "les" logiques intuitionnistes étaient celles justement qui niaient le TE.

    Merci
    S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une

  10. #9
    Deedee81
    Modérateur

    Re : tiers exclu

    Rien n'empêche d'avoir les deux.
    "Il ne suffit pas d'être persécuté pour être Galilée, encore faut-il avoir raison." (Gould)

  11. #10
    ilelogique

    Re : tiers exclu

    quels deux ? je ne comprends pas.
    S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une

  12. #11
    Deedee81
    Modérateur

    Re : tiers exclu

    Citation Envoyé par ilelogique Voir le message
    quels deux ? je ne comprends pas.
    Le constructivisme ET le tiers exclu

    J'ai donné des exemples de logique qui nient le TE mais ne sont pas la logique intuitionniste (c'est la liste donnée dans Wikipedia)
    EDIT mais à confirmer vu que j'ai tatouillé entre "multivalué" et "tiers exclu"
    Dernière modification par Deedee81 ; 20/09/2023 à 10h56.
    "Il ne suffit pas d'être persécuté pour être Galilée, encore faut-il avoir raison." (Gould)

  13. #12
    GBZM

    Re : tiers exclu

    Citation Envoyé par ilelogique Voir le message
    donc le tiers exclu (TE) ne se déduit pas du raisonnement par l'absurde (RA) en logique intuitionniste ; mais peut-être que oui en logique classique ?
    Tu ne m'a pas compris. J'ai bien indiqué que c'était subtil, mais peut-être n'ai-je pas été assez clair.
    Tout d'abord évacuons le cas de la logique classique. Tiers exclus et raisonnement par l'absurde sont tous deux des théorèmes (ou des axiomes, ça dépend de la présentation) donc déduire l'un de l'autre en logique classique ne fait pas vraiment sens.
    Revenons à la logique intuitionniste
    Si à la logique intuitionniste on ajoute l'axiome de raisonnement par l'absurde pour toute proposition , alors on a le tiers exclu, c.-à-d. que est un théorème pour toute proposition . On est en fait alors en logique classique.
    Par contre, on ne peut pas déduire de en logique intuitionniste.
    Cette subtilité se voit peut-être mieux si on pense en termes de sémantique ; pour avoir une sémantique correcte et complète pour le calcul propositionnel intuitionniste, on peut prendre les valeurs de vérité dans le treillis des ouverts d'un espace topologique . Le vrai est , le faux est , le "ou" est l'union et le "non" l'intérieur du complémentaire. Ainsi est l'intérieur de l'adhérence de (je me permets de confondre une proposition avec sa valeur de vérité). Dire que est vrai, c'est dire que est ouvert-fermé. Dire que est vrai, c'est dire que est un ouvert régulier (égal à l'intérieur de son adhérence).
    Bien sûr, un ouvert régulier n'est pas forcément fermé . Mais par contre si dans un espace topologique tous les ouverts sont réguliers, alors tous les ouverts sont fermés (je te laisse faire cet exercice de topologie générale). Vu la subtilité ?

  14. #13
    GBZM

    Re : tiers exclu

    Citation Envoyé par Deedee81 Voir le message
    Rien n'empêche d'avoir les deux, le constructivisme ET le tiers exclu
    À mon avis tout l'empêche, un constructivisme n'admettra jamais le tiers exclus. Bien sûr, dans certaines situations le constructiviste admet des instances de tiers exclus ; par exemple, si m et n sont entiers on a m<n ou m=n ou m>n même pour un constructiviste. Mais le tiers exclus comme axiome logique pour toute proposition, ça jamais.

  15. #14
    Deedee81
    Modérateur

    Re : tiers exclu

    Citation Envoyé par GBZM Voir le message
    À mon avis tout l'empêche, un constructivisme n'admettra jamais le tiers exclus. Bien sûr, dans certaines situations le constructiviste admet des instances de tiers exclus ; par exemple, si m et n sont entiers on a m<n ou m=n ou m>n même pour un constructiviste. Mais le tiers exclus comme axiome logique pour toute proposition, ça jamais.
    C'est vrai et ils le disent aussi dans wikipedia
    Mais il serait faux de dire "pas de tiers exclu" => constructivisme
    "Il ne suffit pas d'être persécuté pour être Galilée, encore faut-il avoir raison." (Gould)

  16. #15
    ilelogique

    Re : tiers exclu

    Ok merci,

    bon je peux me tromper mais je vois plus le TE presque comme une règle de déduction (de nonnonA je déduis A par exemple)

    je veux dire que vous êtes sur du métalangage (puisque vous quantifiez sur les propositions) en proposant une sorte de "schémas d'axiomes"

    Mais oui je n'ai pas encore compris votre subtilité, je crois comprendre : aux axiomes de la logique intuitionniste (LI) vous ajoutez tous les axiomes de RA (pour chaque énoncé) et de ça se déduit le théorème TE mais vous dite qu'on est en logique classique ensuite ? Pas compris

    plus haut quand vous avez écrit (et là je pensais avoir saisi !) vous parties d'un théorème de la LI : nonnon(A ou nonA) puis RA pour (A ou nonA)

    Enfin par la sémantique, je dois creuser pour comprendre.que les valeurs de vérité ne sont pas booléennes mais prises dans le treillis d'un espace topologique, je dois aller revoir mes cours mais ça me semble intéressant,

    merci et pardon si je suis confus
    S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une

  17. #16
    GBZM

    Re : tiers exclu

    Citation Envoyé par ilelogique Voir le message
    bon je peux me tromper mais je vois plus le TE presque comme une règle de déduction (de nonnonA je déduis A par exemple)
    Cette règle de déduction, c'est le raisonnement par l'absurde (RPA). Si on veut le TE sous forme de règle de décuction, ça peut être "si je déduis B de H et A et je déduis aussi B de H et non A, alors je déduis B de H".
    mais vous dite qu'on est en logique classique ensuite ? Pas compris
    Je dis simplement que logique intuitionniste + RPA pour toute proposition A = logique classique

    vous partie(z] d'un théorème de la LI : nonnon(A ou nonA) puis RA pour (A ou nonA)
    Oui, c'est exact : en logique intuitionniste, le TE pour A se déduit du RPA pour (A ou non A) car nonnon(A ou non A) est un théorème intuitionniste.

  18. #17
    ilelogique

    Re : tiers exclu

    ok merci ça m'a aidé,
    me vient une question tout de même : si le TE n'est pas un critère de constructibilité, y a-t-il des théories axiomatiques (les types peut-être ?) qui, par construction si je puis dire, soient nécessairement constructives ?
    merci.
    S'il n'y avait pas de vérité absolue, "toute vérité est relative" en serait une

Discussions similaires

  1. La loi du tiers exclu
    Par invite8ad835bc dans le forum Science ludique : la science en s'amusant
    Réponses: 18
    Dernier message: 18/10/2015, 16h03
  2. Besoin de tiers exclu ou pas
    Par invited647b3e7 dans le forum Mathématiques du supérieur
    Réponses: 10
    Dernier message: 14/08/2015, 20h15
  3. Elève exclu du groupe du voyage en Espagne
    Par phil80 dans le forum Enseignement : le forum des enseignants
    Réponses: 23
    Dernier message: 15/06/2010, 22h47
  4. Une theorie cohérente et compléte induit le tiers exclu ?
    Par invite6754323456711 dans le forum Mathématiques du supérieur
    Réponses: 10
    Dernier message: 08/03/2009, 20h48