Par l'absurde : obligatoire ou facultatif ?

Très rapidement : oui. Enlever le raisonnement par l'absurde revient à raisonner entièrement en logique intuitionniste, et il y a beaucoup de résultats démontrables classiquement non démontrables intuitionnistement, tout ça est bien étudié.

Lupulus : le théorème des valeurs intermédiaires est-il un enoncé plausible ? :-D ou encore l'existence de fonctions non continues, ou même non dérivables ?

Je peux me tromper, mais il me semble que d'Alembert-Gauss : "tout polynôme non constant à coefficients dans $\C$ admet une racine" ne peut être démontré sans raisonner par l'absurde.

La logique intuitionniste réfute

Non, c'est juste que AC=> logique classique. Mais logique intuitionniste $\subset$ logique classique de toute façon.

La non non traduction ne marche bien que pour le propositionnel ou alors il faut taper trop fort, si on veut l'obtenir au dessus. D'ailleurs il n'est pas très pertinent de parler de non non traduction: le bon théorème qui signifie quelque chose de profond est le suivant:

Théorème pertinent:
Toute proposition terminant** par $\perp$ qui est prouvable classiquement (ie en logique intuitionniste + RPA) est prouvable intuitionnistiquement.


Par contre, il est vrai que les questions posées ci-dessus sont trop vagues, puisque ça dépend de l'énoncé choisi pour représenter le slogan et des axiomes admis "en arrière-base" sinon, à peu près rien d'intéressant en maths classiques n'est prouvable intuitionnistiquement.

** Terminaison de (A=>B) := Terminaison de B
** Terminaison d'un énoncé qui n'est pas une implication := lui-même.

Merci pour ta réponse, Martial.
N'ayant jamais étudié la logique ou les méta-mathématiques (?) (autrement que les "bases" nécessaires qu'on voit en L1, s'entend), je me demande : existe-t-il des théorèmes qui affirment quelque chose comme "le théorème toto ne peut être démontré (dans ZFC, disons) que par l'absurde" (ou que par contraposée ou ...) ?

Déjà, merci pour la réponse, Maxtimax.
Ensuite, aurais-tu un exemple (quitte à le vulgariser un peu) pour un novice dans le domaine comme moi (juste par curiosité) ?

@Maxtimax : selon moi la démo du théorème du buveur repose plutôt sur la disjonction des cas :
Soit tous les habitants de l'univers picolent, auquel cas l'implication est toujours vraie, donc tu peux choisir x arbitrairement.
Soit il y en a au moins un qui ne boit pas, et ce x convient.
Dois-je en déduire que la disjonction des cas est équivalente au RPA ou au tiers exclu ?

J'ai peu de disponibilités, pardon de ne me connecter que maintenant.

1/ Il a été dit et je le redis, que la plupart du temps (et non pas parfois) deux énoncés claissquement équivalents ne sont pas intuitionnistiquement équivalents. Donc, ça n'a pas de sens de poser une question comme "le théorème de Machin est-il intuitionniste?" si on ne précise quel énoncé formel on souhaite évoquer par "le théorème de Machin"

2/ Tout théorème classique a une version substantiellement disant la même chose (je ne dis pas équivalent) sur le fond qui est intuitionniste. La LI est beaucoup plus riche et contient dans sa quantité d'informations la LC. Le théorème "dit de Statman", qui est en fait un exercice évident, dont j'ai donné la preuve (je peux la redonner sur demande elle est courte) plusieurs fois sur le forum dit que la logique classique est co-NP complète et que la logique intuitionniste est PSPACE-complète, et ce même si on se retreint au langage propositionnel qui ne contient que le signe implique et des lettres. (Remarque: je ne parle bien sûr que des versions propositionnelles puisque qu'au premier ordre la non calculabilité est la règle)

3/ Presque tous les théorèmes de mathématiques sont NONPROUVABLES en logique intuitionniste quand on prend leur forme disons la plus usuelle. Donc Michael, tire au sort à peu près comme tu veux un énoncé tu as une proba proche de 1 qu'il ne sera pas intuitionnistiquement prouvable dès lors que tu en prendras "nue version usuelle avachie" (c'est à dire, en général celles qui sont choisies pour avoir un énoncé guilleret, sympathoche et concis). Exemple: A ou (non A), théorème de maths s'il en est qui n'est pas intuitionniste, ou encore (non(nonA))=>A

4/ Il faut faire attention quand on parle de raisonnement par cas:

4.1/ Le "raisonnement par cas" n'est rien d'autre que l'utilisation de l'axiome:

$$ ((X\to A)\wedge (Y\to A))\to ((X\vee Y)\to A)$$

