constructivisme

christophe c · October 2011

J'ouvre un fil séparé pour continuer d'y mettre mes réponses éventuelles puisqu'il m'est reproché d'avoir été trop long dans le fil --> http://www.les-mathematiques.net/phorum/read.php?3,698123,700034#msg-700034

De sorte que si j' éprouve le besoin de contester un truc qui y est dit, je mettrai juste un lien vers le présent fil, ce qui rendra l'autre fil concis.

christophe c · October 2011

J'ai nettoyé l'autre fil des mes interventions trop longues et tout copié-collé dans un fichier avec des numéro de références.

les contester.

christophe c · October 2011

Je résume la conversation qu'on vient d'avoir avec Henri Lombardi dans l'autre fil (lien à mettre)

Henri Lombardi est une personne qui a écrit un gros livre d'algèbre commutative effective. et le fil en lien correspond à son envie de faire partager cette aventure et de témoigner de ses motivations.

HL a donc annoncé et mis en liens plusieurs fichiers pdf qui peuvent être ou non des extraits de son livre, ou des extraits d'articles dans des IREM ou des revues scientifiques ou philosophiques qui expliquent ou vantent un certain choix épistémologique concernant les mathematiques et leurs axiomatiques.

Il y a deux parties essentiellement distinctes qui sont ressorties de ses annonces et qui composent les contenus des documents qu'il a mis ou auxquels il fait référence:

1) une partie mathématique effective
2) une partie plaidoyer pour la valeur ou le bien fondé ou la naturalité ou la pertinence d'un mouvement philosophique ou d'une axiomatique.

Je suis un grand admirateur en même temps que quelqu'un qui s'intéresse assez (bien que je n'en sois pas un spécialiste) à la théorie des anneaux. La partie (1) ne me pose aucun problème et je l'ai dit plusieurs fois en rouge.

J'ai souhaité m'opposer très vivement (mais en tout "bien tout honneur" comme on dit souvent) à la partie (2) que je qualifierai (sans accuser nulle part et personne de mauvaise foi) de publicité mensongère (mais dans un sens bien sûr léger et "mondain" du mot "pub mensongère", personne ici ne vend rien et nous sommes des matheux qui papotent)

Dans la partie (2) on a pu lire de la part de HL, des choses comme:

2.1) telle théorie est formidable (bon ça, c'est gentil et inoffensif), mais aussi que:
2.2) "les logiciens ont découvert que" suivi de tout un tas d'informations que je considère comme scientifiquement et mathématiquement complètement inexactes quand elles étaient précises (ou alors il manquait un truc ou une hypothèse pour les rendre exactes), de nature à tromper le lecteur un peu novice qui veut se faire une idée quand elles étaient floues.
2.3) J'insiste bien sur le fait que HL est quelqu'un de probablement tout à fait honnête qui a annoncé ça avec enthousiasme et qui s'est appuyé sur des choses qu'il avait lues et comprises dans un sens qui correspondait probablement à ses propres options philosophiques.
2.4) Techniquement parlant, j'ai pu lire dans ce qu'il disait les choses suivante:
2.4.1) que les théories en question sont faibles (pour aller vite, j'appelle "ces" théories essentiellement une théorie qu'il a lui-même appelée "CZF"), donc qu'elles sont fiables, donc non pseudocontradictoires, mais qu'elles sont la vertu d'entrainer les maths ordinaires (ie ZF) quand on leur ajoute le tiers exclus.
2.4.2) qu'elles livrent systématiquement des algorithmes pour chacune de leurs preuves et qu'elles sont naturelles et faciles à pratiquer
2.4.3) que les logiciens ont mis en lumières des théorèmes profonds qui justifieraient tous ces dires
2.4.4) Qu'elles utilisent la logique intuitionniste ordinaire (c'est à dire la logique classique MOINS le tiers exclus) d'une manière conforme à ce que n'importe quel logicien intuitionniste définit comme tel et qu'il n'y a pas "d'initiation" spéciale ou d'option spéciale "logique" à comprendre en plus ou en différent (en dehors des axiomes propres) qui serait le fondement de maths appelées "maths constructivistes" et qui auraient été principalement inventées par un certain Bishop.
2.4.5) Que "les logiciens" auraient découverts "des gaps" qui se situeraient en gros entre Peano et l'analyse réelle nettement plus infiniste qui tiendraient à prouver que le tiers exclus est assez inoffensifs pour les théories faibles (Peano et cie) et très très problématique dès que les théories devienennt plus fortes.
2.5) Que ZF est bien trop peu fiable et bien trop risquée d'être inconsistante et qu'il (HL) recommande et préfère faire des maths constructivistes qui afficheraient les vertus et les garantis ci-dessus citées.
2.6) Que le programme de Hilbert serait ressuscité, que finalement "Poincaré" avait raison, etc, etc

Mon objectif (et c'est vrai que je n'ai probablement pas été clair car j'en ai posté des tartines) a été de dire qu' à peu près tout ce que je viens de rapporter techniquement (le point (2.4) ) est essentiellement ou bien faux, ou bien sans signifcation car trop flou, ou bien de nature à induire en erreur assez importante un lecteur amateur mais assez intéressé pour s'investir). Et j'ai essayé de dire pourquoi tout au long de mes questions posées dans le fil.

J'insiste bien sur le fait que presque chaque point 2.X décrit ci-dessus est presque "essentiellement faux" et non pas seulement "il en existe au moins". Et que ceci n'a rien à voir avec de la philosphie.

Pour ce qui est de la philosophie, j'estime totalement et je respecte totalement les positions des uns et des autres et je suis même "un peu" du même genre de bord que HL (ironie du sort) car je rève que ZF et même Peano soit contradictoire (pour moi si un jour quelqu'un prouve ça, ce sera un des plus beau jour de ma vie math et je considèrerai ça comme la plus belle découverte de maths jamais obtenue) et je pense que la correspondance de Curry Howard est une des grandes découvertes du 20ième siècle part2 qui livre un regard différent sur tout ça.

Pour les personnes "sceptiques" (c'est le rôle que j'ai essayé de jouer dans l'autre fil), je suis à leur disposition dans le présent fil pour répondre aux questions précises qui me seront posées en adoptant un statut de prouveur, mais je ne le fais que sur demande, ie je ne vais pas me lancer dans un gros exposé technique non sollicité.

Je précise juste un moment clé lors duquel j'ai pu donner l'illusion que finalement "je m'étais trompé" (je l'ai réellement cru), qu'il y avait bien eu une découverte "fondatrice" qui justifiait d'un coup toutes les annonces d'Henri (et même beaucoup beaucoup plus) et que j'étais passé à côté. C'est quand Bu (qui sans vraiment bcp intervenir semblait par ses petites interventions ciblées "soutenir" ou "cautionner") a posté une référence à un article de Friedman paru à annals of maths et vanté par le referee de l'époque Feferman qui a malencontreusement ou volontairement à des fins de pub, laissé trainé dans son rapport une phrase de nature à induire le lecteur en erreur.

Ca tourne autour du point 2.4.1 et de l'expression que j'ai utilisée "de nature à tromper le lecteur".

Il y a plusieurs théorèmes triviaux (des exos élémentaires de logique quasi-élémentaire) qui sont les suivants (j'insiste ce sont des trivialités syntaxiques pas des résultats profonds):

3.1) si une théorie intuitionniste devient contradictoire quand on lui ajoute le tiers-exclus alors elle est pseudocontradictoire en un sens parfaitement formelle qui est qu'elle nie démontrablement le schéma du tiers-exclus. Par conséquent aucune théorie intuitionniste ne peut "faire mieux" en un sens profond (au niveau des "certitudes" que la science cherche sur le monde) en terme "de fiabilité" qu'une théorie classique sauf à accepter de démontrer la négation du tiers exclus

3.2) aucune théorie intuitionniste n'est (contrairement aux théories classiques) vraiment "syntaxiquement contradictoire" dès lors qu'elle est un peu sérieuse et contient du second ordre (direct ou indirect) et des quantificateurs. Les seules théories intuitionnistes qui peuvent devenir "syntaxiquement contradictoire" sont celles qui entrainent propositionnellement l'énoncé "tout", et compte-tenu que le TE ne commute pas aux quantificateurs, il faut entre guillemets mettre exprès le paquet pour faire une théorie intuitionniste bêtement contradictoire

3.3) les points (3.1)+(3.2) entrainent que si un mathématicien sérieux annonce sur un forum que "la théorie T est noncontradictoire" et "représente les maths" et que c'est "cautionné par les logiciens" il sous-entend presque évidemment (pas forcément pour les experts, mais pour ses lecteurs amateurs qui ne doivent pas être trompés) que "les logiciens ont prouvé que T n'est pas pseudocontradictoire" (sinon, son annonce n'a aucun contenu et c'est une trivialité à cause du point (3.2))

3.4) S'il est tout à fait respectable de ne pas accepter le tiers-exclus comme axiome, il est plus engagé d'ajouter un axiome qui le nie ou de travailler dans une théorie qui démontre sa négation. Pour autant le tiers exclus peut paraitre sulfureux ou un axiome trop fort, pour autant, la preuve (irréfutable et incontestable!!!) de sa négation serait tout autant un évènement majeur dans les maths qui n'est encore jamais survenu . Il y a une différence entre "ne pas l'accepter" et "décreter sa négation".

