Raisonnement par l'absurbe

[Médiat]

Suite aux errements d'un autre fil sur le sujet, je préfère en ouvrir un autre pour répondre à la question initiale :

Je me demandais s'il existe un théorème ou un axiome qui dit que tous ce qu'on peut démontrer par l'absurde est démontrable par voie directe ?

Il me semble que l’on peut comprendre cette question d’au moins trois façons différentes :

1. Le raisonnement par l’absurde (réduction à l’absurde et détour par l’absurde étant strictement la même chose en logique classique) est-il nécessaire à la logique classique, ou peut-on le remplacer systématiquement par une démonstration directe.

2. Le raisonnement par l’absurde (réduction à l’absurde, souvent abrégée en RAA) est-il nécessaire à la logique intuitionniste, ou peut-on le remplacer systématiquement par une démonstration directe.

3. Le détour par l’absurde est-il nécessaire aux mathématiques, ou, dit autrement, est-ce que la logique intuitionniste permet de démontrer tout ce que peut démontrer la logique classique.

Je ne répondrai pas à la question N° 2, je laisse ce soin à un spécialiste de l’intuitionnisme qui aurait du temps à lui consacrer.

Pour la question 3, il existe une traduction de Gödel qui permet de transformer toute démonstration classique d’un théorème classique en une démonstration intuitionniste d’un théorème intuitionniste, c’est une façon de répondre à la question 3.

Ci-dessous, il ne sera plus question que de logique classique.

Cette question porte bien sur l’utilité/nécessité du raisonnement par l’absurde en logique classique, et non sur son caractère intuitif, plaisant, ou facile à enseigner (ou alors il faut supprimer l’implication, car je ne crois pas qu’il soit facile à faire comprendre (et ce n’est pas le pire exemple) que [« La tour Eiffel fait moins de 850 mètres de haut » implique « La tour Eiffel fais moins de 800 mètres de haut »] est vraie).

La logique classique est définie par des schémas d’axiomes (il en existe plusieurs jeux possibles, plus ou moins bavards), en choisissant correctement ce jeu, on y trouve un axiome de raisonnement par l’absurde (un schéma donc) qui est la seule différence avec la logique intuitionniste, or à partir de ces schémas d’axiomes on peut prouver le tiers exclu (p ou non p) pour toutes les propositions, si cela était possible sans l’axiome du raisonnement par l’absurde, on pourrait faire de même en logique intuitionniste, ce qui est manifestement faux, il existe donc au moins une démonstration qui nécessite le raisonnement par l’absurde en logique classique.

Signé : un imbécile de logicien formaliste, qui ne répondra pas à ceux qui voudront s’amuser à pourrir ce fil en y important un autre débat.

PS : il n'y a pas de faute de frappe dans le titre, mais un hommage à Gotlib.
-----

[invite6754323456711]

La logique classique est définie par des schémas d’axiomes (il en existe plusieurs jeux possibles, plus ou moins bavards), en choisissant correctement ce jeu, on y trouve un axiome de raisonnement par l’absurde (un schéma donc) qui est la seule différence avec la logique intuitionniste, or à partir de ces schémas d’axiomes on peut prouver le tiers exclu (p ou non p) pour toutes les propositions, si cela était possible sans l’axiome du raisonnement par l’absurde, on pourrait faire de même en logique intuitionniste, ce qui est manifestement faux, il existe donc au moins une démonstration qui nécessite le raisonnement par l’absurde en logique classique.

Très intéressent. j'aurai quelques questions de compréhension.

A partir de ces schémas d’axiomes on peut prouver le tiers exclu (p ou non p) pour toutes les propositions.

Donc le tiers exclu est un théorème (en logique classique) ?


Si il existe un schéma d'axiome appelé raisonnement par l’absurde. il y a t'il équivalence alors entre le schéma d'axiome appelé raisonnement par l’absurde et le "théorème" du tiers exclu (peut on remplacer l'un par l'autre dans la liste des schémas d'axiomes) ?

