Par où commencer la logique ?
Bonjour,
D’un côté, je me sens toujours un peu frustré quand je fais des maths même quand la démo est juste, j’ai toujours l’impression qu’un gros truc me manque pour me sentir « décrispé ». Aussi, j’ai un peu lu wiki sur la définition de ce qu’est un système logique, le calcul de prédicat, ce genre de choses, ça a l’air sympa mais tout est un peu dans tous les sens et je dois ramasser miette par miette les infos dans les articles que je trouve. Or moi j’aimerais bien comprendre comment on démontre « pour de bon » enfin comment tout ça marche pour de bon et ce que je lis me perd plus qu’autre chose.
Est-ce que vous pourriez me conseiller un support si possible gratuit (ou moins de 15€ si possible :-D) qui m’introduit à la logique (mais pas vulgarisé, qui le fasse pour de vrai). Je sais par exemple que « théorie des ensembles » de krivine est censé être bien mais quand j’ai lu le sommaire et un peu le début il partait directement sur « la Théorie des ensembles » mais sauf erreur y avait rien sur « à la base on part d’où on fait quoi » or c’est ça que je cherche.
Merci d’avance !
D’un côté, je me sens toujours un peu frustré quand je fais des maths même quand la démo est juste, j’ai toujours l’impression qu’un gros truc me manque pour me sentir « décrispé ». Aussi, j’ai un peu lu wiki sur la définition de ce qu’est un système logique, le calcul de prédicat, ce genre de choses, ça a l’air sympa mais tout est un peu dans tous les sens et je dois ramasser miette par miette les infos dans les articles que je trouve. Or moi j’aimerais bien comprendre comment on démontre « pour de bon » enfin comment tout ça marche pour de bon et ce que je lis me perd plus qu’autre chose.
Est-ce que vous pourriez me conseiller un support si possible gratuit (ou moins de 15€ si possible :-D) qui m’introduit à la logique (mais pas vulgarisé, qui le fasse pour de vrai). Je sais par exemple que « théorie des ensembles » de krivine est censé être bien mais quand j’ai lu le sommaire et un peu le début il partait directement sur « la Théorie des ensembles » mais sauf erreur y avait rien sur « à la base on part d’où on fait quoi » or c’est ça que je cherche.
Merci d’avance !
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Je te conseillerais les deux tomes de Logique Mathématique de Cori et Lascar, mais ils sont un peu chers. Peut-être arriverais-tu à les trouver en ligne ?
cours calcul prédicats
sur google, le premier résultat est un pdf de cours de Polytechnique.
http://www.lama.univ-savoie.fr/~RAFFALLI/dnr.html/
Les auteurs font en exemples beaucoup de lien entre mathématiques courantes de niveau licence (disons L1-L2) et logique formelle, il me semble que ça pourrait répondre à tes crispations comme tu dis.
Par contre c'est plus que 15€, mais bon tu devrais le trouver dans n'importe quelle BU de sciences, et il faut pas trois ans pour le lire.
Et puis les livres c'est long. Et parle de bien d'autre chose même si les suggestions précédentes sont pertinentes.
Une preuve c'est un arbre dans lequel ce qui n'est pas justifié est AUTOMATIQUEMENT SUPPOSE. Je suis sur mon téléphone, je pourrai détailler si tu veux.
En attendant, ton arbre étiqueté par des phrases est une preuve (quel qu'il soit). La seule chose sue tu ne décidés pas toi même c'est ce qu'il prouve. Pour calculer ce qu'il prouve tu prends sa racine C, tu écris "alors C" et il te reste à RECENSER tout ce que tu as supposé. Certaines sont faciles (les feuilles) d'autres moins visibles mais néanmoins vite trouvées : ce sont les énoncés qui affirment que la conjonctions des fils d'un nœud impliquent le nœud. A ça il faudra ENLEVER les hypothèses de C puisqu'elles ont déjà été assumées comme telles. De plus le mieux est d'appliquer la procédure récursivement en partant de LA RACINE. Attention l'arbre explicite n'est pas forcément fini mais tu peux LE RESUMER par un arbre fini
Q1) Sais-tu ce qu'est un arbre? Sinon arrêter la lecture et te renseigner
2) N'importe quel arbre étiqueté par des phrases est une preuve.
3) Les axiomes de ta preuve se recensent de la manière suivante:
3.1) ton arbre est composé d'une racine r, étiqueté par une phrase $C$ et cette racine a une liste finie de fils (comme fiston-s, pas comme fil-s) $f_1,..f_n$, étiquetés respectivement par les phrases $Q_1,..,Q_n$.
3.2) Chacun de ces fils $f_i$ est lui-même la racine de son arbre $T_i$.
3.3) Si $n>1$ tu passes en 3.4, sinon en 3.6
3.4) Tu recenses, pour chaque $T_i$ ses axiomes et tu additionnes les listes, obtenant une liste $L$
3.5) Tu ajoutes à $L$ l'énoncé $Q_1\to (Q_2\to (Q_3\to (......\to (Q_n\to C)))...) $, puis tu sautes en 3.8
3.6) Si $C$ n'est pas de la forme $X\to Q_1$, tu sautes en 3.4, sinon en 3.7
3.7) On est dans le cas où $C=(X\to Q_1)$ et où la racine n'a qu'un fils. Dans ce cas, tu recenses la liste des axiomes de $T_1$ et tu retires $X$ de cette liste (s'il y apparait)
3.8) Tu obtiens finalement la liste d'axiomes que tu as utilisés. Attention, il peut y figurer un certain nombre d'axiomes "tellement évidents qu'on peut les ignorer quand on enverra le théorème à l'académie des sciences". En particulier, chaque fois que tu fais un modus ponens, la procédure de recensement te signale que tu as utilisé l'axiome "(A=>B)=>(A=>B)" qui est de la forme X=>X
Bon, comme tout mode d'emploi, c'est indigeste à lire une fois, mais c'est très facile à pratiquer sur es exemples. Je t'invite à rédiger quelques preuves de théorèmes classiques du 1er cycle ou des MPSI de cette façon et à en recenser ensuite les axiomes, tu verras que tu seras ébloui. Il reste à préciser le seul et dernier point qui pourrait te bloquer: comment "poster un arbre sur le forum les mathématiques point net" :-D ?
Bon une des réponses possibles et simples est de produire une liste de phrases, chacune suivie d'un numéro ou plusieurs qui est/sont strictement plus petit(s) que le rang, comme dans l'exemple qui suit.
0/ A
1/ A
2/ B (0)
3/ C (1;2)
4/ A=>C (3)
5/ (A=>B) => (A=>C) (4)
C'est un arbre très simple avec beaucoup de noeuds ayant un seul fils (en fait seul le noeud 3 a deux fils). Il y a seulement deux feuilles (les noeuds 0 et 1).
J'ai mis un espace parce que les noeuds 4 et 5 sont la plupart du temps cachés dans les textes "précipités" de maths. Je recense les axiomes de l'arbre qui termine au noeud3, ça donne la liste: A; A; A=>B; A=>(B=>C).
Je te laisse vérifier en exercice que ce recensement est correct. L'arbre qui aboutit au noeud 4 va donc donner comme recensement la liste A=>B; A=>(B=>C)
Et finalement l'arbre qui aboutit au noeud 5 donne comme liste d'axiomes utilisés la liste n'ayant que l'axiome A=>(B=>C)
J'aurais pu ajouter un noeud 6 comme suit:
6) [A=>(B=>C)] => [(A=>B) => (A=>C)] (5)
De sorte qu'au recensement j'aurais pu me glorifier d'obtenir un théorème disant que
en ayant utilisé AUCUN AXIOME
Ce que je peux te proposer comme exercice simple c'est de prouver que $ab=0$ => ($a=0$ ou $b=0$) avec ce format, ça te fera un peu d'effet.
Mais j'insiste une deuxième et dernière fois: ces lectures, à mon avis, ne lui apporteront pas ce qu'il demande car elles offrent BEAUCOUP plus de contenus (qui n'ont rien à voir avec sa demande du premier post) et surtout, elles sont toutes "maladroites" dans le sens qu'elles apparaissent au lecteur non averti (donc en fait déjà formé) comme un "chapitre de plus" rédigé académiquement. Et ça fait surtout des centaines de pages pour une trivialité qui s'expose en 2.
Or, si je ne me trompe pas, il semble bien que grothenbite soit en demande d'un truc assez psychologique concernant le degré de certitude qu'apportent toutes ces constructions et pas tant dans une demande de multiplier culturellement une acquisition de différentes versions équivalentes.
Je peux me tromper bien entendu.
Travaux pratiques:
"il semble bien que grothenbite soit en demande d'un truc assez psychologique"
Cordialement, Pierre.
(Je précise que je suis habituellement bienveillant et assez muet sur les oeuvres "d'introduction à la logique" des non logiciens, qui font ce qu'ils peuvent avec ce qu'ils ont et ne sont pas forcément de mauvaise volonté. Pour que j'émette un avis à ce point défavorable il faut y aller. Quelle mouche a piqué l'auteur (et surtout le serveur de Nice)? Ils devraient vraiment retirer et retravailler leur doc)
@tous: je reformule ou en ajoute sur l'avantage des posts que j'ai envoyés sur les livres. Ils décrivent (formellement) ce qui se fait réellement chez les matheux ordinaires (non logiciens) aux petits mots doux "donc", "car", "puisque" près. Les livres présentent quasi-toujours des systèmes qui ne sont pas utilisés "en vrai" au quotidien, qui décident a priori les axiomes autorisés, explicitent tout et nécessitent de tout transporter (les séquents par exemple) d'une ligne à l'autre, etc.
j'avais débuté une fiche de lecture du livre indiqué par Jesse que je trouve super.
Je l'avais écrite pour retenir qu'il y a des trucs super sciants, du genre variable libre ou pas, des trucs super pratiques genre les arbres, mais surtout qu'un nombre peu important de règles de déduction est suffisant pour convenir de ce qu'est une preuve mathématique, avec certaines qui méritent tout de même de l'attention.
J'ai arrêté lorsqu'il a été question de vérité.
Sieur GaBuZoMeu avait noté le côté un peu bâtard de cette déduction naturelle à la sauce séquent. En tout cas ça me parlait bien.
Il y a des coquilles, pas cap' de les trouver :-) et de me les indiquer que je les corrige une bonne fois pour toute.
S
Moi il me semble bien ce cours du collègue Jean-Louis Rouget, pour acquérir le bagage logique utile pour faire des maths. C'est juste un avis de profane, juste utilisateur de la logique élémentaire pour faire des maths.
Bien sûr ce cours ne comporte pas de phrases poétiques style « N'importe quel arbre étiqueté par des phrases est une preuve ». Il n'a pas la structure des « livres dont vous êtes le héros » : si ceci alors aller en .... Il n'est pas « indigeste à lire une fois ». Il me rappelle l'honnête cours de logique que m'avait fait naguère mon professeur Daniel Lacombe et qui m'a servi de vade-mecum pour faire des mathématiques durant toute une carrière.
Maintenant pour aller plus loin, il me semble judicieux de suivre les conseils de Poirot. Le Cori-Lascar me semble indiqué, je le dis sans l'avoir étudié à fond, mais une telle réputation ne me semble pas pouvoir être usurpée. Plus les autres ouvrages conseillés par les collègues dignes de foi.
Bonne soirée.
Fr. Ch.
Bibliographie (partielle) : Jean-Louis ROUGET
*Créateur du site : http://www.maths-france.fr/
*Maths en Sup : le GPS (guide pour survivre)
*Best of mathématiques
Les meilleurs sujets de Centrale, CCP, E3A, E4A, ESIM
JEAN-LOUIS ROUGET est professeur en classes préparatoires MPSI et MP au lycée privé Notre-Dame de Sion à Marseille.
Donc je suis allé à la bibli près de chez moi et ils avaient seulement le livre que m’avait conseillé jeffe. J’ai juste eu le temps de lire les premières pages et il y a pas mal de choses que je trouve « bizarres » donc j’attends un peu d’y reréflechir et si ça bloque toujours je vous poserai les questions :-D
Pour les autres livres je ne les ai pas trouvés donc je vais me contenter de celui-là et le lire à la bibliothèque du coup.
Christophe c: je pensais que ton pseudo était supprimé avec la grosse embrouille qu’il y avait eu le mois dernier.
Merci du gros pavé, je pense voir un peu du coup je mets dans un lien en dessous la photo « réponse » de l’exo « prouver que ab=0 implique blabla » c’est tout à la fin de mon message.
Mais avant j’ai quand même des questions: en gros si j’ai bien compris au final dans l’arbre (et effectivement j’avais déjà vu ce genre de format et je savais que ça s’appelait arbre mais je ne connais pas la vraie définition) le point un peu bizarre c’est quand on est dans le cas:
0) $B$
1) $A\Rightarrow B$ (0)
Parce que d’un côté faudra enlever $A$ comme tu dis de la liste des axiomes qui prouvent $B$ et en plus si on suit ton algo on ne rajoute aucun axiome à la liste alors que dans le cas:
0) $B$
1) $A$ (0)
Et $A$ n’est pas en fait $C\Rightarrow B$ alors faut rajouter en plus $B\Rightarrow A$ c’est juste ?
Pourquoi l’algo est comme ça ? Pourquoi c’est comme ça qu’on est arrivé à dire « ca c’est une preuve de ... » ? Ah et je trouve ça bizarre aussi parce que du coup si j’écris
0) $B$
1) $B\Rightarrow B$ (0)
J’ai aucun axiome alors que si je dis
0) $B$
1) $B$
2) $B\Rightarrow B$ (0,1)
Dans les axiomes j’ai $B$ qui apparaît deux fois et en plus $B\Rightarrow (B\Rightarrow (B\Rightarrow )$ ...
Alors qu’intuitivement on a envie de dire que l’hypothèse, qu’on la compte une fois deux fois ou plus c’est pareil, avec ton algo c’est pas le cas ... pourtant « paradoxalement », dans
0) $B$
1) $A\Rightarrow B$ (0)
Là tu ne dis pas « on vire $A$ une seule fois des axiomes » mais tu te permets de l’enlever complètement comme si le nombre de fois que l’hypothèse apparaît compte pas.
J’ai pas vraiment réfléchi à la question et je suis un peu paumé mais ça me parait bizarre.
Sinon pourquoi cette règle du
0) $B$
1) $A\Rightarrow B$ (0)
Alors on vire $A$ etc pourquoi ne pas juste faire l’algo sans ça en écrivant absolument tout ? Intuitivement je pense que je vois l’idée, on veut quand même « dire » quelque chose et effectivement avec ce truc en plus on peut « dire » quelque chose qui permet de se mouiller plus qu’en écrivant tout tout tout mais du coup pourquoi cette règle pourquoi pas une autre ?
Ah autre chose, dans ton algo tu ne précises pas comment se présente la liste finale d’axiomes avant le alors, on met quoi ?
$A,B,C$ alors $D$ ? $A$ et $B$ et $C$ alors $D$ ? $[A+B+C]$ alors $D$ ?
Bon je poste ce que j’ai fait, j’ai juste remplacé $a=0$ ou $b=0$ par $a$ différent de 0 implique $b=0$.
@romyna: ah bin ça m'étonne moins. Pour un cours de logique d'introduction ou d'approfondissement lire un livre écrit par un logicien (logique mathématique je précise car il y a des philosophes qui s'auto - qualifient "logiciens" parfois). Ou au pire par un GRAND mathématicien âgé et qui a bien bifurqué mais JAMAIS par un prof, et encore moins par un prof de prepa (ça ne veut pas dire qu'il n'y a pas peut être des RARES exceptions évidemment). Leur méconnaissance des maths MAIS SURTOUT leur cible (leurs propres élèves) influe beaucoup sur leurs textes (ne pas oublier qu'ils bachottent eux aussi même si c'est "au sens classique") et les conduit à des choix pédagogiques consistant comme d'habitude à préférer dire des trucs faux en se disant "ce sera corrigé ensuite pour les meilleurs mais pour des futurs ingénieurs et les concours c'est mieux comme ça" (j'invite les lecteurs peu familiers du forum à étudier toutes les interventions mathématiques de chaurien par exemple il est assez représentatif)
Pour comprendre leur immersion-nez sur le guidon un exemple d'ailleurs passionnant se trouve dur google "torossian vilani" en allant sur le site de la smf et en cliquant sur la contribution présentée par l'UPS. S'y affiche de façon flagrante la difficulté de cette communauté (son texte inopérant et vide montre , si on ne sait pas d'avance qui c'est , une sorte d'alliance de prof de quatrième énervés disant "faut dire aux enfants d'apprendre leur leçon" (j'exagere un peu j'avoue)).
Je respecte grandement ces travailleurs mais ils taffent beaucoup sont immergés et finissent par se raidir et sortir des maths sans le sentir.
C'est tout bête. Tu as un arbre qui aboutit à P et tu as utilisé tout plein d'axiomes, disons $A_1,..,A_8$. Autrement dit, tu as prouvé en fait (et l'ordre dans lequel on met les $A_i$ n'importe pas):
Maintenant, disons que tu rallonges ton arbre en faisant partir de la racine $P$ une arête et que tu la fais arriver en $A_8\to P$. Et bien ce nouvel arbre ne fait que dire la même chose, sauf que maintenant les axiomes sont $A_1,..,A_7$ et la racine de l'arbre est étiqueté par $A_8\to P$. Mais in fine globalement, tu peux toujours dire que tu as prouvé :
Fondamentalement tu n'as pas tort de remarquer qu'on devrait recenser comme axiomes supplémentaire, l'énoncé de passage: $P\to (A_8\to P)$.
Une remarque: je t'ai donné le système "idéal" pragmatiquement par rapport à la pratique de TOUS les scientifiques, pas seulement des logiciens. Je l'ai configuré pour çà.
Mais les logiciens par exemple ne présenteraient pas le choses comme ça même s'ils voulaient coller le plus possible au format utilisé. Ils diraient que tu n'as droit qu'au modus ponens et quand moi je dis que tu ajoute l'axiome $H_1\to (H_2\to (H_3\to C))$ au moment du recensement quand tu passes sur le noeud étiqueté $C$ qui a 3 fils étiquetés respectivement $H_1,H_2,H_3$, eux ne font pas, ça, ils rajoutent un QUATRIEME fils au noeud $C$ qui est JUSTEMENT $H_1\to (H_2\to (H_3\to C))$, puis ils appliquent un premier modus ponens qui va donner $(H_2\to (H_3\to C))$, puis un deuxième modus ponens qui va donner $H_3\to P$ et enfin un troisième modus ponens qui va donner $P$.
Ce n'est pas que de l'économie d'encre qui m'a fait te refuser cette présentation (de toute façon lourdingue), mais des raisons profondes, hélas un peu longue à détailler et qui puisent leur fondement dans la recherche récente.
Ce qui se passe en fait c'est que le modus ponens n'est pas utilisable vraiment vraiment de chez vraiment. C'est une illusion platonicienne. En effet, c'est un enchainement du type :
Sauf que c'est une règle malhonnête dans le sens où il y a des tas de situations scientifiques où on ne peut pas vraiment savoir si $A=C$ sauf à calculer durant des millénaires une résolution horrible de pointeurs (je considère le point de vue de la programmation massive) divers.
Le "vrai" (en quelque sorte) modus ponens devrait être la règle
qui ne pose aucun problème (il y a un adressage de pointeur à faire et c'est tout, aucune analyse n'est nécessaire).
Le modus ponens est par contre tout à fait LEGITIME et HONNETE à la condition (qui est d'ailleurs la vraie et bonne incarnation des preuves de maths/sciences) que ce soit dans le jeu prouveur-sceptique, car, là, c'est aussi et uniquement un jeu de pointeurs: Lea propose A et Bob choisit entre continuer avec "prouve-moi A=>B" et continuer avec "prouve-moi A".
Mais l'arbre (les preuves papiers) sont hélas des productions solitaires
Concernant le fait que j'efface plusieurs fois A, oui, j'ai en fait décidé (en cours de route) de ne pas t'ennuyer avec les histoires de logique linéaire ou pas. Donc les listes sont tout bêtement vues comme des ensembles (dans mon post, je modifierai si tu veux, mais demain)
Attention concernant ton papier scanné: ton recensement semble bon, mais par contre ta preuve n'est pas du tout sincère, je ne pense pas que tu prouverais comme ça à des gens le truc. D'ailleurs, tu le vois dans ton recensement car figure carrément des axiomes qui disent exactement ce que tu veux prouver.
Et pour info, un arbre étant un graphe orienté, c'est mieux de mettre des flèches et aussi je pense que la plupart des gens préfèrent lire de haut vers le bas (toi tu as mis l'arbre à l'envers avec la racine tout en haut)
Je réponds demain mais vraiment merci pour les pavés, ça doit prendre je sais pas combien de paquets de minutes de pondre un truc comme ça.
Juste, pour la preuve en photo, non c’est pas écrit très gros mais c’est pas le résultat que j’utilise, j’aurais pu détailler plus mais c’est : si a est non-nul alors si ab est nul alors c’est b qui est nul (qui se justifie par le fait que je compose par l’inverse qui du coup existe puis associativité puis inverse fois a fait 1 puis 1 est neutre donc reste b puis truc fois 0 egal 0 ...)
Bin voui, mais c'est toute cette justification qui manque, le reste n'étant que de la logique pure. En ne la mettant pas, tu t'es retrouvé à prouver que $(A\to (B\to C))\to (B\to (A\to C))$, ce qui ne mange pas de pain et de plus, tu as oublié d'inférer "A ou B" de ((nonA)=>B), qui était l'un des moments "forts" de l'aventure, même si personne ne conteste cet axiome.
Et bin, il dit <<si ab=0 et ca=1 alors b=cab=0>>
Puis il installe ça dans une preuve formelle destinée à l'export. Ta dernière phrase du (avant)dernier post à toi montre que tu y penses mais l'a gardé pour toi. C'est typiquement une des difficultés de la plupart (99,5%) des étudiants (les maths sont évidentes, mais, contaminés par une volonté de faire croire le contraire issue du pédagogisme, ils se retiennent la plupart du temps de coucher sur le papier LEURS ARGUMENTS et cherchent des trucs savants aléatoires qu'ils imaginent être plus "fièrement exportables")
Non, tu as tort, et je ne te réponds pas spécialement pour te convaincre toi, je te connais, mais pour convaincre des lecteurs qui t'auraient pris au sérieux lors de cette sortie.
Les maths sont, et sont exclusivement, de la logique appliquée. (*)
Ca n'a pas de sens de dire "je prends une petite rasade modérée de logique élémentaire pour faire des maths" comme si les maths était une forme d'astrologie qui daigne accessoirement et de temps en temps prendre quelques petites menues vitamines de logique pour éviter l'anémie ou la fatigue les jours d'hiver.
Tu n'es pas seul à "refuser" ou "ne pas savoir" ou "ne pas avoir pris conscience" de ça suffisamment complètement (**). Mais par les temps difficiles que vivent les maths au sein de l'enseignement supérieur et de puis leur disparition factuelle de l'enseignement secondaire, je pense qu'il est important d'éviter les sorties, certes plus souvent produites pour faire rire que sérieusement, imagées et fausses-assumées de ce genre.
N'oublie pas que tu as maintenant (c'est une multiplication par 15 depuis les années 2000) des proportions importantes d'élèves qui auraient pu être prometteurs et subissent un choc définitivement décourageant quand ils découvrent trop tard l'exigence hypothético-déductive (définitivement décourageant car ils avaient bien souvent mis un point d'honneur à s'entrainer à ne surtout jamais se laisser aller à produire une déduction, celle-ci étant de leur point de vue, réputée auprès des matheux comme vide donc non rémunératrice en points et du fait de la corruption du secondaire cette attitude leur rapportait beaucoup, donc était encouragée). Ta sortie humoristique peut encourager ce type d'erreur conséquente. [large]En maths on déduit!!!!![/large] et on ne fait rien d'autre
* même si par politesse, il est d'usage de ne pas trop faire crier les matheux professionnels en le leur rappelant, car ils ne veulent pas se croire présentés comme "la science appliquée de quelqu'un"
** je me rappelle encore des cris d'orfraies au début de je signalais sur le forum que tout, je dis bien TOUT théorème de maths est un CAS PARTICULIER d'évidence formelle. Certains n'étaient pas au courant et ce n'étaient pas forcément des débutants ou des amateurs.
Une fois de plus, il ne s'agit pas de démonter une personne physique qui s'est même probablement donné du mal. Mais de signaler ce qui ne va pas et surtout de déconseiller ce genre de doc à qui veut s'introduire à la logique***. Pour ce qui concerne les élèves de l'auteur, on peut espérer pour eux que justement l'un de leurs rôles est d'acquérir une autonomie leur permettant de dépasser leur enseignant (c'est le bon âge et le bon endroit généralement, sinon où?) pour éviter ses fautes.
*** en plus de contenir un grand nombre de fautes ou des devises plus que maladroites, il est inopérant dans le sens que si on n'y connait rien avant, on en sort en n'y connaissant encore plus rien si j'ose dire (les auteurs ne se rendent souvent pas compte que quand ils ne savent pas présenter une notion, ils sortent un tautologie en croyant s'être débarassés du problème (l'exemple typique étant "on dit qu'on s'est donné une fonction f quand pour tout x on s'est donné f(x)", trouvée dans de nombreux livres et battant peut-être le record de la plus mauvaise "définition" présente dans les livres (Celle-ci figure dans un livre de F.Liret par exemple))
« A ou B" de ((nonA)=>B) »
Je vois pas comment justifier ça pour moi « A ou B » c’est une façon d’écrire autrement la phrase ((nonA)=>B du coup je vois pas « ce qu’il y a à démontrer ». C’est quoi du coup la définition de A ou B?
Aussi quand tu dis que j’ai prouvé $(A\implies(B\implies C))\implies (B\implies(A\implies C))$
Si je reprends ce que t’as dit sur l’algo L’arbre prouve:
Si [liste axiome] alors ce qui a marqué avec la racine.
Donc quand tu dis « prouve blabla » ou « tu as prouvé blabla » tu veux dire que je dois trouver un arbre avec pour racine blabla et donc en fait je prouve selon le format que t’as Donné pour faire une preuve:
Si [liste d’axiomes quelconques] alors blabla
Ou alors je dois trouver un arbre de liste vide telle que l’etiquette De la racine est juste blabla donc en fait « prouve blabla » est une abréviation de « si [] alors blabla » ?
Parce qu’avec mon truc j’ai montré normalement
Si $A\implies (B\implies ( (A\implies (B\implies C))\implies C))$ alors $(A\implies(B\implies C))\implies (B\implies(A\implies C))$
Le fameux gag de "il va fournir un pdf". Et quand on regarde, on constate qu'il s'agit, encore et à nouveau, d'un vague truc bâclé... et VIDE de contenu.
En premier lieu, les pages du poly SONT numérotées.
Ensuite de quoi, une fois la page 6 du poly merdifiée par ablation de tous les signes mathématiques, il devient difficile de suivre quoi que ce soit.
Mais au cas où (I) ---telle qu'elle est dans le poly--- serait fausse, il devrait être possible d'exhiber un contre exemple, vérifiant la négation fournie à la ligne d'après, à savoir un $n$ entier et $n \geq 2$ et $n$ premier et $n\neq 2$ et $n$ pair. On risque d'attendre.
les maths sont ,et sont exclusivement, de la logique appliquée.
Non, bien sûr que non !
Bien cordialement.
kolotoko
Si tu veux par exemple (activement) utiliser des connecteurs poétiques (comme "et", "ou", "non", etc), il apparaitra fatalement dans ton arbre des axiomes qui seront recensés. Mais JUSTEMENT ce n'est pas grave, et c'est même le but du jeu: si je t'ai donné ce format c'est, je le redis parce qu'il est idéalement adapté à ce qui se fait et en même temps respecte parfaitement la logique et la recherche la plus récente**. Par exemple, quand les arbitres voient que les seuls axiomes recensés dans ta preuve sont des axiomes du genre (A et =>A; A=>(B=>A), etc, il n'y a aucun problème pour eux à réagir. Je te rappelle que même un modus ponens provoque une inscription de la forme X=>X dans le fichier de recensement. Tu peux d'ailleurs l'ordonner dans l'autre sens et obtenir un recensement de
**En quel sens? Et bien les gens n'aiment pas être bridés: donc je livre un outil où on fait ce qu'on veut, mais où on "subit" le spectacle de voir s'afficher ce qu'on a supposé. Je préfère ce cadre à "on ne peut pas faire ce qu'on veut" et plein de gens se détournent du jeu.
Ca a un autre avantage qui n'a rien à voir avec le présent sujet c'est que ça permet de noter TOUTE copie (qui met des flèches quand-même), aussi délirante soit elle. Par exemple:
1/ je fais KK
2/ je fais $\pi\pi$ (1)
3/ je deviens léger (2)
4/ je fais KK => je deviens léger
5/ ( je fais KK => je fais $\pi\pi$)=>( je fais KK => je deviens léger)
ou encore
1/ ABC est isocèle
2/ ("donc") ABC est rectangle (1)
Donc pour te répondre , non, "prouver blabla" ne veut pas dire construire un arbre sans axiome qui aboutit à blabla, mais par contre, s'il aboutit à blabla avec seulement des axiomes acceptables, tu peux être content.
Concernant ton approche de ((nonA)=>B), qui veut dire "d'office" selon toi "A ou B", il n'en est rien sans axiome, en fait, remplace B par non A et tu obtiens que la platitude (nonA=>nonA) devient le tiers exclus (A ou nonA). Mais en aucun cas il ne t'est interdit de le SUPPOSER. C'était tout le sens de ma remarque à ce propos.
Aux lecteurs du trolls pldx: je citais un document, ce ne sont pas mes propos.
c'est nouveau la tournure : "être, et être exclusivement" ?
S
J'espère que tu comprends bien cet énoncé. Dit autrement, quand un énoncé n'est pas une évidence formelle mais est un théorème de maths, c'est parce que par exemple, il affirme $\forall x: R(x,x)$ alors que l'évidence est $\forall x,y: R(x,y)$, etc, etc, autrement dit, ce qui le rend difficile à voir comme sûr c'est juste qu'il est "trop un cas particulier" d'une platitude grammaticale vraie par définition du langage".
* au sens général (car ce mot est parfois utilisé aussi pour désigner "théorème de la logique propositionnelle finie")
Ton texte est très dense pour moi, j’ai mis du temps à essayer de comprendre et je suis naturellement lent à la détente, en plus j’ai beaucoup de questions sur ce que t’as dit donc du coup je propose la chose suivante: est-ce que tu pourrais confirmer ou reprendre en détaillant simplement (sans perdre d’information si possible mais quand tu dis illusion platonicienne que tu détailles ce que t’entends par ça par exemple bon pour le coup je vois de quoi tu parles je crois mais ça demande quand même un gros effort d’interprétation et au final je suis pas sûr qu’on parle des mêmes trucs) quasiment tout ce que je vais dire. Je sais que c’est une demande un peu égoïste parce que ça demande du temps mais t’as l’air d’accepter d’en consacrer. En gros essayer de passer sur chacun des points que j’essaie d’aborder même si c’est de la bouillie infâme à tes yeux parce que comme j’essaie d’interpréter un peu tout à ma sauce et que j’ai aucune expérience en logique et tout ça va être très brouillon ce que je vais te demander ou essayer de reformuler... bref vraiment merci si c’est possible de faire ça.
Point 1
(C’était dans un de tes premiers messages)
Mettons qu’on me demande de démontrer $(1+1)+1=2+1$.
En français je dirais: on sait que $1+1=2$ et que $1+1=2 \Rightarrow (1+1)+1=2+1$ donc $(1+1)+1=2+1$.
Pour moi c’est ça le modus ponens de ce que j’ai appris parce que j’ai comme hypothèse $A == 1+1=2$ et $1+1=2 (== A)\Rightarrow (1+1)+1=2+1 (==B)$ en gros comme j’ai $A$ et $A\Rightarrow B$ j’ai le droit d’écrire et de prononcer la phrase « alors ça démontre que » $B$, je sais pas comment je le vois dans ma tête quel est le statut du modus ponens par rapport aux phrases que j’écris pour moi c’est un truc un peu « hors maths » qui m’autorise à écrire un truc qui sera « vrai » si on me dit que $A$ et $A\Rightarrow B$ le sont. Ça veut dire quoi vrai quelle différence de statut y a entre le modus ponens et les phrases que j’écris tout ça vraiment j’en sais rien du tout, je suis d’ailleurs très paumé là-dessus. Bref du coup avec ton arbre et ton algo ce qui serait modus ponens serait le nom qu’on donne « au plus petit arbre » avec un sens que je ne saurais pas expliciter mieux sans me perdre qui aurait une fois l’algo preuve appliqué comme axiomes $A$ et $A\Rightarrow B$ et comme conclusion si ça s’appelle comme ça $B$. Donc ce serait l’arbre (et je pense qu’il n’y aurait que lui):
0)A
1)B (0)
(Je suppose que A c’est pas de la fameuse forme qui vire les axiomes)
Là j’ai bien comme axiome $A$ et $A\Rightarrow B$
Or t’as l’air de dire que le modus ponens c’est l’arbre:
0)$A\Rightarrow B$
1)$A$
2)$B$ (0,1)
Et du coup on a bien l’axiome supplémentaire qu’apparemment les mathématiciens enlèvent après le programme preuve qui est $(A\Rightarrow \Rightarrow (A\Rightarrow $.
Pourquoi cette différence, est-ce que c’est moi qui connais une mauvaise définition ?
Donc pour toi j’insiste lourdement un modus ponens c’est (c’est quoi d’ailleurs c’est le nom qu’on donne à un arbre ?) ça aboutit (?) à trois axiomes et pas deux.
Point 2
Quand tu avais décrit l’algo tu n’avais pas fini sur la partie « qu’est ce qu’on prouve » je sais juste qu’il y avait une liste d’axiomes puis un « alors » puis la phrase en racine. Pourquoi je peux interchanger les axiomes entre les Si et les alors si ?
Imaginons que je puisse pas et qu’on donne un sens d’écriture dans les listes et dans leur concaténation et qu’à la fin l’algo fait un PRINT Si blablab alors bloublou en reprenant les axiomes dans l’ordre donné dans la liste en lisant mettons de gauche à droite les axiomes, est-ce que cet algo est « équivalent » à l’algo qui dirait la chose suivante, il sort une liste d’axiomes puis fait une liste de PRINT chaque PRINT donnant un si axiomes alors racine et au final les PRINT donnent toutes les combinaisons possibles en interchangeant les axiomes. On appèlerait phrase prouvée par l’arbre bidule une des phrases après l’un des PRINT, est-ce que c’est un peu dans ce sens là que je suis censé comprendre ? En gros un arbre ne prouve pas une seule chose mais prouve plusieurs phrases qui sont la même en changeant l’ordre des axiomes et ça a été décidé comme ça point ? Qu’est ce que ça voudrait dire que ces deux algos sont équivalents si jamais c’est le cas ? Est-ce que le fait de prouver: $(A\to (B\to C))\to (B\to (A\to C))$ permet de justifier par exemple le fait d’interchanger les axiomes dans la phrase « preuve » ? Si oui comment ?
ATTENTION si jamais les questions sont évidentes dans le sens où tu penses que je peux trouver tout seul la réponse sans y passer 1 an, merci de me le dire et j’essaierai de chercher, là je commence à fatiguer aussi.
Autre chose c’est quoi le statut de la phrase Preuve ? Est-ce que le « si A alors B » que tu utilises dans la phrase preuve est « quelque part de même nature » de que la phrase « $A\to B$ »? Moi tout ce que je vois c’est que c’est si j’ai un arbre qui me donne « si A alors B » alors l’arbre qui reprend le même et rajoute à la racine un fil vers la nouvelle racine « $A\to B$ » alors la phrase preuve du nouvel arbre est « si alors $A\to B$ ». T’as l’air de parler de ça un peu après notamment pour justifier cette règle qui permet de virer un axiome sous condition mais ca me parait toujours pas clair, les arbres sont pas les mêmes, les phrases preuves sont pas les mêmes d’accord on a une liste d’axiome vide mais ensuite ? Tout ce que je sais c’est que le symbole implication se prononce « si alors » à voix haute après je sais pas si y a un lien avec le si alors de ta phrase preuve et qu’est ce qui le justifie (et pour le justifier d’ailleurs faudrait que je le fasse avec un arbre mais la justification serait une nouvelle phrase preuve mais ... et alors ? Y a pas un cercle vicieux quelque part ?)
JE SAIS QUE C’EST SAOULANT de me lire et tu dois peut-être avoir envie de m’égorger mais si c’est possible j’adorerais que tu puisses répondre dans le détail à toutes ces interrogations :-D
Point 3
De ce que je comprends de l’algo j’ai prouvé plutôt si $A_1$ alors si $A_2$
alors si ..... alors si $A_7$ alors $A_8\to P$ ce qui n’est pas censé être pareil, si oui je ne vois pas pourquoi et je ne vois pas comment le montrer parce que pour le montrer faudrait utiliser l’algo preuve sur un arbre avec cette phrase dedans (on est d’accord je peux mettre n’importe quoi comme phrase dans l’arbre pas forcément un truc « conventionnellement » mathématiques ?) qui me sortira une preuve avec son format mais je vois pas quoi en faire.
Point 4
Voilà on commence à rentrer dans ce que je trouve plus dur à comprendre.
Donc si je comprends ce que tu veux dire, pour toi tout arbre est une preuve, les logiciens eux d’une part ils disent que tous les arbres ne sont pas des preuves il faut que pour chaque « arbre élémentaire » il y ait une feuille $A$ une feuille $A\to B$ et une racine $B$ ou alors une feuille A une feuille B une feuille $A\to (B\to C)$ une feuille $B\to C$ et une racine $C$ ou alors etc etc ET EN PLUS dans l’algo preuve on enlève le passage qui rajoute automatiquement une succession d’implication entre les fils dans la liste d’axiomes c’est ça ?
Point 5 De ce que je sais un pointeur est un emplacement mémoire qui contient l’adresse d’un autre emplacement mémoire. Tu as l’air de dire qu’une variable (ou je sais pas quel nom on donne d’ailleurs j’ai du mal avec le statut de ces choses) c’est un pointeur. Mais du coup en maths c’est quoi un pointeur ? En info un pointeur est un objet physique en maths pour filer la métaphore de l’illusion platonicienne, c’est en quelque sorte un pointeur dans l’emplacement mémoire abstrait (ensemble ?) des caractères abstraits appelés symboles de constantes dont la valeur est l’objet mathématiques abstrait platonicien pur :-D
Je veux bien d’ailleurs dans l’absolu y a pas plus de sensation de concret dans ma tête j’ai l’impression quand je me fais croire à la persistance « réelle » du pointeur physique et ce truc là dans tous les cas c’est un sentiment global de cohérence une sensation bizarre de « je parle d’un truc » c’est vrai que pour le pointeur physique le truc est renforcé par la sensation « image visuelle des sens » mais bon...
Tu as l’air de dire que donc si je dis « a » dans une phrase mathématique et qu’à la ligne d’après je redis « a » rien me garantit que c’est le même mais le problème c’est que j’ai vraiment l’impression que justement c’est censé faire partie des « non-dits » des trucs on y croit tous de même qu’on croit que le symbole est vraiment un vrai « symbole platonicien » etc etc dans ce cas jusqu’où je suis censé pousser la « barre platonicienne » des trucs que j’écris en maths ? Apparemment je dois me mettre en mode les symboles sont pas « sensation d’être des taches d’encre toutes différentes » mais « sensation d’être la représentation d’un objet symbole abstrait » bon ça ok de toute façon la « sensation de tache d’encre » est elle-aussi l’objet platonicien de «représentation de l’objet réel tâche d’encre » et je pourrais boucler comme ça longtemps et c’est flou dans ma tête ça me perd et c’est très très frustrant.
Point 6
J’ai rien compris, c’est quoi le prouveur sceptique ?
Point 7
Non d’ailleurs dans un message au dessus t’as dit: A; A; A=>B; A=>(B=>C).
En listant les axiomes de ton premier exemple d’algo preuve. Et en vérifiant je trouve pareil.
Cependant à toute vitesse, je te dis deux choses:
1/ je considère toujours que $(A\to $ est égal à "si A alors B".
2/ la structure de phrases dans laquelle on travaille n'est pas "libre", je considère qu'elle vérifie d'office et "de l'extérieur" $\forall A,B: [(A\to (B\to C))=(B\to (A\to C))]$, mais j'aurais dû te le dire. Mais tu peux omettre cette idée et du coup il faut accepter que l'algo de recensement n'est pas déterministe et ses divers exécutions peuvent donner diverses listes d'axiomes (en fait toutes équivalentes) puisque l'exécuteur tri comme il veut les fils de chaque noeud.
La formulation "un axiome est un énoncé supposé vrai..." est maladroite. on ne suppose pas les énoncés vrais, on les suppose tout court (sans quoi il n'y aurait jamais de raisonnement par contraposition ou par l'absurde).
La réponse est comme je l'ai dit à 110% NON. Il faut se mettre à la place d'un entrant en MPSI 2017: il doit jeter illico ce pdf sous peine d'empirer un niveau de sortie de lycée déjà triste. En effet, il ne fera qu'aggraver une confusion déjà bien installée. Homonymies non averties (sens de vrai défini puis immédiatement utilise autrement etc), incohérences, etc.
Nulle part n'est défini ce qu'est une preuve [...], des définitions de connecteurs logiques sont pseudo-données sans jamais assumer qu'une phrase est une expression comme une autre, etc.
Ce qu'il faut comprendre je pense et comme souvent c'est que certains enseignants de MPSI tapent ce genre de choses informes pour les utiliser comme listes de PRÉVENTIONS de fautes que leur expérience les a conduits à constater trop fréquemment à leur goût. Mais ils devraient changer la disposition pour que ça n'apparaisse pas comme un cours bidon mais plus comme une liste morale et titrer autrement.
J'attends avec plaisir d'être contredit, mais je crains que mon contradicteur ne puisse échapper à ce que je viens d'écrire .. :-)
Dans un texte mathématique apparaissent des énoncés dont le statut de "vérité" est inconnu. Si on sait (ou on suppose) $T\to (X\vee Y)$, $T\to (X\to Z)$ et $T \to (Y \to Z)$ on en déduit bien sûr $T\to Z$. Mais lequel des deux énoncés $X,Y$ est vrai? D'ailleurs l'un au moins de ces deux énoncés est-il vrai? On ne sait pas.
Pire dans un raisonnement par contraposition, on cherche à montrer $\neg T$ et on commence par "supposons $T$" (et déduisons en $Z$-qui serait en l'espèce manifestement impossible). Donc on voit bien que supposer ne peut pas vouloir dire "se forcer à considérer (ou à croire) l'énoncé vrai".
Encore? A mon tour:
La logique c'est juste un cas particulier de langage de programmation fonctionnel (bridé: il y a des types).
La logique est de l'informatique appliquée.
La logique est juste de l'algèbre avec d'autres opérations.
etc etc.
Faut arrêter avec ça, la construction formaliste des maths à laquelle tu fais référence a grosso modo un siècle, ça voudrait dire que les gens ne faisaient pas de mathématiques avant cette date (ce qui est faux bien sûr, regarder tout ce qui a été accompli jusqu'à la fin du 19ème siècle et qui est resté tel quel, puisque les gens ne se trompaient pas malgré l'absence quasi complète de formalisme assumé comme tel).
Prenons la première phrase de ton post :
Dans un texte mathématique apparaissent des énoncés dont le statut de "vérité" est inconnu.
Reconnais-tu que c'est un énoncé ?
Reconnais-tu que cet énoncé possède une valeur de vérité ?
Reconnais-tu que tu lui attribues la valeur "vrai" ?
Enfin, reconnais-tu que la vérité est une notion qui existe, qu'elle est première, et qu'elle est ANTÉRIEURE à toute considération mathématique ?
Après j’avoue je dis ça au pif j’y connais rien j’ai juste l’impression que l’argument « la logique c’est blabla appliqué » n’a pas de rapport avec le fait que malgré tout les maths puissent être de la logique appliquée (bon elles seront aussi des blabla appliqués du coup mais bon et alors ?)
En effet, ce que tu appelles "vérité" est une relation entre faits réels et énoncés dans un langage donné (et non une relation entre faits ou une relation entre énoncés). (Ou si tu veux entre faits réels et concepts pensés, mais j'admets alors que nous pensons suivant un langage donné).
Or il n'y a pas de correspondance naturelle et totale entre ce langage donné et les faits réels. Certaines phrases peuvent être interprétées dans l'ensemble des faits, mais cette interprétation résulte d'une convention qui n'a qu'une définition partielle.
Plus on veut définir l'interprétation d'un grand ensemble de phrases, plus la définition devient complexe, ce qui fait qu'il n'y a pas de définition générale, uniforme, qui permettrait de faire correspondre une phrase à un état de faits.
Même toi, qui pourtant est "essentiellement" d'accord avec moi, tu tiens un propos qui peut être perçu d'une manière que tu ne voudrais pas avec ton rappel qu'avant on était dans le flou. Certains progrès ne sont pas inutiles, même s'ils ne sont pas tous écologiques. Je suis donc obligé de "contrer" (modérément :-D ) ton rappel.
Bien entendu qu'il y a eu des époques où on faisait des maths de manière vague et intuitive et il n'est pas question de dénigrer ces époques. Il y a même eu des époques où où on chassait à mains nues et se comportait comme des sauvages, assez probablement. Par contre, il est très important de souligner que strictement aucun des acquis de ces époques n'a été oublié au moment de la mise au propre récente, autrement dit, comme certains lecteurs fragiles pourraient le penser, il n'existe pas de découverte de maths qui ne soit pas une tautologie formelle pure et dure vérifiable par ordi. Je sais que tu le sais et que les gens compétents et chercheurs sérieux le savent, mais contrairement à un préjugé optimiste, il existe hélas dans la communauté des matheux des tas de gens qui ne le savent pas et peuvent préjuger qu'il existe une sorte de "transcendance irréductible" dans certaines spécialités.
Et il n'y a pas besoin pour trouver de tels ignorants de s'envoler pour la Patagonie, l'Afghanistan ou la Syrie, à nos portes, on peut trouver moult pros [...] qui ont ce préjugé (ie qui ne savent pas qu'ils produisent des tautologies par définition de leur activité): certains croient calculer des choses profondes ou manier du concept transcendantal.
Il est donc important d'être prudent quand on rappelle que les "maths sont difficiles" (c'est vrai qu'elles le sont) car certains y préjugent la présence de "mystère de nature physique" et c'est parfois inconscient chez eux, donc ils ne le contrôlent pas.
Je me force donc à rappeler, avant de me déconnecter, que pour tout théorème de maths $P$, il existe une suite finie $H_1,..,H_n$ d'énoncés tels que $H_1=(H_2\to (H_3\to (...\to (H_n\to P)...)$ avec chaque $H_i$ d'une des formes suivantes:
$A\to (B\to A)$
$(A\to \to ((B\to C)\to (A\to C))$
$(A\to (A\to )\to (A\to $
$A\to (\forall xA)$ (quand pas d'occurence de $x$ dans $A$)
$(\forall x(A\to )\to ((\forall xA)\to (\forall xB))$
+ un axiome non logique assumé comme tel (extensionnalité, compréhension, absurde, etc)
En toute rigueur, même si ce serait long en pratique, une preuve de maths consiste donc en une seule phrase de la forme $Z:= (X\to X)$ où le théorème s'obtient en retirant une par une les hypothèses de $Z$ qui nous paraissent des axiomes.
Christophe c: Si tu peux pense à répondre à mon gros pavé avec les points en gras là, merci pour toutes les réponses que je peux avoir d’ailleurs,même si j’ai peur que ça finisse encore en clash ( vous adorez ça sur ce forum :-D (je plaisante osef personnellement))
la réalité est-elle vraie ?
Moi à Noël, je dépense donc je suis.
S