3.5) Par conséquent, compte-tenu de l'annonce appuyée d'Henri que (3.1) pouvait avoir été cassé et compte-tenu que Bu, pour soutenir les dires d'Henri, a posté un rapport de referee "important" d'un article de Harvey Friedman dans lequel on peut lire en toutes lettres de la part de Feferman une phrase aussi ambigue sous la plume de Feferman (qui est quasiment texto la phrase d'Henri qu'à ce titre on peut considérer comme cautionné dans son annonce par Feferman (qui a eu tort, je parle de Feferman, d'écrire ça!!! Que ça ne fasse aucun doute), je veux absolument préciser que tout ceci est "du flan" publicitaire:

3.5.1) Rien de nouveau sous le soleil à ce niveau (HFriedman a juste prouvé la conservativité de certaines théories (qu'il a formalisées lui-même) ou dessus de certaines autres. Pour ça, il travaille tacitement dans ZF, en utilise toute la puissance, (en particulier l'existence de epsilon0) et soumet donc son résultat à la faillibilité de ZF (et pas qu'un peu car c'est de la subtile "recursion theory")
3.5.2) En aucun cas, ni Friedman ni un autre n'ont à ce jour prouvé ou donné la moindre indication que les théories faibles dont il est question sont pseudoconsistantes (non pesudocontradictoires)
3.5.3) En aucun cas on ne dispose d'un théorie fiable au sens de (3.1). Il n'y a que des théories plus fortes que d'autres, mais le classement est toujours relatif et ... effectué ou démontré dans une troisième théorie (à savoir ZF)
3.5.4) En aucun cas "les logiciens" ont découvert des choses de nature X ou Y à justifier ou à fonder plus qu'elle ne l'était dès le départ, en tant que théorie tout à fait respectable et "théorie d'auteur" (si j'ose dire) la théorie de Bishop
3.5.5) En aucun cas "un programme de Hilbert sur le point d'être réalisé ou je ne sais quoi d'incroyablement spectaculaire n'est une réalité scientfique qui "serait entrain d'être découvert par "les logiciens"
3.5.6) En aucun cas le th de Godel aurait été "mal compris" ou "sur le point d'être dépassé" (d'ailleurs qu'est-ce que ça veut dire dépasser le th de Godel????? c'est un théorème de maths, pas de physique ou de philo)
3.5.7) Et probablement (mais même sinon c'est un détail complètement vide de contenu), il n'y a pas un lien logique irréfutable qui ferait de ZF la théorie obtenue quand on ajoute le tiers exclus à une théorie constructiviste. Dans l'article de Friedman, il y a juste essentiellement deux théories (et en fait plus) qui sont comparées, dont on "peut dire si on veut" que l'une peut être considérée comme "une version respectable (pour certains!!) constructive de l'autre.

Maintenant, que ce soit clair, je suis friand et passionné par les maths que propose Henri. Mais les revendications fondatrices émises "en passant" et surtout les cautions prétendues de ces revendications au détour de ses discours dans l'autre fil, je les conteste.

Quant au point 2.4.5, que HL appelle "gap découvert par les logiciens", il ne s'agit (comme je l'ai bien répété 10 fois) que des fameuses difficultés qui surviennent dans le très général domaine "correspondance de Curry Howard " quand on essaie de prouver des théorèmes de fortes (ou faibles) normalisations à propos de systèmes plus riches que la logique propositionnelle (simi: th d'élimination des coupures présenté aux étudiants qui débutent un cursus de logique) ou que la logique propositionnelles du second ordre et l'arithmétique du second ordre (ce qu'on appelle l'analyse parfois) (théorème de forte normalisation du système F, de Girard).

Le point 2.4.4 mérite aussi une remarque concise: plusieurs post de HL (assez précis) tendent à faire penser que "constructivisme $\neq $ intuitionnisme, et l'addition de plusieurs de ses déclarations n'est pas limpide à cet égard car à un moment il dit à Bu (étonné): "mais Bu on se sert de la logique intuitionniste", mais à d'autre moment on n'a pas semble-t-il que $(0=0\to tout)\to tout$ car "l'égalité à zéro n'est pas une évidence... même pour zéro. Donc le constructivisme semble avoir une vie propre par rapport à "l'intuitionnisme".

christophe c · October 2011

4) Compléments sur les points 3.5.2 et 3.5.3 du post ci-dessus (au regard de 3.1): je ne suis pas un connaisseur en détails (et loin s'en faut) des théories qui ont été essayées pour "constructiviser" les maths. Par contre, j'ai été informé qu'il y a eu deux tendances:

4.1) des théories proposées par Brouwer qui de manière cash, ajoutaient des axiomes qui niaient l'axiome que j'appelle TE pour aller plus vite $\forall X( (non(nonX))$=>$X)$ (donc des théories pseudocontradictoires au sens de la définition du post précédent)
4.2) des théories proposées plus dans la lignée de Bishop, qui refusaient cette démarche et donc ne niaient pas intentionnellement dans leurs axiomes l'énoncé (du second ordre) TE.

Par contre: qu'en est-il de leurs théorèmes? Et bien tout simplement "suspens". On n'en sait rien. On "espère" juste (enfin je pense Bishop espère) que ces théories T n'ont pas la propriété que $T|---nonTE$, au même titre qu'on "espère" (pour certains? que ZF ne prouve pas tout)

PS: j'insiste que tout ceci ne remet aucunement en cause la profondeur et la valeur du livre et de la démarche de Henri (dont je lirai le livre avec grande curiosité et que je remercie pour cette immense somme), je voulais juste contrer ce que j'ai lu ou cru lire dans ses posts. A noter aussi que c'est bien moi qui "formalise" une part de ses propos, peut-être de manière infidèle, en particulier sur l'aspect (3.1)

christophe c · October 2011

Compléments:

5) je précise un peu pourquoi j'ai été si virulent (en plus de parfois devoir tromper des journées entières des douleurs physiques).

5.1 ) C'est parce que j'aurais rêvé que la version superlative de ma lecture des msg d'HL soit réelle (ie en fait ça a fait naitre des espoirs chez moi), d'où mon exigence apparente délirante de précisions

5.2) C'est parce que tout théorème (de quelque ordre logique que ce soit, premier second, infini-ième) de maths P est forcément tel qu'il existe $H_1,...,H_n$ des énoncés tels que

5.2.1) $H_1$=>($H_2$=>($H_3$=>(.....($H_n$=>P))....) est un axiome qu'on a décidé d'accepter formellement
5.2.2) Chaque $H_i$ est un axiome

je dis bien AXIOME et pas "évidence", ou autre chose, ie "AXIOME" cadire quelque chose qu'on a décidé (qui que ce soit qui fasse les axiomes, ie quelquesoit la théorie) d'admettre pérennement dans la théorie.

La seule condition de validité de (5.2) est de faire figurer les A=>((A=>B)=>B); (A=>B)=>((B=>X)=>(A=>X)); (A=>B)=>((X=>A)=>(X=>B)) + que les conjonctions (infinies) impliquent leurs items + $(\forall x(P\to Q))\to ((\forall xP)\to (\forall xQ))$, parmi les axiomes (ce que personne n'a jamais vraiment refusé) et ça s'applique à toutes les logiques.

En conséquence de quoi, il ne peut plus vraiment y avoir de "débats vraiment théoriques" sur des histoires de fondements, puisqu'on sait exactement quels sont les théorèmes d'une théorie quelle qu'elle soit (en gros des cas particuliers de ses axiomes).

Du coup, je suis "à l'affut" de tout indice qu'on aurait trouvé une sorte d'échappatoire: pourquoi? Parce que quand il y a un conflit entre des découvertes, leur mariage entraine des conclusions beaucoup plus fortes. (Par exemple, le modus ponens est l'aboutissement d'un conflit entre "A" et une sorte de négation affaiblie de A, à savoir A=>B, qui accouche de B.

christophe c · October 2011

6) Je contexte (5.2). Ceci n'a rien à voir avec tous les "elicut", bien au contraire, c'est la direction opposée (une des), qui consiste non pas à "déplier" une preuve, mais à la ... plier de telle sorte qu'elle ne contienne plus que "deux" phrases (qui peuvent être très longues).

Eliminer des coupures consiste entre autre à éliminer des utilisations d'axiomes. Là au contraire, on élimine des "enchainements" en les réinsérant comme vus dans les axiomes de la théorie quelconque. Cepedant, il y a une connexion entre les deux, et la forme "totalement pliée" (5.2) a paradoxalement l'avantage de décrire de manière uniforme "le graphe qu'on obtiendrait si on dépliait" et donne l'avantage de voir le théorème comme "plus que constructif" (puisqu'il est pointé comme cas particulier d'un axiome principal (5.2.1) où on gomme des "hypothèses transparantes" (5.2.2) )

Description:

6.1) Objectif mettre des flèches qui joignent les occurences dans (5.2.1) qui peuvent être prolongées pour les occurences négatives des (5.2.2)

6.1.1) face à A=>A: joindre les occurences négatives des variables du A vert à leur soeur jumelle du A bleu
6.1.2) face à un axiome logique , mettre les flèches naturellement (ie conformément à sa preuve en déduction naturelle) **
6.1.3) face à un autre axiome: l'admettre.

** exemple: (A=>B)=>((B=>X) =>(A=>X)) . Occurences intra positives dans le sens vert--->bleu, occurences intra négatives dans le sens bleu--->vert, ce qui donne:

christophe c · October 2011

En fait, je crois qu'il y a un "pont-aux-ânes" pour essayer de rendre les preuves le plus possible concrêtes. Il y a un petit lemme pas très excitant mais qui me semble représenter un défi à propos des suites à termes dans $\N^*$ qui la proproiété suivante: toute preuve trop courte ou trop constructives (les preuves connues sont courtes, mais pas assez courtes) entrainerait une contradiction dans ZF.

Définitions: On note T l'ensemble des suites à termes dans $\N^*$, ie l'ensemble $(\N^*)^\N$. Soit $(x,y)\in T^2$. On dit que $x>y$ (ce n'est pas une relation d'ordre!) quand il existe un entier p tel que $\forall i\leq p-1: x(i)=y(i)$ et $x(p)=y(p)+y(p+1)$ et $\forall i>p: x(i)=y(i+1)$ (quand p=0, la première condition est automatiquement vérifiée). On dit que x,y sont voisins quand $x>y$ ou $y>x$. On appelle chemin une suite finie $(e_1,..,e_n)$ d'éléments de T telle que deux termes consécutifs sont voisins, ie $e_i$ et $e_{i+1}$ sont voisins quand i est tel que ça a un sens. On appelle n-1 la longueur d'un tel chemin et "parité" du chemin la parité de sa longueur.

Lemme: tous les chemins joignant deux éléments de T ont même parité.

Problème: entre autres indices, il ne semble pas possible de remplacer vraiment $\N ^*$ par un semigroupe commutatif fini de même nature (ie qui puisse donner le même résultat)?

Lombardi Henri · October 2011

je réponds ici à un post que CC a mis je ne sais plus où

> @HL, ah bin voui, j'y pense comme tu disais que "le petit défi:
> prouver que tels anneaux ont un petit cardinal" n'était pas adapté,
> en voici un autre (que j'ai aussi mis avec une preuve non constructive
> dans "il est facile"): Soit A un anneau noethérien.
>
> On appelle idéal fortement premier un idéal P ayant comme propriétés que:
> 1) il est premier et
> 2) s'il contient une intersection (quelconque) d'idéaux
> (même infinie la famille intersectée) alors il contient un des
> idéaux de l'intersection.
>
> Prouver qu'il n'y a qu'un nombre fini d'idéaux fortement premiers dans
> un anneau noethérien. Bon là, la conclusion c'est avec le mot "fini"

Tu n'as pas l'air de te rendre compte qu'il ne s'agit toujours pas d'un résultat que l'on puisse qualifier de concret.
La condition 2) doit être reformulée pour qu'elle puisse être considérée comme "signifiant quelque chose de précis".
Par exemple une reformulation concrète de la noethérianité est: dans toute suite croissante d'idéaux de type fini, il y a deux termes consécutifs égaux.
Tu vois que cet énoncé utilise une quantification acceptable, i.e. une quantification sur les objets d'un ensemble acceptable:
pour toute suite croissante d'idéaux de type fini bla bla bla
cela revient à quantifier sur les suites d'éléments de l'anneau, entrecoupées d'un symbole spécial chaque fois que l'on passe à l'idéal suivant
c'est un peu compliqué, mais raisonnable

