Homo Topi face aux fondements des mathématiques et de la logique - Page 2 — Les-mathematiques.netThe most powerful custom community solution in the world
@cohomologies si j'étais un nouveau venu du forum, j'accepterais qu'on dise ça de moi. Depuis des années que j'y viens, je pense avoir prouvé que j'essaie de travailler sérieusement. Je ne mérite pas qu'on parle de moi comme ça.
Désolé mais, là tu as toutes les réponses, tu devrais prendre un peu de temps pour examiner les réponses à tes questions plutôt que de les rejeter en bloc. Je ne vois pas ce qui peut être rajouté aux réponses données.
Donc à ce stade, où est-ce que j'en suis : toutes les maths se font avec ZFC (ou équivalent), ZFC a besoin du calcul des propositions et du calcul des prédicats pour pouvoir être écrit, donc, il faut "fonder la logique" avant de "fonder les maths". Ben oui, sauf que, quand on cherche une "formalisation propre" de la logique, ça devient mathématique.
Ce que je comprends de ce que dit Foys (mais je peux me tromper) c'est que les symboles logiques employés ne font pas l'objet de définitions mathématiques telle que celle d'un groupe ou d'une fonction continue.
Je trouve au contraire que je n'ai aucune réponse. Je ne comprends absolument rien de ce qu'on me raconte depuis avant. J'ai lu des cours sur le calcul des propositions, j'ai lu des cours sur le calcul des prédicats, j'ai lu des cours sur la démonstration, et ici j'ai l'impression qu'on me dit des choses qui vont absolument au contraire de TOUT ce que j'ai appris. Tu peux comprendre que c'est déroutant, j'imagine.
Si 𝐴 et 𝐵 sont des propositions (des énoncés avec une unique valeur de vérité),
Ce sont des propos de ce type qui me font penser que tu devrais tout
reprendre depuis le début et consulter les sources proposées en allant à
ton rythme. Les phrases/propositions/etc n'ont pas intrinsèquement de
"valeur de vérité". Ce genre de considération est ajouté indépendamment.
Les objets manipulés sont syntaxiques avant toute chose.
Je ne comprends pas comment ceci peut avoir le moindre sens. Et quand je dis ça, ce que je veux dire, c'est : j'aimerais qu'on m'explique le sens de ceci.
Littéralement tous les cours de "calcul des propositions" que je connais définissent une "proposition" comme un énoncé ayant une valeur de vérité. Donc d'après Foys, tout ce que j'ai appris est faux ? Je ne comprends pas non plus ce que signifierait "les objets manipulés sont syntaxiques avant toute chose". Qu'est-ce que ça c'est censé vouloir dire ?
Qu'est-ce que vous autres considérez être du "calcul des propositions" purement syntaxique ? Je ne comprends juste pas de quoi vous parlez.
De ce que j'ai appris, dans le "calcul des propositions", 1) les propositions ONT des valeurs de vérité 2) on construit des nouvelles propositions à partir d'autres propositions en utilisant les connecteurs logiques 3) le comportement des connecteurs logiques est défini par des axiomes (permettant de déterminer la valeur de vérité des propositions complexes à partir de celles des propositions atomiques qui les composent, cf les tables de vérité)
Qu'est-ce que ceci a de faux, et si c'est faux, pourquoi je trouve ça partout ? Je suis perdu là-dedans, moi.
Le fait que $A$ et $B$ puissent être des énoncés mathématiques ou des énoncés de la vie courante vient après l'axiomatisation de la théorie de la démonstration.
Dans cette axiomatisation, $A$ et $B$ sont juste des lettres de ton alphabet préféré.
C'est un peu la même chose avec les structures algébriques usuelles : avant de voir des exemples de groupes (dont certains sont connus en fait depuis l'âge de 9/10 ans), on définit un groupe de façon très abstraite et syntaxique.
Ce que je comprends de ce que dit Foys (mais je peux me tromper) c'est que les symboles logiques employés ne font pas l'objet de définitions mathématiques telle que celle d'un groupe ou d'une fonction continue.
Ben, ça c'est au minimum étrangement formulé. Comment un symbole logique pourrait-il avoir une définition en termes de la théorie des ensembles, ça ne fait aucun sens, donc jusque-là on est d'accord.
Mais de là à dire que ces symboles ne sont pas définis, ça c'est bizarre quand même. Si on se sert des connecteurs logiques, c'est bien qu'on leur a associé un comportement précis, et que tout le monde leur associe le même.
Donc comme je disais, je ne comprends pas les réponses qu'on m'a donné.
[Inutile de recopier l’avant dernier message. Un lien suffit. AD]
Donc moi et les autres, on parlait sans se comprendre depuis avant, je pense.
Je vais poser la question comme ça : il y a donc (au moins) quatre "éléments" quand je bidouille les fondements. 1) Il y a les fondements desmathématiques, disons pour simplifier la théorie des ensembles. La théorie des ensembles est constituée au départ d'une liste d'axiomes. 2)3) Pour pouvoir faire quelque chose à partir de ces axiomes, il faut avoir la possibilité de générer des nouveaux énoncés à partir des énoncés déjà existants, d'où le calcul des propositions et le calcul des prédicats. 4) Le reste, ça relève de la théorie de la démonstration.
Là où pour moi ça coince, je pense, c'est quand on me demande de distinguer calcul des propositions et démonstration. Je vais essayer de fabriquer un exemple, histoire d'expliquer ce que je ne comprends pas. Il va me falloir un peu de temps pour ça, j'espère que ça donnera aux autres le temps de comprendre que j'étais juste réellement perdu dans leurs explications qui n'avaient l'air d'avoir aucun rapport avec ce dont je voulais parler, et que je ne suis pas juste un troll/connard venu les embêter. Je reviens quand j'ai ce qu'il faut.
En fait, non. Quand j'essaie de faire les choses, il n'y a pas de problème.
C'est vraiment ce message de @Foys qui m'a complètement fait buguer. Je sais qu'il est 1h30 du matin un dimanche mais j'aimerais vraiment qu'il m'explique ce qu'il a voulu dire quand il sera réveillé.
Bonjour, perso, excusez- moi si c'est hors sujet, j'ai toujours trouvé "bizarre" d'être obligé de poser un ensemble pour impliquer l'existence d'ensembles infinis. Et j'ai toujours trouvé curieux que tout l'édifice ZF soit au fond construit sur l'ensemble vide.
Mais évidemment c'est subjectif. Cordialement. Jean-Louis.
@Jean-Louis moi j'y trouve une logique. Tu construis une théorie formelle abstraite dont les objets, que tu veux interpréter en termes d'ensembles, de "boîtes", sont entièrement définis par leur contenu (exprimé à l'aide du symbole $\in$). Tu vas évidemment commencer par te donner des axiomes qui décrivent le comportement de ces objets : par exemple l'axiome de l'ensemble des parties "étant donné une boîte, il existe une boîte constituée de ses sous-boîtes", ou d'autres axiomes permettant de comparer ou d'opérer sur deux boîtes (extensionnalité, paire...). Tout ça c'est bien beau, mais encore faudrait-il qu'on ait l'existence de boîtes dans notre théorie, sans quoi on n'a aucun objet à manipuler. Alors allons-y, axiome : il existe une boîte. Oui, mais, le bon élève a retenu que j'ai dit juste avant, une boîte est entièrement définie par son contenu, donc mon axiome "il existe une boîte" est imprécis : qu'est-ce qu'il y a dedans ? C'est quelle boîte ? Donc il faut mettre quelque chose dedans, sauf qu'on n'a encore rien dans notre théorie, donc ce qu'on met dedans, c'est, ben... rien. Donc mon axiome devient "il existe une boîte vide", c'est le mieux qu'on puisse faire sans présupposer l'existence d'autres objets qu'on pourrait mettre dans des boîtes.
Mais en effet, c'est subjectif. Ou plutôt, c'est arbitraire. Ces axiomes sont là parce qu'ils sont pratiques, parce qu'ils établissent "facilement" ce qu'on veut (puisqu'ils ont été construits pour). Quand on y réfléchit, est-ce que "il existe un ensemble vide" + "il existe un ensemble contenant l'ensemble vide, chacun de successeurs, et rien d'autre" c'est réellement plus arbitraire que de poser directement "les entiers naturels et l'ensemble des entiers naturels existent" ?
Pour en revenir au message de @Foys (si tu passes par là tu pourras confirmer), je pense qu'il voulait seulement dire qu'en fait on ne manipule que des chaînes de caractères (les énoncés) formées selon certaines règles. Il n'y a pas de valeur de vérité intrinsèque pour une telle chaîne de caractères.
C'est ce que j'ai fini par me dire aussi, j'attends confirmation.
Techniquement, l'énoncé : $(\exists V \forall x \neg(x \in V))$ n'a pas de valeur de vérité puisqu'il n'a même pas de signification tant qu'on ne lui en a pas donné une. Dans la TDE du coup, on déclare que cet énoncé est vrai. On peut toujours le voir comme un simple objet de syntaxe sans lui donner une interprétation ensembliste, et le manipuler syntaxiquement (donc, déclarer qu'il est vrai mais ne pas lui donner de signification pour autant). J'imagine qu'implémenter de la logique dans une machine, c'est justement ça, trouver des manipulations syntaxiques faisables par la machine qui correspondent à la logique qu'on veut. La machine ne se souciera pas de l'interprétation ni de la vérité.
Littéralement tous les cours de "calcul des propositions" que je connais définissent une "proposition" comme un énoncé ayant une valeur de vérité.
C'est faux. Il faut savoir que la plupart de ces "cours" sont écrits par des non spécialistes et racontent littéralement n'importe quoi. La logique est une niche dans le paysage académique et on peut être matheux avec HDR et publis, ne pas la connaître du tout et se tromper lourdement à son sujet (tout en étant capable de produire une prose mathématique correcte de manière fiable et fluide).
La totalité de ce qui suit est implémentable en informatique. Vous pouvez vous amuser à créer une classe "formule propositionnelle" en C++ (ou le langage que vous voudrez).L'emploi du langage ensembliste ne sert qu'à la description des algorithmes.
Le "calcul des propositions",j'imagine que ça doit être l'étude des suites de caratères produites comme suit: On fixe un entier $d$ et des lettres $P_1,...,P_d$ appelées "variables propositionnelles".
-Une variable propositionnelle est une formule propositionnelle
-si $A,B$ sont deux formules propositionnelles alors $nand(A,B)$ est une formule propositionnelle (les autres connecteurs seront définis à partir de celui-ci selon des méthodes qu'en principe le lecteur connaît déjà, on utilise nand pour gagner du temps).
On construit une fonction $\mathbf{val}$ qui à une formule propositionnelle et un élément de $\{0,1\}^d$ renvoie un élément de $\{0,1\}$ de la façon suivante:
1°) Pour tout $\vec e\in \{0,1\}^d$ et tout $k\in \{1,...,d\}$, $\mathbf {val} (P_k,\vec e) := e_k$ ($k$-ième coordonnée de $\vec e$)
2°) Pour tout $\vec e \in \{0,1\}^d$ et toutes formules propositionnelles $V,W$, $\mathbf {val} (nand(V,W),\vec e) := 1 - \mathbf {val} (V,\vec e) \mathbf{val} (W,\vec e)$
Ceci permet donc à chaque formule propositionnelle $F$, de faire correspondre une fonction qui va de $\{0,1\}^d$ dans $\{0,1\}$ et qui à $\vec e\in \{0,1\}$ fait correspondre $\mathbf {val} (F,\vec e)$ ("valeur de vérité de $F$ dans l'environnement $\vec e$").
L'affirmation consistant à dire qu'une "formule propositionnelle" est toujours vraie ou fausse n'est donc qu'un cas particulier de la FAUTE GRAVE consistant à confondre l'expression d'une fonction avec une des valeurs de son image.
C'est d'autant plus problématique qu'avec cette présentation on voit déjà que les fonctions associées à certaines formules propositionnelles seront constantes tandis que pour d'autres elles ne le seront pas. Par exemple avec $d:=3$, $P_1 \wedge \neg P_1$ et $(P_1 \Rightarrow P_2)\Rightarrow ((P_2 \Rightarrow P_3)\Rightarrow (P_1 \Rightarrow P_3)) $ donnent des fonctions constantes (donnant tout le temps respectivement $0$ et $1$) tandis que la fonction associée à $P_1 \wedge P_2$ n'est pas constante.
La propriété suivante (triviale) permet de faire le lien entre valeurs de vérité et démonstration:
Soit $e\in \{0,1\}^d$ et $T_e:= \{F \mid \mathbf {val} (F,e) = 1\}$. Alors pour toutes formules propositionnelles $A,B$, si $A$ et $A\Rightarrow B$ sont dans $T_e$ alors $B\in T_e$.
On dit qu'une formule $F$ est une tautologie si la fonction $x\mapsto \mathbf{val} (F,x)$ est constante égale à $1$. Cela revient à dire que $F$ appartient à $T_e$ pour tous les $e\in \{0,1\}^d$. Il est clair d'après ce qui précède que pour toutes formules $A,B$, si $A$ et $A\Rightarrow B$ sont des tautologies, alors $B$ en est également une.
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
Donc tu distingues les règles de syntaxe d'une part, et fonction de vérité d'autre part. Je trouve ça très, très bizarre (dans le sens où je vois revenir l'ouroboros logique...)
Tu es obligé de définir une syntaxe pour distinguer les propositions que tu veux étudier et celles que tu laisseras de côté (parce que, pour toi, elles n'auront aucune signification).
Ensuite, tu définis les règles de sémantique qui donnent sens aux propositions que tu acceptes comme syntaxiquement correctes.
Enfin, tu définis des règles de logique pour déterminer une valeur de vérité aux différentes propositions sémantiquement significatives.
Tu ne peux pas te passer d'un alphabet pour définir ta syntaxe, ni de règles syntaxiques. La plupart de ces règles sont définies "récursivement", mais cela ne signifie pas que l'on a besoin d'axiome de récurrence ou de nombres entiers pour le faire. Pour chaque proposition, on peut vérifier en un nombre fini d'étapes si elle est ou non syntaxiquement correcte.
l'énoncé : $(\exists V \forall x \neg(x \in V))$ n'a pas de valeur de vérité puisqu'il n'a même pas de signification tant qu'on ne lui en a pas donné une. Dans la TDE du coup, on déclare que cet énoncé est vrai. On peut toujours le voir comme un simple objet de syntaxe sans lui donner une interprétation ensembliste, et le manipuler syntaxiquement...
Oui, d'ailleurs même les démonstrations ne sont que des "manipulations syntaxiques" qui permettent d'obtenir une formule à partir d'autres formules (les hypothèses) mais il n'y a pas besoin d'interpréter les formules, leur donner du sens.
Oui, c'est juste une question de formalisation. J'ai besoin qu'on oublie toute question d'implémentation informatique pour le moment.
Dans cet article, le paragraphe "Structure" est particulièrement intéressant. Contrairement à ce que racontait Foys, il n'y a aucune notion de "fonction" ici. C'est ça qui me rendait fou : la notion de "fonction" de vérité, c'est une fonction dans la théorie des ensembles, théorie qui a besoin d'axiomes, axiomes qui ont besoin d'une valeur de vérité définie par une fonction de vérité.
Donc :
- on se donne un alphabet pour les variables de notre théorie (en calcul des propositions, ces variables sont des propositions)
- on se donne une liste finie de connecteurs logiques
- on se donne une liste finie de règles de syntaxe : comment assembler variables et connecteurs pour former des nouvelles proposition
- on se donne une liste finie de tables de vérité : une sémantique, pour associer à chaque assemblage syntaxique sa valeur de vérité "en fonction de" celles de ses propositions constituantes
Ensuite, il faut des premiers énoncés dont on connait la valeur de vérité : les axiomes d'une théorie à construire.
Je n'ai pas besoin de théorie des ensembles dans mes messages. A nouveau, tout est implémentable informatiquement (et le point de vue informatique est important je dirais, c'est lui qui rend concret toutes les constructions dont on parle). L'emploi du langage ensembliste n'est là que pour permettre une description plus rapide des programmes informatiques dont il est question.
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
@Homo Topi : bonjour. Après avoir lu en diagonal ton lien, tu auras soin de t'attarder sur la section La déduction naturelle, à partir de laquelle les notions rudimentaires d'ensemble, de multi-ensemble et de fonction font leur apparition.
Le chat ouvrit les yeux, le soleil y entra. Le chat ferma les yeux, le soleil y resta. Voilà pourquoi le soir, quand le chat se réveille, j'aperçois dans le noir deux morceaux de soleil. (Maurice Carême).
- on se donne une liste finie de tables de vérité : une sémantique, pour associer à chaque assemblage syntaxique sa valeur de vérité "en fonction de" celles de ses propositions constituantes.
Cette partie est facultative pour définir ce qu'est une démonstration par exemple (mais les règles de démonstration auront à être choisies de sorte qu'il y a un lien entre concepts sémantiques et concepts syntaxiques)
Ensuite, il faut des premiers énoncés dont on connait la valeur de vérité : les axiomes d'une théorie à construire.
Les axiomes d'une théorie sont arbitraires. On n'a pas toujours le luxe de connaître leur "valeur de vérité". En plus dans les théories courantes des mathématiques il est possible que ces axiomes soient contradictoires entre eux sans qu'on le sache (théorème de Gödel). Ça n'invalide en rien le fait que certains textes sont des démonstrations et d'autres non.
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
par exemple l'axiome de l'ensemble des parties "étant donné une boîte, il existe une boîte constituée de ses sous-boîtes",
L'axiome des parties est plus subtil que ce que croit la majorité des gens, d'ailleurs il serait mieux exprimé sous la forme : "étant donné une boîte, il existe une boîte constituée des boîtes qui sont ses sous-boîtes"
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Oublie l'informatique. Je réfléchis à comment fonder la logique mathématique, sur papier. Je pars de rien. Je veux "fonder" "la" "logique mathématique" dans le but de "fonder" les mathématiques après, grâce à cette logique. Et je ne comprends pas comment une fonction de vérité peut être légitimement introduite ici, puisque les mathématiques n'existent pas encore dans mon système.
L'article de wikipédia prend soin de distinguer sémantique et syntaxe quand même.
Moi aussi, il me semble ! Donc c'est bon.
Plus tard, tu me dis qu'on ne connait pas toujours la valeur de vérité des axiomes. J'ai encore du mal avec ça. Je veux bien qu'on puisse construire une démonstration "purement syntaxique" dont le résultat serait un "théorème" vide de tout sens "mais légitimement démontré". Quel est l'intérêt ?
@Homo Topi : bonjour. Après avoir lu en diagonal ton lien, tu auras soin de t'attarder sur la section La déduction naturelle, à partir de laquelle les notions rudimentaires d'ensemble, de multi-ensemble et de fonction font leur apparition.
Techniquement, ils apparaissent plus dans le formalisme du calcul des séquents. À part quand ils disent "ensemble d'hypothèses", mais bon, là on pinaille.
@Médiat_Suprème Oui, je sais, j'écris les choses à la va-vite parce que 1) ce n'est pas le cœur de mon propos 2) les gens savent de quoi je parle.
Homo Topi a dit :Et je ne comprends pas comment une fonction de vérité peut être légitimement introduite ici, puisque les mathématiques n'existent pas encore dans mon système.
Mais pourquoi veux-tu introduire une fonction de vérité ou quoique ce soit de mathématique ?
Une démonstration est un texte donc la "cohérence grammaticale" est validée par un système d'axiomes, rien de plus.
@JLapin sans vouloir prendre partie dans ta discussion avec @Homo Topi, j'aimerais juste rajouter cette information : quand une théorie est complète, on peut définir une fonction qui à chaque énoncé du langage va associer sa valeur de vérité selon cette théorie. J'ai déjà dit à @Homo Topi qu'on ne fondait pas la logique avant de fonder les mathématiques, mais que la logique est une branche des mathématiques au même titre que l'algèbre, mais bon, cette remarque ne lui a pas paru satisfaisante.
@cohomologies non, ça ne me parait pas satisfaisant, puisque ça me paraît fondamentalement incohérent. C'est l'ouroboros : aucune "branche" des mathématiques ne peut exister sans qu'on fasse deux choses. 1) fonder les mathématiques (par exemple, théorie des ensembles ZFC), 2) fonder les règles qui permettent de faire des raisonnements pour établir des résultats rendant les mathématiques non-vides. Si le problème ici est qu'on ne parle pas de la même chose, alors d'accord, au moins l'un de nous deux a mal compris l'autre. Si ces règles, et je pense que là il s'agit de ce qu'on avait appelé théorie de la démonstration, se formalisent sans mathématiques "ensembles ZFC", je n'ai aucun problème. C'est juste difficile pour moi de dissocier syntaxe et sémantique, l'aspect "syntaxe pure" peine à avoir le moindre intérêt à mes yeux. Une démonstration ne sert à rien si sa conclusion n'est pas un résultat dont on sait s'il est vrai, je trouve. C'est juste ça.
C'est juste difficile pour moi de dissocier syntaxe et sémantique, l'aspect "syntaxe pure" peine à avoir le moindre intérêt à mes yeux.
Tu sais qu'on pourrait dire la même chose de n'importe quel théorème portant sur des groupes abstraits ? Ca reste de la syntaxe pure tant que ce n'est pas appliqué.
Un sous-groupe d'un groupe est un groupe. La preuve consiste juste à écrire les axiomes qui vont bien de façon grammaticalement correcte.
D'ailleurs, un certain nombre d'étudiants commencent à être perdus dans les maths (qui n'ont alors plus le moindre intérêt à leurs yeux) lorsque arrivent ces définitions et énoncés très formels.
Pour le coup, oui, un théorème comme celui-là contient peu de "vraie" démonstration puisque les idées sont très basiques. Cependant, dans l'absolu, ce n'est pas "que" de la syntaxe. Tel énoncé/axiome est-il vrai pour tout $x \in H$ ? Oui, par définition de $H \subseteq G$ et de "$G$ est un groupe". Il y a de la "vérification sémantique" si je puis dire, même si ici elle est triviale.
Il y a de la "vérification sémantique" si je puis dire, même si ici elle est triviale.
Il n'y a aucune sémantique dans les preuves formelles. Toutes les preuves dans ZFC peuvent s'écrire formellement via les séquents (voir images ICI). C'est nous dans notre tête qui interprétons automatiquement les formules pour leur donner du "sens", ce qui nous aide à trouver la démonstration que l'on cherche.
À part ça il y a aussi une définition précise de la sémantique et un lien avec les preuves (syntaxiques), c'est le théorème de complétude de Gödel qui le fait.
Mais de toute façon pour éviter l'ouroboros il faut accepter de commencer par quelque chose d'admis. Par exemple si tu considères la théorie des ensembles comme système fondationnel des mathématiques alors il faudra accepter que les symboles $\in,\exists,\forall$, que tu utilises pour définir les axiomes de ZFC, ne sont pas des ensembles et donc sont à "l'extérieur" de ta formalisation des mathématiques.
Il y a zéro ouroboros; simplement @Homo Topi rejette les exemples qui l'établissent (et qui rappellent que les objets syntaxiques dont il est question sont informatiques). A un moment ça devient lourd de poser les questions et choisir les réponses.
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
Je demande depuis le début qu'on ne fasse pas d'informatique, tu persistes à vouloir ramener MES questions à la manière dont TU voudrais que je les pose, mais ça ne marche pas comme ça. Je voulais comprendre les fondements des mathématiques et du raisonnement, un ordinateur n'a rien à voir là-dedans, j'ai quand même le droit de poser moi-même le cadre de mes questions ! J'arrive à être d'accord avec d'autres, donc le problème vient-il vraiment de moi ?
Je n'ai rien "rejeté" du tout, j'ai simplement expliqué pourquoi je n'étais pas d'accord avec ce qu'on me disait. J'ai des arguments, si tu ne les aimes pas, ce n'est pas de ma faute. Si tu lis les derniers messages en détail, j'accepte beaucoup de réponses parce qu'elles m'ont convaincu, y compris des choses que tu as dites. Si je ne suis pas convaincu, j'ai le droit d'être sceptique. Mon rôle n'est pas d'être un mouton qui dit "oui chef", je suis un apprenant qui demande à être convaincu. Je ne sais même pas pourquoi tu râles maintenant alors que les derniers messages ont été riches en éclaircissemens.
Tu choisis peut-être le cadre de tes questions, tu ne choisis pas celui des réponses. L'informatique et la logique sont intimement liées, elles se recoupent largement (ce n'est pas un hasard si les modules de logique et de théorie de la démonstration se trouvent dans les cursus d'info et d'info théorique à la fac, plutôt que les cursus de maths). Ca fait bientôt un siècle que c'est comme ça. Tes questions ont la forme d'une demande d'aide. Ce n'est pas un problème mais dans ce cas tu ne peux pas te permettre d'être autoritaire sur les réponses, ou pire de décréter la véritable nature des maths en citant tes amis qui seraient d'accord. Le mec qui vient se faire sortir de son appart en flammes il va dire aux pompiers "c'est pas comme ça qu'on met la sangle"?
Par contre si tu viens faire du militantisme bah tu te débrouilles et moi je dis ce que je veux (je ne suis peut-être pas comme ton prof de maths que tu peux enfumer en trois secondes).
A nouveau si tu es dans une démarche de demande d'aide: en fait l'informatique contient des réponses à tes questions. Il y a un parallèle entier entre programmes informatiques et preuves de maths et de logique (la correspondance de Curry-Howard). Coder et démontrer c'est littéralement la même chose.
Tu insistes pour dire que la logique contient un cercle vicieux? Je pose la question qui gêne: pourquoi les ordinateurs peuvent-ils exister (ils n'ont pas besoin manifestement que les opérations qu'ils font existent au préalable). Et je ne parle pas qu'à toi. Je parle aussi aux lecteurs. Je veux qu'ils voient ça. Je n'en peux plus de cette propagande anti-formaliste.
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
@Foys je me considère plutôt formaliste, mais c'est bizarre à quel point nos points de vue divergent. Bien sûr je ne remets pas en cause ce que tu dis. Je ne peux juste pas prendre l'informatique ou la théorie de la démonstration comme points de départ. J'adore lire des points de vue qui divergent du mien, j'apprends toujours quelque chose.
Tu aurais pu remarquer que j'ai arrêté d'insister sur l'existence d'un cercle vicieux (et que ça pourrait vouloir dire que j'ai compris un truc). Et, je ne suis juste pas "autoritaire sur les réponses", ça c'est n'importe quoi : si tu essaies d'expliquer un truc à un élève/étudiant, et qu'il ne comprend pas avec ta manière habituelle d'expliquer, tu changes ta façon d'expliquer ou tu le traites juste de connard ? Si je suis un blaireau en informatique, et que tu veux me convaincre avec des trucs d'informatique, alors, explique un peu plus, adapte-toi à l'apprenant. Sinon ça ressemble juste aux profs qui mettent 0 dès qu'on utilise une autre méthode que la leur.
Je ne fais aucun militantisme, ça aussi c'est n'importe quoi. Si demander qu'on m'explique un truc qui a été formalisé avant les ordinateurs (démonstrations, logique et fondements) sans me parler d'ordinateurs c'est du militantisme, on n'est pas sortis de l'auberge. D'ailleurs, les autres ont réussi à me faire comprendre des choses, et ça s'est passé calmement. J'ai juste l'impression que tu t'offusques du fait que je trouve que ta façon d'expliquer ne m'a personnellement pas aidé à comprendre. Mais ça c'est juste normal que ça arrive de temps en temps, la pédagogie qui fonctionne dépend de l'apprenant.
A nouveau si tu es dans une démarche de demande d'aide: en fait l'informatique contient des réponses à tes questions. Il y a un parallèle entier entre programmes informatiques et preuves de maths et de logique (la correspondance de Curry-Howard). Coder et démontrer c'est littéralement la même chose.
Oui, d'accord, et ce n'est pas la première fois qu'on m'entionne ça dans le fil. J'essaierai de m'y intéresser un peu, mais je comprends très peu l'informatique, donc je préfère des explications "texte" que des explications "code", c'est juste ça.
Je ne sais pas non plus à quelle "propagande anti-formaliste" tu fais référence. Je n'ai pas de problème avec le formel. Seulement pour moi dans le contexte syntaxe/sémantique "le formel" ne voulait rien dire à lui tout seul, donc j'ai un peu résisté à ce qu'on me racontait. Encore une fois, on a abouti à des conclusions dans ce fil. Je ne veux pas qu'il y ait d'animosité entre qui que ce soit ici. Je ne peux pas empêcher les gens de penser ce qu'ils penseront de moi, mais, encore une fois, je ne suis juste pas d'accord qu'on me prête des mauvaises intentions. J'ai insisté pour que les enseignants s'adaptent à l'apprenant, j'estime que c'est la base. Que j'ai parfois un sale caractère, je veux bien qu'on me le reproche et l'admettre. Mais qu'on m'accuse de ne pas avoir voulu faire l'effort de comprendre alors que j'étalais en détail ce que je ne comprenais pas, ça c'est tout bonnement absurde.
@Foys les ordinateurs peuvent exister mais Homo Topi n'est pas le seul qui pensait voir un cercle vicieux dans tout ça... pas mal de gens voient un cercle vicieux de prime abord. Même le Cori Lascar évoque le cercle vicieux, certes en disant qu'il n'y en a pas mais il l'évoque quand même. Moi aussi j'ai cru en voir un à l'époque car je m'attendais à ce que la logique me donne des réponses qu'elle ne peut simplement pas donner.
Plus précisément voici un exemple tiré de ma lecture du Cori Lascar. Imaginez que vous êtes confronté pour la première fois à la logique et que vous vous attendez qu'elle puisse formaliser toutes les mathématiques. La première phrase que vous lisez du chapitre 1 est celle-ci : On considère un ensemble $P$ non vide, fini ou infini, qu'on appelle ensemble des variables propositionnelles... Enjoy
On ne rêve pas on vient bien de lire les mots : ensemble, non vide, infini.
Bref voici un extrait de l'introduction, toujours du Cori Lascar, qui aide à y voir plus clair @Homo Topi j'espère que ça va t'aider comme ça m'a aidé :
Je n'ai pas de problème avec le formel. Seulement pour moi dans le contexte syntaxe/sémantique "le formel" ne voulait rien dire à lui tout seul,
Et alors ? Je vous rappelle ce que disait Hilbert : Il doit toujours être possible de substituer "table", "chaise" et "chope de bière" à "point", "droite", "plan" dans un système d’axiomes géométriques. Attribuer un sens aux symboles permet de démontrer l'existence de dieu, cf. Gödel.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Foys disait bien que la plupart des cours de logique mathématique sont conçus par des non-spécialistes et mal fichus. Est-ce la faute de celui qui essaie d'apprendre de prêter des fonctions à un outil qui n'a pas ces fonctions, si l'outil lui a été mal présenté ?
Je pense qu'il est "naturel" de vouloir voir dans la logique mathématique une formalisation abstraite des règles de démonstration qu'on utilise pour faire des mathématiques, c'est souvent présenté de manière à faire croire ça. Si c'est des conneries, ben, comme on parle des fondements, des choses sur lesquelles l'apprenant essaie de se baser, si on ébranle ça il faut vite rattraper l'apprenant qui tombe avec tout ce qu'il croyait savoir.
@Homo Topi il y a le point de vue de @Foys et le point de vue (théorie naïve)->(théorie des modèles)->(théorie formelle des ensembles). Il me semble que tu voulais avoir les avantages des deux réunis en un. Mais, comme les jeunes le diraient "it's a package deal", il faut choisir un point de vue. (Le mien de préférence 😆)
Ma vision est que les mathématiques ont besoin d'un langage déjà existant pour être définies (j'entends par là une langue maternelle). Ce langage a déjà structuré notre pensée et nous y incorporons ensuite les mathématiques. Donc en plus des axiomes que l'on décide de définir pas tout à fait ex nihilo il y a déjà une structure de pensée qui prééxiste et qui a par exemple empêché Euclide de prendre conscience de tout ce qu'il présupposait, et qui fait sans doute de même avec nous ses successeurs. Croire que l'on détient un modèle parfait relève de l'orgueil ou de la foi. On peut en revanche se satisfaire de cet objet imparfait qui permet tout de même de faire des merveilles tout en se convaincant que l'on ne sait rien.
The fish doesnt think. The Fish doesnt think because the fish knows. Everything. - Goran Bregovic
J'ai l'impression que les trois quarts des messages de ce fil aurait pu être évités si Homo Topi s'était plongé un minimum dans la théorie des modèles, qui fait comprendre la distinction fondamentale entre la syntaxe et la sémantique.
Ma vision est que les mathématiques ont besoin d'un langage déjà existant pour être définies (j'entends par là une langue maternelle). Ce langage a déjà structuré notre pensée et nous y incorporons ensuite les mathématiques. Donc en plus des axiomes que l'on décide de définir pas tout à fait ex nihilo il y a déjà une structure de pensée qui prééxiste et qui a par exemple empêché Euclide de prendre conscience de tout ce qu'il présupposait, et qui fait sans doute de même avec nous ses successeurs. Croire que l'on détient un modèle parfait relève de l'orgueil ou de la foi. On peut en revanche se satisfaire de cet objet imparfait qui permet tout de même de faire des merveilles tout en se convaincant que l'on ne sait rien.
Y a-t-il besoin d'un langage déjà existant pour faire fonctionner un PC?
Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
Réponses
Je veux comprendre ça:
https://fr.wikipedia.org/wiki/Déduction_naturelle
1) les propositions ONT des valeurs de vérité
2) on construit des nouvelles propositions à partir d'autres propositions en utilisant les connecteurs logiques
3) le comportement des connecteurs logiques est défini par des axiomes (permettant de déterminer la valeur de vérité des propositions complexes à partir de celles des propositions atomiques qui les composent, cf les tables de vérité)
1) Il y a les fondements des mathématiques, disons pour simplifier la théorie des ensembles. La théorie des ensembles est constituée au départ d'une liste d'axiomes.
2)3) Pour pouvoir faire quelque chose à partir de ces axiomes, il faut avoir la possibilité de générer des nouveaux énoncés à partir des énoncés déjà existants, d'où le calcul des propositions et le calcul des prédicats.
4) Le reste, ça relève de la théorie de la démonstration.
Cordialement.
Jean-Louis.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
À part ça il y a aussi une définition précise de la sémantique et un lien avec les preuves (syntaxiques), c'est le théorème de complétude de Gödel qui le fait.
Mais de toute façon pour éviter l'ouroboros il faut accepter de commencer par quelque chose d'admis. Par exemple si tu considères la théorie des ensembles comme système fondationnel des mathématiques alors il faudra accepter que les symboles $\in,\exists,\forall$, que tu utilises pour définir les axiomes de ZFC, ne sont pas des ensembles et donc sont à "l'extérieur" de ta formalisation des mathématiques.
Bien sûr je ne remets pas en cause ce que tu dis.
Je ne peux juste pas prendre l'informatique ou la théorie de la démonstration comme points de départ.
J'adore lire des points de vue qui divergent du mien, j'apprends toujours quelque chose.
Plus précisément voici un exemple tiré de ma lecture du Cori Lascar. Imaginez que vous êtes confronté pour la première fois à la logique et que vous vous attendez qu'elle puisse formaliser toutes les mathématiques. La première phrase que vous lisez du chapitre 1 est celle-ci : On considère un ensemble $P$ non vide, fini ou infini, qu'on appelle ensemble des variables propositionnelles... Enjoy
On ne rêve pas on vient bien de lire les mots : ensemble, non vide, infini.
Bref voici un extrait de l'introduction, toujours du Cori Lascar, qui aide à y voir plus clair @Homo Topi j'espère que ça va t'aider comme ça m'a aidé :
Je vous rappelle ce que disait Hilbert : Il doit toujours être possible de substituer "table", "chaise" et "chope de bière" à "point", "droite", "plan" dans un système d’axiomes géométriques.
Attribuer un sens aux symboles permet de démontrer l'existence de dieu, cf. Gödel.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Il me semble que tu voulais avoir les avantages des deux réunis en un. Mais, comme les jeunes le diraient "it's a package deal", il faut choisir un point de vue. (Le mien de préférence 😆)
On peut en revanche se satisfaire de cet objet imparfait qui permet tout de même de faire des merveilles tout en se convaincant que l'on ne sait rien.
Y a-t-il besoin d'un langage déjà existant pour faire fonctionner un PC?