qui est intuitionniste, mais qui n'est QUASIMENT jamais utilisé seul!

4.2/ Il est en effet, le plus souvent JUSTE APRES avoir obtenu classiquement, mais non intuitionnistiquement $X\vee Y$, dans l'optique de continuer en disant "donc $A$"

4.3/ Donc dire "nous avons fait un RPC" n'est pas renseignant en soi.

5.1/ Tout ce que je viens de dire n'a en fait qu'une valeur très relative: en effet, les maths propositionnelles (sans les variables liées et les quantificateurs) ne sont pas en question quand des gens échangent sur un forum à propos de "théorèmes usuels". Or "les théorèmes usuels" sont pour les gens, même si officiellement exprimés comme théorèmes de ZF(C), des énoncés du 2e, 3e, and so on, ordre. L'exemple archi-académique est celui des anneaux: la théorie des anneaux est bien évidemment un bête et méchante théorie du premier odre, mais elle est la plupart du temps vécue, bousculée, retournée, aimée, détestée, exploitée, répudiée, etc, comme une théorie du deuxième ordre.

5.2/ Il suit que s'interroger sur l'intuitionnisme formellement et s'interroger sur des petites parties de raisonnement locales ne donnera PAS DU TOUT les mêmes réponses. Par exemple, on ne peut pas prouver que $\{0;1\}$ muni de l'ordre $0<1$ est un bon ordre de manière intuitionniste, mais la TOTALITE de $(Peano, \to , \forall )$ intuitionniste est PARFAITEMENT équivalente à $(Peano, \to , \forall)$. Simplement, on aura la farfeluité de commencer un chapitre 1 peu populaire (au sens non pas inintéressant, mais exotique) où on prouve par récurrence les propriétés évidentes du signe $=$

5.3/ Au niveau de la recherche, il y a comme beaucoup de familiers de ce forum savent, l'outil topos (qui singe ZF intuitionniste) qui est à la mode, avec l'inconvénient, là encore "en pratique" qu'on ne peut y parler que des phrases avec des quantificateurs bornés, qui sont justement celles qui sont officieusement "sans quantificateurs" en TDE habituelle. Autrement dit, on a deux ensembles presque disjoints de préoccupations, celles des théoriciens, analystes, infinitistes, cohérentistes, indécidabilistes d'une part, et celles des algébristes et géomètres abstraits d'autres part.

Les premiers ont jusqu'ici plutôt mis le phare sur ce qui n'est pas prouvable dans ZF ou ZFC, quand les autres ne se sont intéressés qu'à ce qui est DEJA PROUVE dans ZF, ZFC, mais ne l'est pas avec uniquement des raisonnements intuitionnistes

6/ Pour prouver qu'un truc n'est pas prouvable (préoccupation typiquement dans le post de Michael), en fait, de la même manière qu'avec Godel, on ne le prouve pas, on prouve un truc plus faible de la forme: "SI telle théorie est consistante ALORS tel truc n'est prouvable que classiquement MAIS PAS intuitionnistiquement"

7/ Le buveur, signalé par Martial est sitrctement compris entre la logique classique et la logique intuitionniste. Pour le voir, c'est très simple: il est vérifié topologiquement** par tous les bons ordres, alors que la logique classique implique topologiquement* qu'un bon ordre ne contient que 2 éléments


voili voilou, en espérant avoir comblé la curiosité de tous.

** je rappelle ce que sont les logiques classique et intuitionniste par un processus qui n'est pas à prendre au sérieux "complètement ici", mais qui permet d'être consis et particulièrement adapté aux interrogations précises des posteurs du présent fil:

a/ Ensemble de vérité = topologie
b/ A et B := interieur de (A inter
c/ A ou B := A union B
d/ $\forall i: A_i$ := interieure de l'instersection des $A_i$
e/ $\exists i: A_i $ := union des $A_i$
f/ (A implique := union des ouvert X tels que (A inter X) est inclus dans B
g/ non(A) := intérieur du complémentaire de A

h/ Se situer intuitionnistiquement, c'est ne rien supposer sur la topologie
k/ Se situer classiquement, c'est supposer que non(non(A)) = A pour tout ouvert A (exercice ça force un cadre $\{vrai; faux\}$)
m/ La topologie sur un ensemble ordonné est celle engendrée par les intervalles ouverts
t/ Le buveur équivaut demander que l'ordre soit un bon ordre (ou bien fondé, pas le temps d'y rfléchir, mais trancher est évident en 5mn)

N'hésitez pas s'il reste des questions. Et si au bout d'une semaine je ne réponds pas n'hésitez à m'envoyer un MP, ma boite est cassée mais je reçois une notif par mail

J'ai sauté une étape, pardon, je laisse les lecteurs la trouver, ça leur apportera plus qu'à moi, je mets la correction en blanc

De mon téléphone: en fait j'ai répondu à ta demande mais tu l'as peut être pas vu. Quand tu peux construire un espace topologique où ta phrase est un ouvert différent de l'espace entier elle n'est pas un théorème intuitionniste. Vois si tu peux le faire pour le buveur par exemple et si besoin de détail je te les donnerai d'un PC. (J'ai donné les espaces qui vérifient le buveur)