Toi tu proposes une définition où tu quantifies sur la classe des familles infinies d'idéaux. Ce n'est certainement pas un ensemble (même dans ZF ce n'est pas un ensemble, mais on peut se ramener à un ensemble dans ZF).

Donc tu vois toujours beaucoup trop grand.

Je suis tout prêt à croire qu'elicut fait souvent des choses intéressantes,
mais je crois que tu te trompes sur sa capacité à rendre constructives des choses qui ne le sont manifestement pas. Par exemple sauter au dessus du gap identifié par les logiciens
(et auquel j'ai l'impression que tu ne crois toujours pas).

Je prends un exemple de très bas niveau: un énoncé du type logique
Tout Existe Tout
sur les entiers. C'est vraiment pas méchant.
L'énoncé dit sur un cas précis qu'il est possible d'énumérer en ordre croissant les valeurs prises par une suite d'entiers
Prends une fonction primitive récursive f : N -> N dont l'ensemble de valeurs n'est pas récursif.
Considère l'énoncé suivant vrai en classique et indémontrable en constructif:
pour tout n, il existe m, tel que pour tout p on a
f(m) > f(n) et ( f(p) > f(n) => f(p) > ou = f(m))

Une preuve classique de cet énoncé est très facile,
tu pourras l'élicuter tant que tu voudras, tu ne fourniras pas
une preuve constructive du même énoncé,
tu obtiendras un énoncé "stupide", avec plein de négations,
équivalent à l'énoncé classique en mathématiques classiques,
et ne présentant aucun intérêt mathématique du point de vue constructif

Je suis par contre curieux de savoir ce que donnera ton elicut
pour des énoncés raisonnables d'algèbre abstraite, du type logique Tout Existe,
dont la démonstration constructive a demandé de sérieux efforts de décryptage.

ne serait-ce que les petits théorèmes matriciels que j'ai proposés

A+

leon1789 · October 2011

Henri,

que penser de mon amorce d'approche dans cette réponse ? http://www.les-mathematiques.net/phorum/read.php?3,698123,700731,page=17#msg-700731

ccnc · October 2011

Tu n'as pas l'air de te rendre compte qu'il ne s'agit toujours pas d'un résultat que l'on puisse qualifier de concret

C'est sûr, y a plus concret, mais "concret" est un mot controversable dans la mesure où les choses abstraites ont parfois bcp de solidité pour s'appliquer au concret

doit être reformulée pour qu'elle puisse être considérée comme "signifiant quelque chose de précis".

euuu, elle est formelle donc pas possible de faire plus précis. Par contre, tu voulais surement mettre le mot "concret" à la place de précis j'imagine

e suis tout prêt à croire qu'elicut fait souvent des choses intéressantes,
mais je crois que tu te trompes sur sa capacité à rendre constructives des choses qui ne le sont manifestement pas. Par exemple sauter au dessus du gap identifié par les logiciens

J'ai déjà répondu en détail à tout ça, Henri. Je veux bien te proposer une initiation plus progressive mais pas d'un cyber, j'ai essayé de concentrer dans plusieurs posts, mais peu nombreux de quoi il s'agit, tu ne sembles pas arriver à sortir des premières impressions que tu as eues lors de tes lectures initiales (et je te comprends ce n'est pas forcément facile, on peut y mettre une forme d'adhésion "affective"). Mais de facto, si tout ceci est parfaitement maitrisé et "dépassé" depuis les années 80.

Après tout dépend ce que tu appelles "constructiviste" car tu ne l'as jamais défini (et Bishop non plus, HF l'a fait à sa place apparemment?). Je comprends que cette volonté "de ne pas définir" soit une option philosophique respectable, mais justement on tombe ensuite sur des difficultés dans l'échange avec les autres qui finiront par se lasser que quand ils pointeront tel ou tel truc on leur réponde "ah mais non, ça oui, mais ça non" à la petit semaine "informelle".

Deja le terme "elicut" je l'emploie à dessein pour raisons "pédagogique" mais il s'agit "d'exécution de preuves" en termes techniques (précision sans importance ici, mais importante dans le domaine).

Par exemple sauter au dessus du gap identifié par les logiciens

Oulala, snif, je te l'ai dit, ça n'a rien à voir avec ce débat ce que tu crois avoir lu comme un gap.
Ce que tu appelles "gap" est une vulgarisation d'un mécanisme qui n'a strictement rien à voir avec des histoires de constructivisme vs classique ou d'intuitionnisme vs classique ou de cosntructivisme vs intuitioninsme. D'ailleurs, on peut "en vouloir" aux gars qui ont vulgarisé ça comme ça s'ils existent. (si ce n'est pas un résumé d'un résumé d'un résumé un peu perso de ta part