Le formalisation en langage des prédicats du schéma d'axiome de raisonnement par l’absurde est ((Non P ==> faux) ==> P ) ?

Patrick

[invité576543]

Bonjour,

(Et merci de lancer ce fil)

Je n'arrive pas à comprendre comment on peut avoir à la fois :

il existe une traduction de Gödel qui permet de transformer toute démonstration classique d’un théorème classique en une démonstration intuitionniste d’un théorème intuitionniste

et

il existe donc au moins une démonstration qui nécessite le raisonnement par l’absurde en logique classique.

Si on prend la démonstration évoquée par la seconde phrase et qu'on lui applique la transformation évoquée dans la première, qu'obtient-on?

Cordialement,

[Médiat]

Si on prend la démonstration évoquée par la seconde phrase et qu'on lui applique la transformation évoquée dans la première, qu'obtient-on ?

Bonjour,

J'ai bien écrit
démonstration classique d’un théorème classique --> démonstration intuitionniste d’un théorème intuitionniste.

C'est à dire que le théorème obtenu en logique intuitionniste n'est pas exactement le même que celui de la logique classique (il y a des (non non p) à la place de certains p).

Cordialement,

[A voir en vidéo sur Futura]

[invité576543]

J'ai bien écrit
démonstration classique d’un théorème classique --> démonstration intuitionniste d’un théorème intuitionniste.

J'avais bien lu, je voulais une confirmation de l'idée et en particulier des différences entre les théorèmes.

C'est à dire que le théorème obtenu en logique intuitionniste n'est pas exactement le même que celui de la logique classique (il y a des (non non p) à la place de certains p).

Ce qui répond très bien à ma question.

---

