tiers exclu

[ilelogique]

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,
-----

[Médiat]

Il y a plusieurs courants constructivistes (tous reposent sur la logique intuitionniste), l'intuitionnisme (Brouwer) est l'un de ces constructivismes

[ilelogique]

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.

[GBZM]

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 ().

[A voir en vidéo sur Futura]

[Deedee81]

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

[GBZM]

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.

[Deedee81]

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é.

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

[ilelogique]

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

[Deedee81]

Rien n'empêche d'avoir les deux.

[ilelogique]

quels deux ? je ne comprends pas.

[Deedee81]

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"

[GBZM]

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é ?

[GBZM]

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.

[Deedee81]

À 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

[ilelogique]

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

[GBZM]

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.

[ilelogique]

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.