-D )
Ce "gap" dont "tu parles" est juste un terme "stylé" pour résumer les difficultés rencontrées pour la forte normalisation des systèmes expressifs (quelle que soit la logique sous-jacente, constructive, intuitionniste ou classique, ce n'est pas essentiellement lié, à part dans les définitions mathématiques du problème)

En tout état de cause, théories consistantes ou contradictoire (voire celle que j'ai implémenté dans caml dans l'autre fil), théories classiques ou intuitionnistes, théorie terriennes ou de martien, tous ces mécanismes sont parfaitement compris depuis 20-30 ans, en gros (et implémentés parfois (exemple l'excellent caml, par exemple, attention pas "COQ" qui est limitatif) et transforme tout arbre (classique avec axiome du choix Zorn, compréhension, etc et tout le tralala contradictoire que tu veux) en "graphe constructiviste" si j'ose dire (en tout cas parfaitement formellement intuitionniste)

Ce que tu crois être un gap via tes lectures n'a rien à voir: cela concernerait plutôt les difficultés liées aux questions de savoir si le graphe s'arrête ou non vu comme processus dynamique (bouclage, bouclages partiels, bouclages sains ou malsains), mais pas sa nature "intuitionniste" (qui est évidente).

Prends une fonction primitive récursive...

[size=x-large]

+

[/size]

Toi tu proposes une définition où tu quantifies sur la classe des familles infinies d'idéaux. Ce n'est certainement pas un ensemble (même dans ZF ce n'est pas un ensemble, mais on peut se ramener à un ensemble dans ZF).

donnent vraiment à penser (et effectivement, je l'ai lu dans ton pdf et aussi dans des extraits de discussion autour des iidées de Bishop) que tu adhères à une pétition de principe qui veut en gros se situer principalement dans le domaime des ensembles récursifs quand on fait des maths. Alors effectivement ça pose bcp de problèmes techniques et c'est "obsolète" (je déteste ce qualificatif qu in'est pas un argument) dans la mesure où plein de gens se sont "perdus" dans des méandres platoniciens à l'époque où c'était très étudié car c'est un sujet interminable et que la correspondance de Curry Howard a rendu complètement "maladroit d'aller s'y perdre" (entre les recursifs, les rec enumerables universels, pas universels, etc, bref tout le champ de laTuring-réduction et toute la complexité, c'est une vraie spécialité à part entière, on ne peut pas "décréter que ce serait bien d'être dans le récursif" comme ça juste pour philo)

En résumé: d'accord avec toi pour respecter que le constructivisme VEUT ne pas étudier des objets de trop grande complexité (les parties des parties de IR par exemple) et refuse de donner un sens à l'énoncé du défi. Pour l'heure je n'ai pas mieux en magazin

Par contre, pas trop d'accord que tu exptrapoles ça à l'affirmation que "certaines preuves ne s'exécutent pas". En effet, il faudrait que je rentre énoncé et preuve incriminés dans une moulinette (par exemple dans le prog caml que j'ai mis en lien dans l'autre fil pour prouver concretement que ca tourne et aboutit à une preuve de 3500 000 000 lignes qu'il faudrait que je pose ensuite sur le forum... hum hum)

Je ferai plutôt un post (mais pas ce soir) avec preuve irréfutable que ça marche à tous les coups (quand ça ne boucle pas), ie que ça marche à tous les coups (car les bouclages sont juste des circuits dans le graphe, mais c'est pénible à rattraper avec des pointeurs). Mais d'ores et deja tu peux me croire t'inquite (tout ceci est bateau depuis fort longtemps).

L'interet de demander à des hommes plutot qu'à des machines justement (d'où le defi de l'autre fil), c'est que quand une machine va de constructiviser la preuve en trois milliards de lignes, toi, ta créativité, etc, tu vas peut-être la constructiviser en 500 lignes, donc ma question ma paraissait légitime. Les constructivisation d'ojets finis me paraissent bcp moins intéressantes car de toute façon, c'est évident qu'elles sont grosso modo les preuves classiques légèrement trafiquées (j'ai deja dit pourquoi: si on prouve dans, même dans ZF***, qu'une équa diophantienne a une solution, on cherche la solution et quand on la trouve on obtient une preuve de l'existence d'une solution plus que constructive (un calcul d'enfant de 7ans, sauf si ZF "se trompe", ie prouve un truc "faux")

*** remplacer ZF par PEano ou n'importe quelle théorie en laquelle "tu as confiance"... L'important est donc non pas de constructiviser "à la main" des énoncés "concrets" (aussi difficile que ce soit, c'est juste la réalisation de l'évidence ci-dessus en remplacant la confiance par un calcul) mais plutot (enfin à mon gout et au gout des chercheurs qui essaient d'attacher des spécifications aux théorèmes de maths) de constructiviser des énoncés "abstraits" et "infinitistes"

Ce passage précédent répond aussi à

et ne présentant aucun intérêt mathématique du point de vue constructif Je suis par contre curieux de savoir ce que donnera ton elicut

Bin, ce qui est surtout intéressant c'est le processus. A la fin t'obtiens un truc attendu (un calcul qui rend "évident" la chose comme toute preuve de maths). Par contre le processus entame une sorte de danse de salsa avec les noeuds de la preuve initiale et élimine "progressivement" les utilisations des "non(non(A)=>A" jusqu'à les agglomérer sur les énoncés atomiques ou sur les interruptions logiciels (interventions du sceptique dans un jeu). Mais à l'arrivée tu serais deçu, t'obtiens juste une preuve... comme une autre.

Les preuves intéressantes sont celles qui génèrent de manière fine un bouclage partiel (ie un graphe avec des cycles)et dnt l'exécution ne termine jamais. Celles qui donne arbre-->arbre ne sont pas très bandantes, mais c'est une question de gout.

Comme je te l'ai dit dans un post controversé, cette activité peut vite edvenir une drogue au point que celui qui est en addiction peut se mettre à "trouver intéressant" des petits détails que tout un chacun ne voit pas. Il me semble que ton témoignage

dont la démonstration constructive a demandé de sérieux efforts de décryptage.

atteste que tu "vois" dans ça quelque chose qui prend vie. Mais si tu veux le publiciter, je te le répète, je ne suis pas sûr que c'est en constructivisant des trucs deja à 95% constructivistes et concrets que le "grand public" va le plus s'apercevoir du côté magique du phénomène. C'est plutot en constructivisant (exécutant) des preuves bourrées d'AC, de Zorn, de TE dans tous les sens que le spectacle fait ou ferait boum pour les gens. A ce titre ton idée d'effectiviser des exos d'anneaux est excellentissiiiiiiiiiiiiime car la théorie des anneaux est essentiellement une théorie du 3ième ordre

Mais comme tu n'es pas (encore?) conscient que toutes les preuves s'exécutent et croit que dès qu'on passe à P(P(IR)) on est dans les nuages

...

leon1789 · October 2011

ccnc écrivait:

> C'est plutot en constructivisant
> (exécutant) des preuves bourrées d'AC, de Zorn, de
> TE dans tous les sens que le spectacle fait ou
> ferait boum pour les gens.

Il me semble que c'est exactement ce que l'on peut lire dans ce livre de 1000 pages d'algèbre commutative de Lombardi et Quitté, en particulier concernant les modules projectifs de type fini et la théorie de la dimension de Krull http://hlombardi.free.fr/publis/couverture.pdf : ils ont mis à jour des constructions algébriques inhabituelles en math classiques, et pourtant complètement élémentaires (au sens logique du terme), jusqu'à donner assez souvent des relations polynomiales permettant des généralisations de résultats classiques

Lombardi Henri · October 2011

@CC

Citation (de moi Henri)

doit être reformulée pour qu'elle puisse être considérée comme "signifiant quelque chose de précis".

euuu, elle est formelle donc pas possible de faire plus précis.

réponse:
dans ma phrase le mot "signifiant" était la chose importante

pour moi la plupart des énoncés de ZF ne signifient rien de précis,
parce que ZF n'a pas de sémantique claire
être un énoncé de ZF est certes une chose extrêmement simple,
c'est sans doute ce que tu entends par: "pas possible de faire plus précis".

pour toi le mot "signifiant" est apparemment "vide de sens",
ou alors tu as une sémantique de ZF dans un coin de ta tête qui te permet de
penser que les énoncés de ZF écrits conformément à la syntaxe ont une "signification" précise

j'ai de plus en plus l'impression que notre discussion ne sert strictement à rien

j'ai néanmoins une bonne nouvelle:
un bon bouquin concernant la logique et le calcul, à paraître,
j'attache le pdf de la préface et de la table des matières

Proofs and Computations
Helmut Schwichtenberg (Munich) and Stanley S. Wainer (Leeds)
Series: Perspectives in Logic
Cambridge University Press
Hardback
(ISBN-13: 9780521517690)
Not yet published - available from January 2012

Driven by the question, 'What is the computational content of a (formal) proof?', this book studies fundamental interactions between proof theory and computability.
It provides a unique self-contained text for advanced students and researchers in mathematical logic and computer science.
Part I covers basic proof theory, computability and Gödel's theorems.
Part II studies and classifies provable recursion in classical systems, from fragments of Peano arithmetic up to Pi11–CA0.
Ordinal analysis and the (Schwichtenberg–Wainer) subrecursive hierarchies play a central role and are used in proving the 'modified finite Ramsey' and 'extended Kruskal' independence results for PA and Pi11–CA0.
Part III develops the theoretical underpinnings of the first author's proof assistant MINLOG.
Three chapters cover higher-type computability via information systems, a constructive theory TCF of computable functionals, realizability, Dialectica interpretation, computationally significant quantifiers and connectives and polytime complexity in a two-sorted, higher-type arithmetic with linear logic.

christophe c · October 2011

Je poste de mon tel

merci pour le livre. Non je ne pense pas que ZF ait du sens pas plus meme que 10 a la puissance 10000 en aitvrmt bcp non plus simplement sans t en rendre compte vrmt tout ce que tu dis a finqlement ete construit en raisonnant tacitement dans ZF

s il fallait tout detricoter il serait plutot difficile de demeler comment dire les eventuels virus cqches dans la masse de choses qu on connait des choses qui ne sont pas prejugees par des habitudes ensemblistes etc etc

ce qui gene dans ton positionnement philo c est que tu sembles attacher une espece de valeur platonique superieure a des trucs comme les entiers etc

quand tuparles de semantique par exemple tu sembles penser que ca a un sens alors que par essence meme de la semantique c est plus moins forcement ensembliste a la rigueur c est lq syntaxe qui pourrait tenter d echapper a l ensemblisme

si l histoire et les decouvertes avaient ete differentes si les entiers avaient une definition insensible a ZF par exemple alors si je serais plus adherent a tes positions mais cette facon de rejeter telles maths vs telles autres alors que les deux sont issues de la meme chose et surtout que lune les entiers dependent entierement de l autre me parait une position i.tenable philosophikment

tout ceci n est que conventions et de toutes facons les maths et leurs theoremes sont tjs enonces avec leurs hypotheses tacites ie les axiomes utilises dans leur preuve ecrits en encre blanche et petite il ny a pas de mystere juste un jeu de symboles dans les regles du jeu et je trouve pas assez fondee ton demi platonisme si on regarde la science tout entiere et tout particulierement la MQ a cote de laquelle les entiers ou ZF c kif kif la seule chose qui importe etant d etre clair precis et finalement tres formel dans l archivage des choses sures

christophe c · October 2011

A leon je viens de voir ton post telephone oblkge oui je n endoute pas je suis persuade de l immense interet du livre de HL

je participe meme a ma maniere du mieux que je peux a sa pub

je suis d autant plus un peu contrarie par les discours philosophiques qu il tient pour fonder son travail qui merite mieux que ca a mon avis on ne peut justifier de la science sure surtout ses propre s preuves tres effective sur un sujet generalement investique a coup de zorneries exploit plus que notable par des positions philosophiques non sures relativement "naives" ie peu actualisees par les chocs quantiques avec une sorte de selection arbitriare de statut platonique different pour les entiers ou les autres ensembles en toute volontaire ignorance de ce que la correspondance du cuho enseigne sur l irrealite de tout ca

samok · October 2011

Bonsoir

test d'envoi ... ok ça marche.
J'ai ressorti un livre que j'avais abandonné à la page 5, son petit nom est "Logique, ensembles, catégories. Le point de vue constructif" chez ellipses de P.Ageron.

voici mon trouble (un peu comme les trous noirs qui sont troublants) :
2.1 Principe du raisonnement par l'absurde.
Pour toute proposition $P$, $ non non P$ entraîne $P$.

-> ah, on me l'avait jamais dit comme ça ...

2.2 Théorème.
Les principes du tiers exclu et du raisonnement par l'absurde sont équivalents.

-> ah ? voyons la démo ...

Démonstration :
Admettons (TE) et cherchons à montrer (RA). On suppose donc $non non P$ et on tente d'en déduire $P$. D'après (TE), de deux choses l'une : soit on a $P$, et alors c'est terminé, soit on a $non P$, auquel cas on a une contradiction puisqu'on a supposé $non non P$.

-> j'arrête là pour la première implication parce que le monsieur il fait un raisonnement par l'absurde (qu'on m'a appris quand j'étais petit).

test d'envoi ... ok ça marche

1.2 Principe du tiers exclu.
Pour toute proposition $P$, on a $P$ ou $non P$

-> je vous laisse remettre dans l'ordre, simplement "avant" on me parlait des principes.

Exercices
Exercice 1.
a) Montrer en utilisant (TE), que pour tout réel $a \in [1,+\infty[$ l'équation $(1-a)x-sin(\sqrt{1-a})=0$ a au moins une solution réelle.
b) Montrer que dans le cas de l'équation $(1-a)x-sin(1-a)=0$, il est possible de le même résultat en se passant de (TE)

Solutions
1. a) Fixons $a\in [1,+\infty[$, le principe du tiers exclu permet d'affirmer : $a=1$ ou $a\neq 1$.

-> stop, honnêtement ça me dégoûte, quand j'étais plus grand $a \geq 1$ ça ressemblait à un prédicat pas à une proposition. Le mot proposition n'est par ailleurs pas défini (des fois qu'il y en aurait une autre (de définition)).

-> en fait j'ai continué ...

-> dans b) en résumé on prend $x_a=\lim_{x \rightarrow a} \frac{sin(1-x)}{1-x}$
avec comme remarque : cet exercice suppose qu'on ait développé la théorie des fonctions de variable réelle sans utiliser (TE).

Mais revenons à la suite de mon trouble (j'espère sincèrement que tu peines à lire ce post sieur cc, comme cela cela fera 1 partout).

2.3 Vrais et faux raisonnements par l'absurde.
...
Ainsi la démonstration bien connue de l'irrationnalité de $\sqrt{2}$, souvent malencontreusement présentée aux étudiants comme prototype de démonstration par l'absurde, n'en est pas une ;

-> ok, ok je comprends de plus en plus rien.

-> le clou final, enfin

2.4 Principe du raisonnement par contraposition.
Si $non Q$ implique $non P$, alors $P$ implique $Q$

-> on me l'avait présenté dans l'autre sens mais là je comprends, ce doit être une histoire de poupée russe qui quand elle dit $non non$ elle dit pas $oui$ mais $ouainh je veux rentrer chez ma môman$

PA a écrit:

La confusion entre raisonnement par contraposition et raisonnement par l'absurde est aussi une erreur fréquente. Mais celle-ci n'est pas très grave puisqu'on montre facilement :

2.5 Théorème.
Les principes du raisonnement par contraposition et du raisonnement par l'absurde sont équivalents.

-> fin du trouble, je ferme le livre, je suis trop con pour comprendre le constructivisme.

S

D. Hilbert · October 2011

Théorème.
Les principes du tiers exclu et du raisonnement par l'absurde sont équivalents.

-> ah ? voyons la démo ...

Démonstration :
Admettons (TE) et cherchons à montrer (RA). On suppose donc $\text{non }\text{non }P$ et on tente d'en déduire $P$. D'après (TE), de deux choses l'une : soit on a $P$, et alors c'est terminé, soit on a $\text{non }P$, auquel cas on a une contradiction puisqu'on a supposé $\text{non }\text{non }P$. \dots

Le fait de dire "On suppose donc $\text{non }\text{non }P$" montre que l'on utilise la méthode de l'hypothèse auxiliaire. Ensuite, l'auteur utilise le principe du tiers exlu : ce qui donne deux possibilité dont une mène à une contradiction. Dans ce dernier cas, l'on n'a en aucun cas utilisé le raisonnement par l'absurde. Il s'agit d'une méthode de démonstration qui ne fait intervenir que l'hypothèse de départ (ici $\text{non }\text{non }P$). C'est elle qui est en cause, ou, du moins, qui nous permet de conclure rapidement, vu que l'on aboutit à une contradiction. Aucun principe lié de près ou de loin au véritable raisonnement par l'absurde n'est utilisé. J'oubliais, il y a également la méthode de disjonction des cas qui est utilisée de manière tacite.

Ce ne sont là que quelques bribes bourbakistes citées de mémoire.

A +

Matsaya · October 2011

Ton problème samok, viens sans doute du fait que, comme la plupart des mathématiciens «classiques», tu confonds $P\Rightarrow ¬¬P$ et $¬¬P\Rightarrow P$.
Seul le premier est vrai pour les constructivistes, et s'appelle raisonnement par contradiction (si je ne dis pas de bêtises).

Démonstration. Soit $P$, on suppose $¬P$. On a alors $P\wedge ¬P$ ce qui est faux et donc notre hypothèse $¬P$ est fausse, autrement dit on a $¬¬P$.

Par contre, si on essaye de faire le raisonnement dans l'autre sens, on a soit :
1) Soit $¬¬P$, on suppose $¬P$ on arrive à une contradiction et on a alors $¬¬P$ (on tourne en rond).
2) Soit $¬¬P$, on suppose $¬¬¬P$ on arrive à une contradiction et on a alors $¬¬¬¬P$.

On a de même $¬P\Rightarrow ¬¬¬P$, etc.

Toute la subtilité vient que sans tiers exclu (ou vrai raisonnement par l'absurde), l'opérateur $¬$ n'est pas auto-inverse. On peut donc le rajouter par paire, mais pas forcément enlever des paires.

Par contre, comme le fait remarquer Léon plus bas, on a $¬¬¬P\Rightarrow ¬P$.
En effet, soit $¬¬¬P$. On suppose $P$ on a alors $¬¬P$ (ajout de deux $¬$), puis une contradiction avec $¬¬¬P\wedge ¬¬P$. $P$ étant absurde, on a finalement $¬P$.

leon1789 · October 2011

Matsaya écrivait:

> Toute la subtilité vient que sans tiers exclu (ou
> vrai raisonnement par l'absurde), l'opérateur $¬$
> n'est pas auto-inverse. On peut donc le rajouter
> par paire, mais jamais enlever des paires.

On peut enlever des paires de non, mais seulement à partir de 3 négations : non(non(non(P))) => non(P)

Lombardi Henri · October 2011

@ tout le monde

j'avais beaucoup aimé le livre de P. Ageron,
je vais devoir m'y replonger pour discuter

à part cela,
pour ceux qui s'intéressent aux théories formelles constructives "totalisantes" (genre CZF)
voici quelque chose qui pourrait plaire
je mets juste l'introduction de l'article

je mets la page web où je l'ai trouvé
et j'attache le pdf du papier pour ceux qui ont la flemme d'aller voir la page web

http://math.fau.edu/lubarsky/

CZF and Second Order Arithmetic,
Annals of Pure and Applied Logic, 141 (2006), pp. 29-34

Robert S. Lubarsky
Dept. of Mathematical Sciences
Florida Atlantic University Boca Raton, FL 33431, USA Robert.Lubarsky@alum.mit.edu
July 10, 2006

Introduction

CZF, Constructive Zermelo-Fraenkel Set Theory, is an axiomatization of set theory in intuitionistic logic strong enough to do much standard mathematics yet modest enough in proof-theoretical strength to qualify as constructive. Based originally on Myhill’s CST [10], CZF was first identified and named by Aczel [1, 2, 3]. Its axioms are:
• Pairing: ∀x,y∃z∀w w∈z↔(w=x∨w=y)
• Union: ∀x∃y∀z (z∈y ↔ ∃w(w∈x∧z∈w)
• Extensionality: ∀x, yx=y ↔ ∀z(z∈x↔z∈y)
• Set Induction (Schema): (∀x((∀y ∈ x φ(y)) → φ(x))) → ∀x φ(x)
• ∆0 Separation(Schema): ∀x∃y∀z z∈y ↔ (z∈x∧φ(z)), forφ a ∆0 formula
• Strong Infinity: ∃x [(∅ ∈ x)∧(∀y ∈ x (y∪{y}) ∈ x)∧∀z((∅ ∈ z ∧ ∀y ∈ z y ∪ {y} ∈ z) → z ⊆ x)]
• Fullness (AKA Subset Collection): ∀x,y ∃z ∀ R (if R is a total relation from x to y then there is a total relation R’ ∈ z from x to y such that R’ ⊆ R)
• Strong Collection (Schema): ∀x(∀y ∈ x ∃z φ(y,z) → ∃w (∀y ∈ x ∃z ∈ w φ(y, z) ∧ ∀z ∈ w ∃y ∈ x φ(y, z)).

Among Aczel’s accomplishments was an interpretation of CZF, and various extensions thereof, in Martin-Löf type theory, which established CZF as a predicative theory. As it turns out, CZF is proof-theoretically equivalent with Martin-Löf type theory ML1V, as well as KP (Kripke-Platek admissible set theory), ID (inductive definability), and a host of other identified theories. Such theories can arguably be considered to be the limit of predicative mathematics, allow for a philosophical justification as being constructive, and are in any case very much weaker proof-theoretically than ZF. For an overview, references, and some proofs, see [11].
It is a natural enough question to ask about the strength of variants of CZF. Michael Rathjen conjectured that adding full Separation to CZF elevates the theory’s strength from ID, which is a small fragment of Second Order Arithmetic, to full Second Order Arithmetic. In this note, this conjecture will be shown to be correct.
What is the value of such a result? It is certainly nicer if a theory is shown to be weak, in that one can then use that theory with fewer philosophical scruples. This is the case for instance in [2], see also [11], where it is shown that adding certain choice principles to CZF does not change the proof-theoretic strength. Still, knowing that CZF + full Separation has the strength of Second Order Arithmetic tells us at least that the former theory is not predicative, providing a warning to the constructively-minded mathematician not to work within it. In addition, the exact determination of this strength provides independence results. For instance, Rathjen ([12], prop. 7.12 (ii)) shows that CZF + Power Set is proof-theoretically stronger than nth Order Arithmetic for all n, from which it follows that CZF, being much weaker, does not prove Power Set. Similarly, it follows from the result in this paper that even with the addition of full Separation Power Set does not follow. (The latter result is re-proven model-theoretically in [8].) None of this should be surprising. Both the main result of this paper and the consequences just cited were anticipated by Rathjen (and perhaps others), and the ideas contained in the proof to follow are themselves mostly a reworking of those found in [1] and [11]. Still, at least now the results are formally established.

[3] Peter Aczel, The type theoretic interpretation of constructive set theory: inductive definitions, in R.B. Marcus et al. (eds.), Logic, Methodology and Philosophy of Science VII (North-Holland, Ams- terdam, 1986), p. 17-49

[10] John Myhill, Constructive set theory, Journal of Symbolic Logic, 1975, p. 347-382

[11] Michael Rathjen, The Strength of Some Martin-Löf Type Theories, Archive for Mathematical Logic, 1994, p. 347-385

Lombardi Henri · October 2011

dans l'introduction de l'article citée dans mon post précédent, il est question de prédicativité

la prédicativité est essentielle d'un point de vue constructif

Poincaré, qui n'avait pas mis le doigt sur le tiers exclu, avait mis le doigt sur la prédicativité
il considérait que la clef des mathématiques raisonnables (pour lesquelles la signification est claire, parce qu'elles ne se mordent pas la queue) était la prédicativité

c'est également la préoccupation essentielle de Martin-Löf dans sa théorie constructive des types

chez les gens de l'informatique théorique, il semble aussi que la prédicativité soit considérée comme la clé des sémantiques sérieuses

bref: on pourrait faire une pause sur la discussion du tiers exclu,
dont il semble qu'on ait fait au moins six fois le tour,
et discuter de la prédicativité ?

Quant à moi, je proposerais de s’en tenir aux règles suivantes :
1. Ne jamais envisager que des objets susceptibles d’être définis en un nombre fini de mots ;
2. Ne jamais perdre de vue que toute proposition sur l’infini doit être la traduction, l’énoncé abrégé de propositions sur le fini ;
3. Éviter les classifications et les définitions non-prédicatives.
Henri Poincaré, dans La logique de l’infini (Revue de Métaphysique et de Morale, 1909). Réédité dans Dernières pensées, Flammarion.

Encore un mathématicien d'une naïveté ridicule, n'est-ce pas ?

bisam · October 2011

Ce doit être l'apanage des personnes prénommées Henri... (:P)

christophe c · October 2011

De mon tel

sur ta last phrase j ai carrement envie de repondre oui il pensait a une epoque ou la mq n etait pas vrmt decouverte et ou la corcuho n etait meme pas une idee

comme le manifeste ton post d avant avec une liste d axiomes etudiee dans un article on est dans un grave contresens qui oppose une vision saine et sure a une vision philosophique qui n en finit pas de tourner en rond sur quoi admettre comme enonces qui ne seraient pas a justifier car entre guillemets acceptables

bien que ca donne lieu a d interessants exercices techniques ce nest plus pertinent depuis lontemps en dehors de debats philosophiques un peu etrangess

la suggestion qui me parait la plus de nature a induire les amateurs qui lisent en erreur est AVANT TOUT cette idee dangereuse que les axxiomes ne sont pas des hypotheses parfaitement presentes dans les theoremes de maths meme si telle ou telle convention les ecrit en encre blanche et petis caracteres ton "combat insistant suggere aux neophytes qu il n en irait pas ainsi et que les matheux seraient d etranges physiciens qui se disputeraient aussi sur une liste.de.lois de la nature abstraite ce qui est a mon avis super desinformant tu parles comme s il y avait encore au jourdhui des polemiques sur les fondements

je respecte tes volontes apparentes de rehabilitation des theories des types (predicativite etc) mais ca me parait dangereux de faire passer ca pour de relles recherches sur les fondements il sagit plus d amusements techniques aussi difficiles techniquement soient ils en part a la lumiere nouvelle de la corcuho

je rappelle que toutes les maths sont faites et simples dans la theorie contradictoire que j ai rappele ds l autre fil que les regles sont formelles et simples et qu une telle theorie n est pas typee

en termes pratiques tu confonds la recherche technique qui essaie graphe apres graphe de prouver que cui ci ou cuila est un arbre et la simplicite du passage de arbre a graphe dans la traduction en preuves constructives ou effectives des preuves quelconques

or cette recherche est interminable c est banalement celle autour de la calculabilite ie quels sont les programmes qu s arretent

ta position me fait un peu penser a celle des philo qui disent on ne peut utiliser un programme tant qu on n a prouve qu il termine ce qui met de drastiques limitations drqstiques mais aussi inutiles!!

Aujour d hui tu sais tres bine qu un programme interessant ne s arrete justement jamais tant que tun as pas tape "quitter windows et eteindre le pc" et vouoir etudier uniquement les algos entiers --->entiers c est vrmt se priver de pratiquement tous les raisonnements riches de la science

plus grave encore celui de vouloir eriger des interdits et de qualifier de «raisonnables» certaines maths au detriment de d autres

Matsaya · October 2011

@Leon1789, c'est corrigé, merci.

@Lombardi Henri, le «Ne jamais envisager que des objets susceptibles d’être définis en un nombre fini de mots» me paraît douteux si on ne veut pas se mordre la queue. Mais c'est peut-être une erreur naïve de ma part.

@Christophe, il y a quelque chose qui me dérange dans ton argumentation. Tu as dis une fois à Henri (en gros) que pour toi une théorie mathématique se devait d'être formelle en utilisant l'exemple de l'avion et en disant que tu ne voudrais pas monter dedans s'il n'était pas construit sur un système formel. Or tu dis d'autres part que le choix des axiomes n'est pas important tant qu'on l'explicite dans les preuves. D'un point de vu formel, je ne suis pas contre, mais d'un point de vue pratique, si je monte dans un avion je préférerai que le choix d'axiomes utilisés pour montrer qu'il vole est «philosophiquement sûr».

Je veux dire que si — par exemple — j'estime que AC est faux, mais AD vrai, je serais prêt à monter dans un avion AD, mais pas AC*.

* J'entends par là que la preuve que l'avion puisse voler sans risque soit obtenue en utilisant AC.

myrtille0 · October 2011

"Quant à moi, je proposerais de s’en tenir aux règles suivantes :
1. Ne jamais envisager que des objets susceptibles d’être définis en un nombre fini de mots ;
2. Ne jamais perdre de vue que toute proposition sur l’infini doit être la traduction, l’énoncé abrégé de propositions sur le fini ;
3. Éviter les classifications et les définitions non-prédicatives.
Henri Poincaré, dans La logique de l’infini (Revue de Métaphysique et de Morale, 1909). Réédité dans Dernières pensées, Flammarion. "

Oui Wissam, Henri Lombardi et Henri Poincaré, même combat ! Les deux en rient.

christophe c · October 2011

A matsaya, les théorèmes ne sont pas leur conclusion en faisant comme si les axiomes étaient infaillibles, ce sont des énoncés de la forme A=>B ou A est une conjonction des axiomes et si B est l'avion vole je ne pense pas que tu te contenterais de A avec AC OU AD dedans, tu voudrais d'abord qu'ils en soient éliminés via une AUTRE preuve

C'est tout l'intérêt du progrès qu'a constitué la corcuho en ce sens que moult axiomes ont été découverts plus comme des montagnes dont on peut observer au loin les choses mais ça ne dispense pas ensuite de s'en rapprocher

[CC écris moins vite ! Le téléphone portable a bon dos ! AD]

D. Hilbert · October 2011

@C. Chalons : Je me permets d'introduire ici trois fichiers au format PDF conçus à partir de l'excellent ouvrage de Michael J. Beeson, intitulé "Foundations of Constructive Mathematics (Metamathematical Studies)" [éditions Springer]. Les voici :

P.S. : Selon l'auteur, "[t]his book is dedicated to the memories of Errett Bishop and Arend Heyting." (C'est moi qui souligne).

A +

ccnc · October 2011

merci et aussi merci pour le deuxième fichier du livre de Bishop, je viens de voir que je l'ai bien reçu!

ccnc · October 2011

Etant sur un PC, j'en profite pour faire une synthèse rapide la discussion ayant tourné sur d'autres sujets que les précédents fils. Je rappelle que j'ai posté quelques posts techniques qui donne une vision exhaustive de ce qu'il y a à savoir pour débattre de ce sujet philosophique (dans ce fil il y a http://www.les-mathematiques.net/phorum/read.php?3,700037,700176#msg-700176 , et dans l'autre fil il y a 3 posts, l'un qui donne la définition des maths intuitionnistes (titré ainsi) , un autre qui donne suite à une demande le comment s'exécute une preuve via un programme caml, un autre (adressé à Zephir qui décrit la partie logique de la logique intuitionniste).

Il faut donc bien distinguer ces choses claires, formelles et vérifiables car posté in extenso, de quelques liens qui mènent à des articles techniques dont quelques phrases sorties de contexte peuvent servir un plaidoyer mais tromper sur le contenu (on l'a vu avec l'exemple de l'article de Friedman dont une phrase de Feferman ouvait vraiment "faire rêver" pour qui était en quète de "croire" aux bonnes nouvelles de style "Godel dépassé" plus ou moins répandue dans les fils.

1) Il n'existe plus aujourd'hui aucune difficulté quant à toute la réalité technique qui se cache derrière cet apparent débat: tout a été compris, et de plus tout est plutot simple sous l'angle de Curry Howard (bien relire l'exo http://www.les-mathematiques.net/phorum/read.php?3,700037,700176#msg-700176 )

2) HL aborde maintenant le sujet des axiomes qu'on accepte ou non. si c'est effectivement un débat philosophique qui intéresse moult philosophes ou épistémologues, il ne faut pas laisser croire que c'est un débat "ouvert" qui ferait l'objet "d'articles de recherches" (comme le fait de poster des liens peut le laisser croire). En effet, la science et les maths sont plus sérieuses que ça et ne peuvent se permettre de faire reposer leurs théorèmes sur des interpretations soumises aux caprices des uns et des autres (on est 7000000000, on en finirait pas). Actuellement, chaque logicien a compris (et se sent obligé de répondre à toute fantaisie philosophique) que les axiomes sont tacitement présents dans les hypothèses, et que c'est simplement par économie d'encre qu'on a des standards (essentiellement ZF, plus rarement certains présentent un travail (qui est en général de rédaction très longue) dont ils mettent en évidence en écrivant tout qu'ils ont travaillé dans une théorie plus faible) non pas qui les en retire, mais qui les y considèrent comme présents de manière sous-entendue à gauche sous la forme "ceci et ceci et cela =>"

3) La correspondance de Curry Howard a prouvé irréfutablement trois choses:
3.1 ) qu'on peut exécuter TOUTES LES PREUVES DE MATHS
3.2) que celles utilisant le tiers -exclus, etc ont tout autant un contenu calculatoire que les autres
3.3) que dans cette bienvenue correspondance, on retrouve (on ne les amoindrit pas, on ne les augmente pas) les "mystères" déjà présents en filigrane dans ce qui n'était au début pas informatique (comme les raisonnements ou les questionnements platoniciens des anciens "les entiers existent-ils?", etc)

4) Il ne change finalement pas grand chose d'affaiblir ou de renforcer les théories fondatrices, toutes sont faibles à l'exception de ZFC et la plupart du temps de véritables usines à gaz à apprendre. Quelle réelle utilité d'apprendre une usine à gaz qui est un sous-ensemble de ZFC, au motif de "refuser" tel ou tel axiome de ZF, sans pour autant l'avoir cassé? C'est une option philosophique, on ne peut pas prouver que quelqu'un qui le fait a tort, mais "refuser" un axiome révèle souvent une incompréhensio quant au fonctionnement des maths: un théorème qui n'utilise pas tel ou tel axiome dans sa preuve n'a pas plus de raison d'être mis en doute parce que son auteur a dit qu'il "travaillait" dans le cadre de la théorie machin. C'est qui est tracassant c'est cette idée de "refuser" par principe et de publier des listes interminables et indigeste de cabalisitques compliquées à priori qui me semblent ne servir à rien à part à confirmer chez leur promoteur qu'ils n'ont pas encore passé le cap de comprendre ou accepter (2)

5) Je termine avec deux aspects qui me semblent à dessein ou non confondus par HL:
5.1) En gros la corcuho transforme n'importe quel preuve de maths en graphes "effectif" (ie en preuve effective et constructiviste mais dont les pointeurs qui la représentent dans la mémoire de l'ordi peuvent s'organiser en cycles). Ca n'a rien d'étonnant dans la mesure où la logique classique est juste la logique intuitionniste à laquelle on a rajouté le droit dans le jeu-prouveur-sceptique de revenir en arrière dans la partie pour dire "ah, bah ça tu me l'as donné en hypothèse"voir (*****)
5.2) Si on devait situer le plaidoyer d'HL dans ses posts où il rappelle les positions de Poincaré et cie dans le paradigme actuel, ça donnerait en gros qu'il "combat" les preuves qui bouclent. Mais je suis complètement et totalement son adversaire dans ce combat, qui me semble largement dépassé (et c'est pas mon genre d'invoquer des affaires de modernismes, simplement quand on a progressé et compris des trucs dans la science ca me parait inutile de "les oublier"): car c'est très exactement comme dire "nous allons étudier toujours de plus en plus près les programmes qui s'arrêtent de manière à avoir des classes de plus en grandes de programmes dont on est sûr qu'ils s'arrêtent". Je tiens à dire que je ne pense pas m'écarter d'un chouya de la pensée de HL en traduisant en le slogan rouge son positionnement philosophique. On le voit depuis ses premiers posts quand il argue autour des notions de fiabilité des théories, etc.
Et bien je suis opposé à ce positionnement (en rouge) de la mnière suivante:
5.2.1) D'une part, c'est "interminable" (on sait depuis longtemps qu'aussi "subtile" que ça puisse paraitre, on trouvera le lendemain plus subtil puis le surlendemain encore plus subtil jusqu'à s'arracher les cheveux sans avancer autrement que stérilement (ce sont la éternelles variations sur l'indécidabilité du problème de l'arrêt mainetnant plus que bien connu). La traduction via la corcuho a bêtement son analogue consistant à faire des théories "très faibles" de plus en plus fortes de manière à rester dans le "pseudodécidable"
5.2.2) D'autre part, c'est ERRONé!!! Aucun programme informatique profond ne s'arrête. Aucun théorème de maths profond ne cherche à établir (à part quelques trucs ouverts ici ou là qui représentent des défis d'Olympiades) l'existence de solutions à telles ou tells équations diophantiennes. La plupart des programmes qu'on utilise tous les jours (que notre cerveau utilise peut-être) sont exprès fait pour ne pas s'arrêter. (Exemple n'importe quel OS qui se lance à l'allumage et qui ne s'arrête que la suite d'une (grosse) interruption de votre part). Le pendant des interruptions et des interactions avec l'extérieur dans un programme c'est "le tiers exclus" et les alternances de quantificateurs, etc qui élèvent les énoncés à des niveaux de plus en plus rejetés par "le consrtuctivisme"
Les programmes issus des maths n'ont strictement aucun raison pertinente (et c'est peu pertinent de chercher lesquels) de "s'arrêter". Faire ainsi la course à "démontrer de plus en plus de situations d'arrêt" n'est qu'un résidu d'une quète initiée à une époque où on n'avait pas compris tout ça. Aujourd'hui bien au contraire, il faut intégrer l'idée qu'une preuve quand elle s'exécute peut tout à fait autant réaliser l'oeuvre d'un OS certifié, d'un jeu de guerre, d'une partie d'échec, etc qui ne terminent pas unilatéralement à prior.

(*****) Jeu de la logique classique:
Cadre: une liste d'énoncés certains en encre verte d'autres en encre rouge.
Regles: le prouveur est déclaré gagnant quand un même énoncé apparait en vert et aussi en rouge dans la liste
Regles-étape: le prouveur peut:
* ou bien choisir un énoncé rouge de la forme A=>B et le remplacer par un A mis en vert et un B mis en rouge rajouté à l aliste (le sceptique n'a alors rien à faire)
* ou bien désigner un énoncé de la forme A=>B qui est écrit en vert et demander au sceptique de rajouter ou bien un A rouge ou bien un B vert à la liste

(*****) Jeu de la logique intuitionniste:
Cadre: une liste d'énoncés certains en encre verte et au plus UN en encre rouge.
Regles: le prouveur est déclaré gagnant quand un même énoncé apparait en vert et aussi en rouge dans la liste
Regles-étape: le prouveur peut:
* ou bien choisir un énoncé rouge de la forme A=>B et le remplacer par un A mis en vert et un B mis en rouge rajouté à l aliste (le sceptique n'a alors rien à faire)
* ou bien désigner un énoncé de la forme A=>B qui est écrit en vert et demander au sceptique de rajouter ou bien un A rouge ou bien un B vert à la liste

La seule différence entre les deux est que dans la classique il y a plusieurs énoncés rouges éventuellement, ce qui permet au prouveur s'il "prend" une hypothèse dans (A=>B) (donc A devient vert) de la faire valoir dans une situation où "avant dans la partie" il "s'intéressait" à prouver A (ie le fait de prendre A le fait gagner s'il y a eu une position éventuellement avant où A était à prouver. Dans la logique intuitionniste le fait de prendre A ne lui est utile que si APRES dans la partie il se retrouve avec un A rouge (mais qu'il y ait eu un A rouge longtemps avant "est perdu" si l'énoncé rouge a changé). Les "sémantiques" de Kripke sont d'ailleurs une illsutration quasi "recpopiée" de ça avec juste le mot "sémantique" qui fait joli.

On appelle "théorèmes" (resp pour les deux logiques) les situations de départ à partir desquelles le prouveur a une stratégie gagnante. (L'ajout de quantificateurs est évident à règlementer). Une situation de départ peut être vue comme une sorte de "disjonction des énoncés de la liste" à prouver.

Lorsqu'un arbre de démonstration classique est transformée en graphe effectif par une quelconque moulinette logiciel issue de la corcuho, les boucles présentes ne sont pas "des choses malsaines" comme ceux qui n'ont pas compris Griffin et pense que le tiers-exclus est problématique mais simplement un état de fait qui traduit la différence entre un énoncé rouge au plus ou autant d'énoncés rouges qu'on veut.
Autrement dit, ce sont simplement des connexions "A=>A" dans le graphe là où les gens croyaient voir des "nonA ou A" dans l'arbre classique. Mais ça ne pose JAMAIS de problème et c'est bien compris. La seule chose que ça change est que la sacrosainte obscession "des programmes qu iterminent" (qui n'est qu'un concepts très contextué du chapitre calculabilité à l'ancienne) n'est plus satisfaite puisqu'on passe d'un arbre à un graphe pouvant contenir tout plein de cycles. Mais peu importe, heuresement même que les programmes ne s'arrêtent pas (exemple le windows de votre PC ) à chaque instant!

Matsaya · October 2011

Je sais bien que les théorèmes ne sont pas leur conclusion. Mais dans l'exemple de l'avion, ce qui m'importe réellement, ce n'est pas que A => l'avion vole soit juste, mais que cela soit juste et que A soit «acceptable» pour moi. Par exemple, sans tiers exclus, … et au final, autre preuve ou pas, tu ne pourras pas tout éliminer (i.e. avoir ø=> l'avion vole).

De plus, il est fort possible que A=> l'avion vole ne me convienne pas, mais B=> l'avion vole oui.

Matsaya · October 2011

Et une question cc pour ta corcuho, je croyais me souvenir que tu avais dit que c'était plutôt une position philosophique qu'une vrai correpsondance formelle. Me trompe-je ?

gerard0 · October 2011

Rappel :

Il y a eu de nombreuses démonstrations que les avions ne peuvent pas voler.

X:-(

Cordialement.

NB : Dans cette intervention, je ne me prononce pas sur le débat.

christophe c · October 2011

A matsaya : oui a ttes tes questions sauf sur la corcuho qui est qd meme un isomorphisme si ce n est une egalite assez.precise et definitive entre preuves et programmes egalite si on la compile dans le bon langage qui est simple

non aussi en cequi concerne le TE dans les preuves il n est jamais problematique car dans le jeu reel face a des adversairzs ou la nature ladversaire joue des coups aux occurences des quantificateurs par consequent tout devient concret et en particulier le il existe et le ou deviennent intuitionnistes meme s ils ne le sont pas dans la preuve du solitaire qui voit de fantomatiques lettres

christophe c · October 2011

Le seul VRAIDE VRAI axiome "problematique est la duplication d hypothese ie A=>[A=>B] => [A=>B] » qui est tout aussi present en logique intuitionniste qu en logique classique et qui correspond a jouer sur deux tables la partie en ayant comme seul objectif de gagner sur au moins une

exemple battre karpov OU kasparov est facile et constructiviste sans pour autant disposer de qualite de virtuose aux echecs il suffit de les faire jouer lun contre l autre si on peut choisir sa couleur

le fait ici de dire A ou A=>A est donc tres tres tres offensif mais n a rien a vvoir avec les limitations platoniciennes apparemment proposees par les constructivistes

dsl je poste d un tel

zephir · October 2011

cc a écrit:

dsl je poste d un tel

Prend-toi un portable de 900 g

samok · October 2011

Merci D.Hilbert pour la réponse,

il faut donc que je change ma manière de lire le livre, en fait il retranscrit en constructiviste le classique (ce que j'ai appris à l'école). Du coup changer les mots seraient moins confusionnels, ou ajouter l'adjectif constructiviste à la fin de chaque principe.

Mais quand même, je ne me remets pas de la remarque à propos de la démo de l'irrationnalité de $\sqrt{2}$.
Supposer $non P$ et arriver à truc du genre $ A\, et \, non A$ c'est bien ça le raisonnement par l'absurde en classique, le raisonnement par contradiction comme vous dites, non ?

-> Avec $\sqrt{2}$ la preuve la plus commune arrive à la conclusion, sous $\sqrt{2} \in \mathbb{Q}$, il existe une fraction irréductible réductible non ?

Question subsidiaire, en classique comment se formalise l'axiome logique du raisonnement par l'absurde? Est-il équivalent à l'axiome logique de contraposition : $A$ implique $B$ est équivalent à $non B$ implique $non A$. L'équivalence s'entendant : je remplace l'un par l'autre, ça ne change rien dans l'ensemble des théorèmes.

Pardon sieur cc, pour cette parenthèse, mais j'aimerais être enfin clair sur cette dernière question, j'ai souvent entendu l'un et son contraire.

S

nicolas.patrois · October 2011

zephir a écrit:

Prend-toi un portable de 900 g

Il a un téléphone de 900g.

zephir · October 2011

Merci à Samok d'avoir posé la question, car beaucoup de raisonnements par l'absurde sont en fait des raisonnements par la contraposée.

christophe c · October 2011

Je confirme pour NP

a samok j ai deja repondu un milliard de fois en cherchant un tu trouveras moults posts

en quelques mots secs:

A=>
A=>=>[A=>B=>[A=>C]]
tout=>A
donnenet tous les theoremes intuitionnistes par modus ponens

tu rajoutes A=>B=>A=>A et tas la logique classique

non A est l abreviation de A=>tout

priorite des parentheses a gauche

pour les autres connecteurs ils sont definis dans l autre post du lautre fil en termes de =>
au second ordre

leon1789 · October 2011

samok écrivait:

>
> Mais quand même, je ne me remets pas de la
> remarque à propos de la démo de l'irrationnalité
> de $\sqrt{2}$.
> Supposer $non P$ et arriver à truc du genre $ A\,
> et \, non A$ c'est bien ça le raisonnement par
> l'absurde en classique, le raisonnement par
> contradiction comme vous dites, non ?
>
> -> Avec $\sqrt{2}$ la preuve la plus commune
> arrive à la conclusion, sous $\sqrt{2} \in
> \mathbb{Q}$, il existe une fraction irréductible
> réductible non ?
>

En fait, il y a deux types de raisonnement dit communément "par l'absurde" :
la réduction à l'absurde (qui n'utilise pas le tiers exclu)
et le détour par l'absurde (qui utilise le tiers exclu).

Quand les logiciens parlent du Raisonnement Par l' Absurde, il s'agit du second type.

Explication :
-- la réduction à l'absurde montre qu'une proposition P est fausse : on suppose P et on déduit une contradiction.
Les logiciens diront qu'on a prouvé non(P) de manière directe.
-- le détour par l'absurde montre qu'une proposition P est vraie : on suppose non(P) et on déduit une contradiction.
Alors on a une preuve directe de non(non(P)), qui implique que P est vraie par tiers exclu.

La preuve de l'irrationnalité de $\sqrt2$ est du premier type : on montre sans tiers exclus que $\sqrt2 \in \mathbb Q$ amène à une contradiction. On conclut donc que $\sqrt2$ n'est pas rationnel, donc irrationnel (par définition de l'irrationnel).

Exemple pour le second type de raisonnement par l'absurde :
"Dans un anneau commutatif $A$, pour tout idéal maximal $M$, on choisit $x_M \in A \setminus M$. Alors 1 appartient à l'idéal $I$ engendré par tous les éléments $x_M$".
Voici une preuve par détour :
on suppose que 1 n'appartient pas à $I$. Alors $I$ est propre et il est inclus dans un idéal maximal $M$.
Ainsi $x_M \in I \subset M$ ce qui contredit la définition de $x_M$. Absurde, donc 1 appartient $I$.

Attention, tout ceci n'a de sens que si on sait faire la différence entre une phrase positive P , et une phrase négative non(P)...

leon1789 · October 2011

zephir écrivait:

> Merci à Samok d'avoir posé la question, car
> beaucoup de raisonnements par l'absurde sont en
> fait des raisonnements par la contraposée.

De même, il y a deux raisonnements dit communément "par contraposée" :
-- celui qui passe de ( P => Q ) à ( non Q => non P ) , qui n'utilise pas le tiers exclu ;
-- celui qui passe de ( non Q => non P ) à ( P => Q ) , qui utilise le tiers exclu.

C'est du même genre que pour les deux types de raisonnement pas l'absurde.

samok · October 2011

pardon, j'ai vraiment l'impression de vous irriter sieur cc. Oui, j'ai vu des posts sur le sujet, mais j'ai pas compris. (Bon après ce que signifie comprendre ...)

Merci leon1789, en première approximation je crois que cela répond à ma question, je relirai demain avec ma petite tête reposée sur ses deux épaules.

S

christophe c · October 2011

Oups pardon samok non mais g ete expeditif par frustration de poster de mon tel et parce que pour taper le moindre symbole non lettre je dois naviquer ds des pages et des pages d options

je te referai un post nicquel d un pc avec petit cours progressif etc

christophe c · October 2011

Concernant la reponse que t a faite leon sur le meme sujet j avais fait un post de moins d un an dc un peu recent qui detaillait le "vrai" rpa

en fait c est quand tu utilises DEUX FOIS l hypothese non P. Dans la preuve de tout que ca saigne sinon c est peu important en fait ca permet aussi de rendre ca insensible a qui est prmitif et qui est" non kekchoz"

christophe c · October 2011

@samok, étant dans un cyber, je te fais un post assez complet avec toutes les définitions. Je le fais formel pour que tu n'aies pas à t'interroger de manière dépendante à mes connexions ces temps-ci car je ne sais pas si j'arrive à venir souvent.

Dans la suite, on suppose toujours qu'on s'est donné un ensemble V dit de "variables propositionnelles", qui est infini. On prend le plus petit ensemble F tel que $F^2\cup E\subseteq F$. Un couple $(a,b)\in F^2$ sera noté $a\to b$ et compris comme "a => b".

La parenthèses tacites seront toujours à gauche (ie $a\to b\to c$ veut toujours dire $(a\to b)\to c$ )

Soit S l'ensemble des $a\to (b\to c) \to ((a\to b)\to (a\to c))$ quand $(a,b,c)$ parcourt $F^2$ et $K$ l'ensemble des $a\to (b\to a)$ quand $(a,b)$ parcourt $F^2$. Soit P l'ensemble des $a\to b\to a\to a$ quand $(a,b)$ parcourt $F^2$.

Soit $LM$ l'intersection des parties $X$ de $F$ telles que $S\cup K\subseteq X$ et $\forall (a,b)\in F^2:$ si $a\to b\in X$ et $a\in X$ alors $b\in X$ (**). On l'appelle l'ensemble des théorèmes propositionnels de la logique minimale (on dit aussi "intuitionniste" bien que "intuitionniste réfère à un langage plus riche, mais ça n'a aucune espèce d'importance).

Soit $LC$ l'intersection des parties $X$ de $F$ telles que $S\cup K\cup P \subseteq X$ et $\forall (a,b)\in F^2:$ si $a\to b\in X$ et $a\in X$ alors $b\in X$. On l'appelle l'ensemble des théorèmes propositionnels de la logique classique.

Les définitions qui précèdent peuvent être appelées "présentation à la Hilbert" de la façon dont raisonnent les maths. D'après ce qu'on m'a dit Hilbert affectionnait les présentations "cash" et simples des regles du jeu. Ici la propriété "simple" s'appelle la regle du modus ponens (ie c'est la propriété (**) des définitions.

L'ensemble P est l'ensemble des axiomes du tiers exclus ou équivalemment du raisonnement par l'absurde.

Il y a une présentation plus douce et un théorème qui dit que c'est équivalent:

Soit $G$ l'ensemble des couples $(H,x)$ où $H$ est une partie finie de $F$ et $x\in F$. Soit $Axiome:=$ l'ensemble des $(H,x)\in G$ tels que $x\in H$.

Soit $LLM$ l'intersection des $X\subseteq G$ tels que:
1) $Axiome\subseteq X$
2) pour tous $(H,x)\in G$ ; $a\in F$: si $(H\cup \{a\}, x)\in X$ alors $(H,a\to x)\in X$
3) pour tous $(H,x)\in G$; $a\in F$: si $(H, a\to x) \in X$ et $(H,a)\in X$ alors $(H,x)\in X$

Théorème: LM=l'ensemble des $x\in F$ tels que $(\emptyset , x)\in LLM$ (prouve-le en exo)

La définition de LLM représente un peu plus l'activité "courante" des matheux qui pour prouver des trucs "supposent" des machins, et les retire à la fin en changeant leur conclusion pour annoncer "on a prouvé hypothèse=>conclusion". Les couples (H,x) sont les situations pour lesquelles on se demande si on peut prouver que la conjonction des énoncés se trouvant dans H entraine x.

Soit $G_2$ l'ensemble des couples $(H,Y)$ où $H,Y$ sont des parties finies de $F$.
Soit $Axiome_2$ l'ensemble des couples $(H,Y)$ tels que $H\cap Y\neq \emptyset$

Soit LLC l'intersection des X inclus dans $G_2$ tels que:
1) $Axiome_2\subseteq G_2$
2) pour tous ... si $H\cup \{a\}, Y\cup \{b\}) \in X$ alors $(H,Y\cup \{a\to b\})\in X$
3) pour tous ... si $(H\cup \{a\} , Y)\in X$ et $(H , Y \cup \{b\} )\in X$ alors $(H \cup \{a\to b \},Y)\in X$
4) pour tous ... si $(H \cup \{a\to a \},Y)\in X$ alors $(H,Y)\in X$
5) pour tous ... si $(H,Y)\in X$ et $H\subseteq H'$ et $Y\subseteq Y'$ alors $(H',Y')\in X$

Théorème:
LC=l'ensemble des $x\in F$ tels que $(\emptyset , x)\in LLC$

Présentation sous forme de jeux:

A chaque étape on a une situation qui est un élément de $G$. Voici les règles:
1) C'est toujours le prouveur qui a l'intitiave lors d'un tour
2) si la situation est $(H,x\to y)$ le prouveur a le droit de dire "on continue avec $(H\cup \{x\}, y)$ ". Le sceptique ne fait rien et la nouvelle situation est $(H\cup \{x\}, y)$
3) Quelle que soit la situation $(H,x)$ , le prouveur a le droit de choisir l'élément $a\in F$ qu'il veut et le sceptique doit alors choisir entre l'une des deux nouvelles situations: $(H,a)$ ou $(H,a\to x)$ et on continue avec celle qu'il choisit.

