Le 27.10.2012 14:00, Une Bévue a écrit :
> Le 27/10/2012 09:43, Lavau Gerard a écrit :
>> Le raisonnement par l'absurde est un des principes utilisés en logique
>> classique, partiquée dans la grande majorité des mathématiques.
>>
>> Cependant, il existe des alternatives. La logique intuitionniste
>> rejette le raisonnement par l'absurde, et il en est de même de
>> l'analyse constructive. Ces domaines sont cependant marginaux.
>
> OK, merci bien, c'est ce que j'avais intuité.
> MAIS, comme il est montré sur la page wikipedia, le raisonnement par
> l'absurde dérive du principe du tiers exclu. disons que c'est oui on non.
>
> En logique intuitionniste je dirais que non oui n'équivaut pas à non.
> Ou "non non" (double négation) n'équivaut pas à oui.
>
> Mais bon, quand est il de la théorie de la démonstration dans le cas
> intuitionniste, puisque le tiers n'est pas exlu ?
La théorie de la démonstration a connu des développements
particulièrement fécond dans un cadre intuitionniste (ce n'est
rien de le dire !), voir par exemple le logiciel Coq.
Pour une introduction :
http://perso.ens-lyon.fr/alexandre.miquel/habilitation/intuitionnisme.pdf