Cela me permet de poser une question incidente, sur la contraposition (ce qui peut être considéré comme un hors-sujet). Me trompe-je (c'est fort possible) en disant que si une démonstration classique utilise la contraposition, la transformation en "intuitionniste" procède comme suit :

passer de (A => B) à (¬B => ¬A) reste tel quel, et

passer de (¬A => ¬B) à (B => A) est transformé en passer de (¬A => ¬B) à (¬¬B => ¬¬A)

(Dans ce que je lis il est plus couramment écrit qu'accepter toute contraposition demande d'accepter le tiers exclu, mais je ne vois pas pourquoi.)

Cordialement,

[Médiat]

passer de (¬A => ¬B) à (B => A) est transformé en passer de (¬A => ¬B) à (¬¬B => ¬¬A)

(Dans ce que je lis il est plus couramment écrit qu'accepter toute contraposition demande d'accepter le tiers exclu, mais je ne vois pas pourquoi.)

Si pour toutes propositions
(¬A => ¬B) permettait de déduire (B => A) , en remplaçant B par ¬¬A, on obtient
(¬A => ¬¬¬A) permet de déduire (¬¬A => A), or la première proposition est toujours vraie (même en logique intuitionniste) et la dernière proposition est un axiome de raisonnement par l'absurde (qui entraîne le tiers exclu).

[invité576543]

il existe donc au moins une démonstration qui nécessite le raisonnement par l’absurde en logique classique.

Est-ce que la loi de Pierce, pourrait être un bon candidat?

La démonstration par l'absurde est simple : si on suppose à la fois et non A, on obtient A.

Wikipédia indique que la loi de Pierce implique le tiers exclu, du coup j'imagine qu'il n'y a pas de démonstration directe pour cette loi. Est-ce correct?

Cordialement,

[Médiat]

Est-ce que la loi de Pierce, pourrait être un bon candidat?

Il me semble bien que oui, mais plus simplement le tiers exclu rempli bien ce rôle aussi et pose le même problème : ce sont des schémas d'axiomes ; et donc pour trouver un "vrai" exemple, il faudrait une vraie proposition (donc dans un langage particulier, et pour une théorie particulière. Et alors se posera la question de savoir si la version classique et la version intuitionniste sont bien "différente", mais là, le débat risque de déraper).

[leon1789]

Il me semble bien que oui, mais plus simplement le tiers exclu rempli bien ce rôle aussi et pose le même problème : ce sont des schémas d'axiomes ; et donc pour trouver un "vrai" exemple, il faudrait une vraie proposition (donc dans un langage particulier, et pour une théorie particulière. Et alors se posera la question de savoir si la version classique et la version intuitionniste sont bien "différente"

Un exemple serait peut-être, si j'ai bien compris, << deux fonctions sont égales ou différentes. >>
Avec tiers exclu, c'est évident. Sans tiers exclus...

[invité576543]

Il me semble bien que oui, mais plus simplement le tiers exclu rempli bien ce rôle aussi et pose le même problème : ce sont des schémas d'axiomes ; et donc pour trouver un "vrai" exemple, il faudrait une vraie proposition (donc dans un langage particulier, et pour une théorie particulière.

Préliminaire : si on reprend la question originale et que l'on accepte dans "démonstration directe" une démonstration utilisant le tiers exclu ou la contraposition au sens du passage de non(B)=>non(A) à A=>B, la réponse est manifestement "oui".

Donc on peut s'intéresser à la question avec "démonstration directe" voulant dire "démonstration n'utilisant pas le raisonnement par l'absurde ou toute méthode connue pour y être équivalente".

Du coup, effectivement l'exemple le plus simple est une proposition selon le schéma du tiers exclu, et mettant en jeu un infini.

Proposition (vu sur un site, et une variante simplifiée de la proposition de Léon), basée directement sur le tiers exclu:

En arithmétique, montrer que pour toute suite a_n d'entiers, la proposition suivante est vraie



Cordialement,

[Médiat]

En arithmétique, montrer que pour toute suite a_n d'entiers, la proposition suivante est vraie

Exemple qui nécessite de démontrer que cette proposition n'est pas démontrable dans l'arithmétique de Heyting (version intuitionniste de Peano).

PS : Je ne connais pas suffisament la logique intuitionniste pour aller plus loin dans ce domaine : dont acte.

[invité576543]

Exemple qui nécessite de démontrer que cette proposition n'est pas démontrable dans l'arithmétique de Heyting (version intuitionniste de Peano).

Bon. Au minimum on a là un exemple de propriété telle que la démonstration directe, si elle existe, n'est pas facile à trouver et doit être, en toute vraisemblance, bien plus compliquée à suivre et à accepter que la démonstration invoquant le tiers exclu () ou une forme de raisonnement par l'absurde, non?

Cordialement,

[invite7863222222222]

Bonjour,

j'ai l'impression que c'est peut-être seulement les problèmes posés sur des ensembles de cardinal supérieur au cardinal des nombres entiers qui ne peuvent se passer de raisonnements par l'absurde. Faudrait pouvoir trouver un contre exemple.

[invité576543]

j'ai l'impression que c'est peut-être seulement les problèmes posés sur des ensembles de cardinal supérieur au cardinal des nombres entiers qui ne peuvent se passer de raisonnements par l'absurde.

Je comprends cela aussi.

Si on se limite au fini, il me semble qu'il y a toujours une démonstration directe, par exhaustion.

Par exemple, montrer que pour les suites finies soit aucun terme n'est nul, soit il y a au moins un terme nul, peut se faire par récurrence : si taille nulle, alors aucun terme n'est nul; si taille n>0 : si le premier terme est nul alors il y a un terme nul, sinon on applique le résultat sur la suite privée de ce terme.

Mais cette approche ne marche pas pour une suite de taille infinie.

Cordialement,

[Médiat]

A partir de ces schémas d’axiomes on peut prouver le tiers exclu (p ou non p) pour toutes les propositions.

Donc le tiers exclu est un théorème (en logique classique) ?

Une proposition n'est pas intrinsèquement un axiome ou un théorème, cela dépend du jeu d'axiomes choisi.

[invite6754323456711]

1. Le raisonnement par l’absurde (réduction à l’absurde et détour par l’absurde étant strictement la même chose en logique classique) est-il nécessaire à la logique classique, ou peut-on le remplacer systématiquement par une démonstration directe.

Si on part des axiomes logiques des Principia Mathematica : http://fr.wikipedia.org/wiki/Axiome_logique

Je n'ai pas l'impression que dans les 6 schémas d'axiomes il y ait le schéma d'axiome de raisonnement par l’absurde.

Il est pourtant écrit :

Gödel a prouvé un théorème de complétude qui affirme que ces six schémas d'axiomes et ces deux règles de déduction suffisent pour obtenir toutes les lois logiques.

Donc on a pas besoin du schéma d'axiome raisonnement par l’absurde ?

Patrick

[Médiat]

Je n'ai pas l'impression que dans les 6 schémas d'axiomes il y ait le schéma d'axiome de raisonnement par l’absurde.

J'ai bien écrit dès le premier message qu'il y avait plusieurs jeux d'axiomes possibles, l'important étant qu'ils soient équivalents en ce sens que les axiomes de l'un doivent être des théorèmes de l'autre et vice-versa.

Personnellement je préfère le jeu suivant (plus court) :




Jeu auquel il faut ajouter la règle d'inférence modus ponens et, éventuellement les axiomes pour le quantificateur et la règle d'inférence qui lui est liée, la généralisation.

Or, avec ce jeu, l'axiome 3 est un axiome de raisonnement par l'absurde.


[HS]
Je viens de tester Google et de m'apercevoir avec étonnement qu'une recherche sur absurbe donne 3 310 000 de pages et une recherche sur absurde donne 3 350 000. Ceux qui n'ont pas compris mon PS du message #1 vont avoir du mal à trouver la réponse sur le NET
[/HS]

[ericcc]

En latin on comptait déjà "absurbe condita..."

[invite986312212]

Par exemple, montrer que pour les suites finies soit aucun terme n'est nul, soit il y a au moins un terme nul, peut se faire par récurrence : si taille nulle, alors aucun terme n'est nul; si taille n>0 : si le premier terme est nul alors il y a un terme nul, sinon on applique le résultat sur la suite privée de ce terme.

mais c'est marrant parce que le principe même de la démonstration par récurrence, je le vois comme très proche de la démonstration par l'absurde: on conclut que la propriété est vraie pour tout entier parce que sinon il y aurait un plus petit entier pour lequel elle serait fausse, etc.
alors une fois qu'on accepte le principe de la démonstration par récurrence, et même qu'on l'érige en axiome (est-ce bien cela?), on ne fait peut-être plus référence explicitement au tiers exclu, mais n'est-ce pas un peu fallacieux?
est-ce que les intuitionnistes acceptent la preuve par récurrence?

[invité576543]

est-ce que les intuitionnistes acceptent la preuve par récurrence?

Je ne sais pas pour le cas général, mais il me semble que le cas proposé entre dans une catégorie acceptable.

La démonstration par récurrence sur les entiers est constructive. C'est juste un "résumé" de la preuve qui est finie et répétitive pour chaque valeur de n.

En finitiste, N n'est pas un ensemble, la preuve par récurrence ne porte pas sur un ensemble infini, elle porte sur tout entier, sur tout cas qu'on voudra bien soumettre à la preuve.

Autre manière de voir, la preuve est faisable par un programme qui termine en un temps fini qu'on peut indiquer à l'avance une fois donnée la longueur de la suite. (Ce n'est pas le cas pour une suite infinie.)

Cordialement,

[invite7863222222222]

Mais cette approche ne marche pas pour une suite de taille infinie.

Oui d'ailleurs, je dirais qu'on pourrait le faire, mais qu'elle serait inutile concrètement puisqu'on ne pourrait pas la mettre en pratique.

[invite6754323456711]

vont avoir du mal à trouver la réponse sur le NET

il existe une réponse ? c'est donc décidable ?

Patrick

[leon1789]

est-ce que les intuitionnistes acceptent la preuve par récurrence?

oui sans problème

EDIT : mince, déjà répondu... disons que je confirme

[invite6754323456711]

il existe une réponse ? c'est donc décidable ?

Patrick

La logique classique est définie par des schémas d’axiomes (il en existe plusieurs jeux possibles, plus ou moins bavards), en choisissant correctement ce jeu, on y trouve un axiome de raisonnement par l’absurde (un schéma donc) qui est la seule différence avec la logique intuitionniste, or à partir de ces schémas d’axiomes on peut prouver le tiers exclu (p ou non p) pour toutes les propositions, si cela était possible sans l’axiome du raisonnement par l’absurde, on pourrait faire de même en logique intuitionniste, ce qui est manifestement faux, il existe donc au moins une démonstration qui nécessite le raisonnement par l’absurde en logique classique.

Cela suffit donc


En logique classique le principe de non-contradiction semble équivalent au tiers exclu ce qui n'est pas le cas en logique intuitionniste.

Ce qui est démontrable à partir du tier exclu en logique classique n'est-il pas démontrable à l'aide de non-contradiction en logique intuitionniste ?

Patrick

[invite6754323456711]

ou alors il faut supprimer l’implication, car je ne crois pas qu’il soit facile à faire comprendre (et ce n’est pas le pire exemple) que [« La tour Eiffel fait moins de 850 mètres de haut » implique « La tour Eiffel fais moins de 800 mètres de haut »] est vraie).

Cet exemple est pédagogique.

Si la tour Eiffel fait 900 mètres cette démonstration reste valide. Ce n'est pas la vérité de A ou B qui importe mais bien A ==> B

Maintenant l'implication classique n'est pas l'implication intuitionniste, qui n'est pas l'implication linéaire. Or tout les axiomes utilisent l'implication.

Personnellement je préfère le jeu suivant (plus court) :

Mais pour démonter

démonstration classique d’un théorème classique --> démonstration intuitionniste d’un théorème intuitionniste.

De quelle implication est-il question ?

Patrick

[leon1789]

Cet exemple est pédagogique.

Si la tour Eiffel fait 900 mètres cette démonstration reste valide. Ce n'est pas la vérité de A ou B qui importe mais bien A ==> B

Comment justifiez-vous [A ==> B] si ce n'est pas en parlant de la valeur de vérité de chaque proposition A et B ???

[Médiat]

De quelle implication est-il question ?

Je ne suis pas certain de comprendre la question, mais en logique classique on utilise l'implication classique et en logique intuitionniste, l'implication intuitionniste.

[invite6754323456711]

Je ne suis pas certain de comprendre la question, mais en logique classique on utilise l'implication classique et en logique intuitionniste, l'implication intuitionniste.

démonstration classique d’un théorème classique --> démonstration intuitionniste d’un théorème intuitionniste.

C'est :

- de l'implication en rouge
- mais aussi des équivalences entre les implications utilisées en logique classique pour formaliser les axiomes et celles de la logique intuitionniste par exemple

Patrick

[Médiat]

démonstration classique d’un théorème classique --> démonstration intuitionniste d’un théorème intuitionniste.

C'est :

- de l'implication en rouge

Ce n'est pas une implication, c'est une correspondance, faire une implication entre une proposition d'une logique et une proposition d'une autre logique ressortirait à une méta-logique.

- mais aussi des équivalences entre les implications utilisées en logique classique pour formaliser les axiomes et celles de la logique intuitionniste par exemple

Même remarque

[invite6754323456711]

démonstration classique d’un théorème classique --> démonstration intuitionniste d’un théorème intuitionniste.

C'est :

- de l'implication en rouge
- mais aussi des équivalences entre les implications utilisées en logique classique pour formaliser les axiomes et celles de la logique intuitionniste par exemple

Patrick

En fait dans quelle logique se place la démonstration de Gödel ? Est-ce cohérent pour démontrer une implication entre deux logiques de se placer dans une ou l'autre logique ? ne faut-il pas utiliser une troisième logique indépendante des deux autres ?

Patrick