Les deux joueurs, "prouveur" et "sceptique" s'affrontent ainsi en produisant une liste de situations $(H_n, x_n)$.

Définitions:
D1) si $x_n\in H_n$ alors le prouveur est déclaré "intuitionnistiquement gagnant" à l'étape n
D2) si $H_n\cap \{x_1;..;x_n\}\neq \emptyset $ le prouveur est déclaré "classiquement gagnant" à l'étape n

Théorèmes:
T1) LM est l'ensemble des $x$ tel que le prouveur a une stratégie qui lui garantit de finir par être déclaré intuitionnistiquement gagnant en partant de la situtation $(\emptyset, x)$
T2) LC est l'ensemble des $x$ tel que le prouveur a une stratégie qui lui garantit de finir par être déclaré classiquement gagnant en partant de la situtation $(\emptyset, x)$

Maintenant, il te reste à étudier les différences pour comprendre les nuances entre raisonnement par l'absurde, et raisonnements intuitionnistes.

En particulier, compare les deux jeux quand on part de la situation $(\emptyset , a\to b\to a\to a)$

samok · October 2011

Merci beaucoup sieur Christophe pour la peine prise à me répondre ,

les premières lignes me posent question, mais je vais tout bien lire cela plus tard. J'avais jamais réalisé que l'implication c'est une loi de composition interne et comprend mieux cette histoire de parenthésage.