michael : :-S je te donne un théorème dont je t'affirme qu'il n'est pas démontrable sans tiers exclu et tu me demandes si il existe un théorème de la forme "le théorème toto n'est pas démontrable sans tiers exclu", tu dois reconnaître que c'est bizarre :-D
Mais pour te satisfaire, voilà un énoncé : "Le théorème du buveur n'est pas démontrable sans tiers-exclu".

Il ne s'agit d'ailleurs pas d'un méta-théorème, mais "juste" d'un théorème: on se donne un système de déduction (typiquement si on veut un truc facile à manier calcul des séquents, déduction naturelle, et si on veut un truc plus primitif, demandant moins d'encodage, on prend des trucs que christophe saura mieux décrire que moi du type "le plus petit ensemble de mots sur $V\cup\{\to\}\cup ...$ contenant patati et stable par patata"), un énoncé; on montre que si on ajoute une règle de déduction du type $\frac{}{P\lor \neg P}$, $T$ est dérivable (par exemple en le dérivant), et que si on ne l'ajoute pas il ne l'est pas : rien de plus mathématique (et non pas métamathématique) comme preuve.

OK. Merci pour vos réponses.
Je ne pensais pas que les-dits théorèmes portant sur la "prouvabilité" de théorèmes dans tel système d'axiomes/théorie (?) s'énonçaient aussi simplement.
Pardon pour le dérangement.

Plutôt que modifier, http://www.les-mathematiques.net/phorum/read.php?16,1743292,1744628#msg-1744628 et post précédent, je fais un ajout, d'autant que j'ai écrit que je mets le truc en blanc et me suis déconnecté avant de le faire, de sorte qu'en le mettant dans un post plus bas, c'est un peu comme du "mis en blanc":

Supposons $non(B)$, où $B:=Buveur$.

Soit $a$.
Begin
$~~$Soit $x$.
$~~$Si non$(R(x))$ alors $B$.
$~~$Donc $non(non(R(x)))$
End
donc $\forall x: R(x)$
donc $R(a)\to \forall xR(x)$
donc B

Je rappelle aussi, même si c'est peu distingué dans le monde estudiantin courant qu'un :
vrai et profond raisonnement par l'absurde fera à un moment ou un autre usage de : $$

(A\to (A\to )\to (A\to

$$ dans un truc de la forme : $$

(X\to Tout)\to ((X\to Tout)\to Tout)

$$ pour obtenir : $$

(X\to Tout)\to Tout

$$ et en déduire $X$.
Si, par contre, on obtient "de manière directe" $(X\to Tout)\to Tout$ et qu'on en déduit $X$, bien "qu'officiellement" un RPA, il ne s'agit que d'un transfert (une permutation des adversaires dans un jeu).

Par contre, quand, après que Jules ait battu, en jouant simultanément contre Lea ET contre Bob, au moins un de ses deux adversaires, on déduit qu'il "PEUT" battre Lea, en jouant "uniquement contre elle" (sous les hypothèses que tout le monde joue parfaitement bien), on fait appel à la puissance de Zeus pour lancer la "foudre sur Lea".

Dans le cas du buveur c'est vraiment typique. C'est un "vrai et profond" RPA qui l'attrape.

On peut le voir comme suit aussi: supposons que : $$

\forall u,v,z: [R(u,v)\vee R(v,z)]

$$ et montrons que : $$

\exists x\forall y: R(x,y).

$$ Contre Lea, je joue $a$, elle répond $b$. Je me sers de ce $b$ pour le jouer sur la table de Bob, qui répond $c$. Du fait que $R(a,b)\vee R(b,c)$, j'ai gagné une des parties.

Par contre, contre Lea seule, quand je vais jouer $r$, et qu'elle va répondre APRES par $t$, j'ai intérêt à ne pas me rater si je veux gagner, ie si je veux $R(r,t)$.

Le jeu est incommensurablement plus difficile pour moi, face à Lea seule, que si on me demande juste de battre un des deux adversaires parmi Lea et Bob.

Le buveur est un cas particulier de ça avec $R(x,y):= (S(x)\to S(y))$.