La relecture du post de leon1789 me laisse penser qu'il y a des subtilités qui m'échappent. Je posterai "la" preuve "classique" de $\sqrt{2} \not \in \mathbb{Q}$ et je poserai les questions résiduelles alors.

S

[La case LaTeX. AD]

Lombardi Henri · October 2011

Pitié !

1)
ccnc, tu sembles avoir écrit un post assez synthétique
et donc sympathique
mais je ne peux lire à l'écran un post de plus de 30 lignes

2)
je propose donc la chose suivante:

toute personne qui propose un post un peu long produit aussi un pdf du même post, qu'il attache

je signale que tout le monde n'a pas une imprimante couleur à sa disposition
et que donc les couleurs doivent être bannies

je signale que gras+souligné+plus grand,
cela ne sert qu'à rendre les textes illisibles

ce qui se conçoit bien s'énonce clairement et les mots pour le dire arrivent aisément, sans gras ni souligné

disons au maximum un ou deux gras, un ou deux italiques, deux ou trois guillemets,
mais pas plus
bref voyez La Pléiade

3)
quant à CC, dont je n'ai pas lu plus de 5% de ses messages,
il devrait
   ne faire qu'un ou deux post par jour sur chaque fil
   prendre le temps de réfléchir pour raccourcir
et faire un petit pdf vraiment synthétique de sa pensée
dans lequel on arriverait notamment enfin à connaître sa position sur la sémantique:
        ce que signifie vraiment pour lui un théorème de math dans le monde réel,
        pas seulement dans le monde des preuves formelles

mais je crains qu'il n'en ait pas
car il me semble qu'il pense qu'il n'y a aucun monde mathématique objectif hors le monde des preuves formelles

4)
la plupart des discussions à bâtons rompus sont difficiles à suivre,
car on ne sait pas à quoi (et souvent même à qui) répond exactement l'interlocuteur
il faudrait toujours dire à quoi précisément on répond
si on répond à un post de 3 pages, il faut préciser: "je réponds à telle affirmation dans le post"

5)
il y a par exemple une discussion sur l'irrationalité de racine de 2 qui se fait jour
mais je n'arrive pas à identifier l'endroit où elle a commencé, et donc ce que commentent les gens
le mieux aurait été d'ouvrir un nouveau fil sur ce sujet précis
je dirai quant à moi une seule chose sur ce sujet:
        n'espérez pas obtenir une preuve de l'absurde (une fraction d'entiers dont le carré est 2)
        autrement que par l'absurde (ie réduire l'hypothèse à l'absurde)
en fait c'est exactement ce que l'on vous demande de faire
il n'y a aucune preuve PAR l'absurde là dedans, seulement une preuve DE l'absurde

christophe c · October 2011

Sur racine de 2 il ya deja plusueiurw post qui ont discute tres exactement de ce point

pour le discours sur couleurs et longueurs cest vrai mais un peu demago comme discours

pour ma position preuves maths sciences formalisme il ya au moins 500 posts qui lont detaille de ma.part je ne peux pas les reecrire pour chaque intervenant : il ya eu un long fil ds le passe sur la modelisation qui a dialectique longuement sur le sujet

@samok concentre toi peut etre toi meme sur la partie jeux.de.mon post et prouve en exo que le jeu classique est equivalent au jeu intuitionniste dans lequel on ajoute A=>tout=>tout=>A a l ensemble vide ie des que cet enonce figure comme x dans une situation (H,x) le prouveur est declare gagnant et pour le reste on garde les regles intuionnistes

samok · October 2011

Je vais rechercher ensuite le ou les posts en question, ensuite, mais j'aimerais tout de même que la réponse figure ici.

Contemplation : $\sqrt{2} \not \in \mathbb{Q}$
Lemme :
Si $n$ est impair (n'est pas pair) alors $n^2$ est impair (n'est pas pair).
-> car il existe $p$ tel que $n=2p+1$ donc $n^2=2\times(2p^2+2p)+1$ est impair.
Corollemme :
Si $n^2$ n'est pas impair (n'est pas pas pair=pair) alors $n$ n'est pas impair (n'est pas pas pair = pair)
Preuve de la contemplation :
Supposons $\sqrt{2} \in \mathbb{Q}$.
Alors il existe $p,q \in \mathbb{N}$ tel que $\sqrt{2}=\dfrac{p}{q}$ avec $\dfrac{p}{q}$ irréductible.
Donc $\sqrt{2}q=p$ et ensuite $2q^2=p^2$. Donc $p^2$ est pair et donc $p$ est pair, disons $p=2r$.
On obtient ainsi $2q^2=4r^2$ et donc $q^2=2r^2$ et donc $q$ est pair.
Ainsi : il existe $\dfrac{p}{q}$ irréductible et $\dfrac{p}{q}$ réductible. Absurde.
Conclusion : $p \in \mathbb{Q}$ mène à une contradiction.

Depuis il y a pas mal de temps on m'a dit : et ben ça c'est un raisonnement par l'absurde.
Mais bon on a démontré $\sqrt{2} \in \mathbb{Q}$ implique $(A \text{et} non(A)) = FAUX$.
Par contraposition $non(FAUX)=VRAI$ implique $\sqrt{2} \not \in \mathbb{Q}$.
Cela relève donc aussi d'un raisonnement par contraposition non ?

Je vais relire ce qui a été dit et voir si c'est cohérent et précise que dans la partie $Logique$ au lycée, il n'est pas mentionné la rubrique : raisonnement de l'absurde.
Cette partie est d'ailleurs, jusqu'à ce jour, strictement incluse dans mon ignorance infinie.
Donc mon souci est de savoir, s'il y a un abus de langage, et ben que moi en tant que prof de nattes, ben au moins je le sache.

S

[Edit final] : j'ai relu vite fait le fil, je mets ça de côté pour quand j'aurai du temps pour y réfléchir pleinement. Je sens que je vais mal dormir cette nuit ...

Bu · October 2011

@Samok : Si tu prouves $A\Rightarrow B$ en supposant $A$ et en en déduisant $B$, tu appelles ça un raisonnement par contraposition ? Par l'absurde ? Je ne pense pas.
Or $\neg A$, c'est par définition $A\Rightarrow \mbox{absurde}$. Pour montrer $\neg A$, tu supposes $A$ et tu montres l'absurde. Est-ce que ça ne te semble pas un cas particulier du raisonnement ci-dessus ?

christophe c · October 2011

@samok

non, en fait tu as l'enchainement suivant:

p²=2q² --> il existe u,v: p=2u et q=2v --> (p,q) n'est pas irréductible

donc r=p/q => pour tout (p,q) .. : (p,q) n'est pas irréductible

tu obtiens donc "r rationnel =>tout" qui est par définition "non(r rationnel)"

il n'y a pas vraiment de clonage des hypothèses (mais il y a utilisation de lemmes de lycée disons et de récurrence) tu ne te sers qu'une fois du fait que r est la racine de 2 et du fait que r est rationnel.

Une preuve "vraiment" par l'absurde c'est quand à un moment tu dis:

A=>(A=>B) donc A=>B ie "tu le sens" quand tu fais ça.

Par exemple pour prouver a²=0 =>a=0 , tu prouves en fait facilement a²=0 =>(a non nul =>(a non nul =>tout)) , mais t'es obligé d'admettre que
(a non nul =>(a non nul =>tout)) => (a non nul =>tout) (enfin je ne connais pas de preuve qui s'en passe, mais je n'y ai pas énormément réfléchi non plus.

En gros, pour te rendre compte et faire le bonne distinction, tu peux supposer
(A=>tout)=>tout [size=x-large]=[/size] A (*****)

Mais par contre tu ne t'autorises plus A=>(A=>B) =>(A=>B) (***)

Et bien quand tu peux te passer de (***) ce n'est pas grave d'utiliser (*****) ie les preuves obtenues sont "essentiellement" concrêtes.

C'est une erreur assez commune commise par les anciens ou les gens peu cultivés en logique de confondre le problème que leur pose le rais par l'absurde (ou le tiers exclus) avec (*****). Le vrai "noeud" c'est (***)

christophe c · October 2011

oups pardon, je répondais à samok

constructivisme

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 21