Homo Topi face aux fondements des mathématiques et de la logique - Page 3 — Les-mathematiques.netThe most powerful custom community solution in the world
Oui, et il est préconçu par le passage de l'électricité. Quand tu construis un ordinateur, tu construis un circuit électrique dont le fonctionnement sera ce que tu choisis. Ensuite, tu rajoutes les morceaux "dictionnaire" qui traduisent des impulsions électriques "instructions de l'utilisateur" en "instructions processeur", le processeur reçoit ce signal électrique, et réagit de la manière dont tu l'as préconçu pour que l'utilisateur obtienne ce qu'il a demandé. Il y a au moins deux langages nécessaires ici : le langage "circuit électrique préconçu" et le langage dont l'utilisateur a besoin pour comprendre les instructions qu'il donne à la machine.
Heu ... un ordinateur sans langage natif ne fait pas grand chose. Tous les PC en ont un (le BIOS).
A l'époque où j'ai implémenté un langage sur un ordinateur, le microprocesseur avait déjà un langage (assembleur) implanté. Je pense que c'est encore le cas.
Par contre, les logiciels de calcul formel montrent qu'on peut travailler sur des formules sans signification, pourvu qu'on respecte la grammaire du langage. Nombreux sont ceux qui se font piéger en croyant que le logiciel "calcule", comme on le fait nous.
Tu as eu besoin d'un langage pour concevoir un ordinateur, qui par la suite effectue ce que tu attends de lui. Je ne comprends toujours pas ce que cet argument veut apporter.
The fish doesnt think. The Fish doesnt think because the fish knows. Everything. - Goran Bregovic
Drôle d'idée de vouloir corriger une comparaison fausse. Surtout une comparaison informatique dans une discussion dont l'initiateur a dit que l'informatique ne l'aidait pas à comprendre ... Ça aboutit à une phrase qui n'a pas de sens.
Foys s'adressait principalement à Soc, et je n'ai jamais eu de problème avec l'existence de ce genre de sous-discussions dans mes fils. On finit souvent par apprendre un truc.
Pour moi, le langage natif d'un ordinateur, c'est son fonctionnement en tant que circuit électrique. L'assembleur, c'est déjà une sur-couche d'interprétation. Les compilateurs et autres "dictionnaires bilingues humain-machine", c'est de la décoration qui simplifie l'utilisation d'un ordinateur. Ce qui reste immuable, c'est qu'on a un jour conçu un ensemble d'instructions, un "langage", qu'on a "implémenté" en le construisant physiquement en tant que circuit électrique : un circuit qui prend en entrée les instructions que le concepteur de l'ordinateur a choisi, et qui répond (en suivant les lois de la physique) par une réaction choisie par le concepteur et utilisable par lui. Si ça, ce n'est pas doter la machine d'un langage, alors je ne sais pas ce que c'est. Un langage sert à communiquer, on communique littéralement des instructions à la machine et elle nous communique des résultats. My 2 cents, à voir ce que vous autres en pensez.
D'accord avec Foys sur le fait que le lien avec l'informatique est fondamental. En grossissant le trait, on peut déclarer que les maths sont un algorithme de vérification de preuves formelles (avec un algorithme qui dit si une formule est grammaticalement correcte, un algorithme qui, quand on lui présente une démonstration, dit si elle est correcte - i.e. si ses axiomes sont dans une "liste" fixée à l'avance - etc.). Tout comme le jeu d'échecs est un algorithme qui, quand on lui donne une position et une proposition de coup, décide si le coup est autorisé par les règles ou non.
Ces algorithmes existent et ne sont pas loin d'être triviaux à coder. Je pense que quand on comprend ça, les questions "est-ce que les ensembles existent ?", "qu'est-ce qu'un ensemble ?" perdent beaucoup de leur charme.
Bonjour Georges. C'est une conception parfaitement formaliste des mathématiques, qui, tu le dis, ravale les maths au niveau du fonctionnement du jeu d'échecs. Mais aux échecs, il y a un adversaire ; et plus grave, je ne connais pas d'application des échecs à la physique ou aux sciences de l'ingénieur. Sans être vraiment platonicien, je pense que l'applicabilité des maths à la réalité physique est une grande part de leur intérêt. Je n'ai jamais été convaincu du "pour l'honneur de l'esprit humain" qui est un peu "tour d'ivoire des mathématiciens formalistes". Cordialement.
@Georges Abitbol L'objet de la théorie des ensembles, c'est la relation d'appartenance et non la notion d'ensemble 😅 D'ailleurs, il y a un manuscrit sur la théorie des ensembles que j'écris depuis quelques années, je me suis demandé s'il ne fallait pas que je l'intitule "théorie de l'appartenance"
@cohomologies : bonjour. Je te propose alors "théorie des $\in$-objets", le vocable "objet" peut être remplacé par "ensemble", "classe", (...)
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).
Je n'ai jamais été convaincu du "pour l'honneur de l'esprit humain" qui est un peu "tour d'ivoire des mathématiciens formalistes".
Et pourtant, les mathématiques dans ce qu'elles ont de plus formel, et la logique en particulier, en disent plus long sur le mode de fonctionnement du cerveau que n'importe quelle application à la "réalité physique", quoi que cela puisse être.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
@cohomologies : bonjour. Je te propose alors "théorie des $\in$-objets", le vocable "objet" peut être remplacé par "ensemble", "classe", (...)
Pour illustrer son célèbre paradoxe, Russell avait proposé que l'univers du discours soit la population d'un village et "$x \in y$" une abréviation de "$x$ taille la barbe de $y$".
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$.
Médiat_Suprème, désolé, mais comme ça peut se traiter uniquement par ordinateur (Foys dixit), ça ne parle pas de l'esprit humain en particulier. Seulement de ce qui est commun avec les ordinateurs. C'est pauvre ! Cordialement.
Bonjour @gerard0, il y a une partie non négligeable des maths qui ont été développées "pour l'honneur de l'esprit humain", mais qui interviennent fréquemment dans les maths appliquées à la physique. A mon avis il n'y a pas d'opposition à faire. Certes chaque mathématicien a ses raisons de pratiquer les maths mais tous contribuent à l'avancement de la matière.
Sophisme. Le cerveau humain a conçu des tas de choses utiles -- les lavabos par exemple -- dont la fréquentation ne m'intéresse guère, si ce n'est pour des raisons utilitaires.
Complètement d'accord avec @gerard0, je me suis déjà élevé sur ce forum contre cette vision (à mon sens assez triste) d'une vision formelle des maths qui ne seraient que dérouler des propositions logiques complètement hors sol pour vérifier des preuves. Ce n'est qu'une petite partie des mathématiques.
Tout à fait d'accord avec Math Coss. Et sa réponse est parfaitement adaptée à ce que disait Médiat_Suprème. Quand je pense que c'est moi qu'on traitait de "formaliste" quand j'étais étudiant ...
Ok, donc j'attends avec impatience un papier présentant l'équivalent de Curry-Howard pour les lavabos, ou a minima un exemple de démonstration dans AP faite par un lavabo !
Si vous ne pouvez pas comprendre la différence entre un lavabo et un ordinateur, je ne peux rien pour vous !
Ma remarque n'était pourtant pas bien compliquée.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Sans vouloir lui faire un procès, je trouve que @Médiat_Suprème fait un peu de mauvaise foi pour défendre sa vision des mathématiques. Je pense qu'il ne faut pas essayer de convaincre quiconque qu'il y a une "vision objectivement la meilleure" des mathématiques. Chacun s'y intéresse pour des raisons qui lui sont personnelles. Je ne pense pas qu'il y ait grand-chose à gagner, dans ce fil de discussion avec des amateurs très investis et des vrais professionnels des mathématiques, à convaincre qui que ce soit qu'il ait la mauvaise conception des mathématiques.
Médiat Suprème et @Foys défendent l'importance des ordinateurs, je pense que tout le monde ici admettra que les ordinateurs sont très importants pour les maths et tout le reste aussi. Mais là où moi, je m'arrête, c'est : certes, c'est très intéressant qu'une démonstration mathématique est faisable si, et seulement si, elle est "calculable" par un ordinateur (c'est ça que j'ai l'impression de comprendre, en tout cas, à ces histoires de Curry-Howard) mais il y a deux choses qui me laissent froid là-dedans.
1) Une preuve qui serait "calculée", peut-on en déduire plus que son résultat (c'est une vraie question de ma part) ? Les démonstrations humaines ont l'avantage d'utiliser des idées novatrices qui pourront être appliquées ailleurs, elles enrichissent les maths par autre chose que le résultat démontré. Je ne sais pas si un ordinateur est capable de ça. Parce que du coup, une preuve "calculée", lui fait-on confiance ? Ou bien faut-il faire l'effort de la reconstruire pour se convaincre de ce que l'ordinateur a calculé ?
2) Un ordinateur va démontrer quoi comme résultats ? Si on est d'accord qu'un "pur vérificateur syntaxique" pourra prouver 1000 résultats avant qu'un humain n'en démontre un seul, la question est, quels 1000 résultats ? Tout exercice de mathématiques qui ne figure pas dans un cours sous forme de théorème est une preuve valide, mais d'un résultat considéré comme peu important. Donc il faut néanmoins guider l'ordinateur sur ce qu'on veut qu'il fasse.
Donc je rejoins en un sens @Math Coss et son lavabo : je ne suis pas convaincu qu'un ordinateur est à égal avec l'esprit humain pour faire avancer les mathématiques, je respecte ces machines, les gens intelligents qui ont fait en sorte que ces machines marchent, mais je préfère faire mes mathématiques sans. J'ai des raisons qui me sont personnelles, les défenseurs des ordinateurs comme Médiat Suprème et Foys ne seront sûrement pas d'accord avec moi mais c'est là qu'il faut "agree to disagree" sans porter de jugement sur l'autre.
EDIT : morceau supprimé parce que détaché à un autre fil.
Sans vouloir lui faire un procès, je trouve que @Médiat_Suprème fait un peu de mauvaise foi pour défendre sa vision des mathématiques.
C'est marrant, parce que je n'ai défendu aucune vision des mathématiques, j'ai juste cité des opinions (et quand c'est celle de Krivine, je suppose que c'est acceptable). Je n'ai, entre autres, pas défendu l'importance des ordinateurs, je n'en ai parlé que parce que gerard0 m'a interpellé sur le sujet.
Personne n'a affirmé que "un ordinateur est à égal avec l'esprit humain pour faire avancer les mathématiques", et confondre un ordinateur et un lavabo, honnêtement, ce n'est pas sérieux, pour ne pas dire plus.
Encore une fois, je n'ai pas défendu les ordinateurs (ni n'en ai dit du mal) si je devais défendre quelque chose sur le sujet, ce serait la correspondance de Curry-Howard (en me fichant de l'implémentation).
Ce serait bien que vous lisiez les messages avant d'attribuer aux uns ou aux autres des pensées qu'ils n'ont jamais exprimé.
Bon j'attends toujours la correspondance de Curry-Howard, pour les lavabos
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Quelle mauvaise foi, Médiat_Suprème : "Je n'ai, entre autres, pas défendu l'importance des ordinateurs, je n'en
ai parlé que parce que gerard0 m'a interpellé sur le sujet."
Je ne t'ai répondu sur les ordinateurs que parce que tu en as reparlé, alors que je mettais en doute le fait de ramener les mathématiques à leur partie purement formelle ("Pour l'honneur de l'esprit humain").
C'est vrai que parfois, tu te conduis un peu comme un troll, répondant fortement à ce que tu considères trop vite comme des attaques. Et de ce fait, arrivant vite à des arguments un peu ridicules (ton histoire de lavabo).
C'est tellement lamentable comme mensonge qu'au moins cela me fait rire, relisez et vous comprendrez (peut-être, car j'ai des doutes), c'est vous qui parlez d'ordinateur (avec moi) à 11h21, quant au lavabo c'est Math Coss qui en a parlé, et vous le savez (enfin, je crois) puisque vous l'avez approuvé, d'ailleurs j'attends toujours la correspondance de Curry-Howard, pour les lavabos, seule façon de justifier vos propos.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Eh oui, à 11h21 j'ai montré que tu contredisais Foys, puis tu as redonné de l'importance aux ordinateurs. Je t'accorde que c'est MathCoss qui a parlé le premier des lavabos, mais c'est ta réponse qui m'est restée comme une absurdité. C'est bien de ça que je parlais.
@gerard0 je sais que tu es argumentatif par nature, un peu comme moi, mais laisse tomber. Il a choisi d'être chiant et je doute qu'on verra un comportement positif de sa part dans ce fil sans que nous autres changeons tous notre discours en "oui chef".
@Médiat_Suprème tu es sur un forum où chacun peut donner son opinion, quel que soit son niveau. Si tu viens répondre aux questions des gens, alors traite ces gens comme des apprenants et comporte-toi comme un enseignant. Ton attitude est extrêmement condescendante, et ce n'est pas en créant et alimentant des conflits qu'on répond aux questions. Ton "je vous insulte dès que vous avez la moindre résistance à mes propos", ça marche à l'armée, mais pas ici.
Et si tu préfères avoir une attitude de "de toute façon je m'en fiche, moi je sais que j'ai raison, tant pis pour vous", la porte de sortie est toujours ouverte. Tu n'es pas obligé de répondre dans ce fil.
Ne défendant aucune idée en particulier, je trouve amusant ce genre de reproche, mais bon, j'aurais le plus grand respect pour vous dès que j'aurais reçu la correspondance de Curry-Howard pour les lavabos.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
1) Une preuve qui serait "calculée", peut-on en déduire plus que
son résultat (c'est une vraie question de ma part) ? Les démonstrations
humaines ont l'avantage d'utiliser des idées novatrices qui pourront
être appliquées ailleurs, elles enrichissent les maths par autre chose
que le résultat démontré. Je ne sais pas si un ordinateur est capable de
ça. Parce que du coup, une preuve "calculée", lui fait-on confiance ?
Ou bien faut-il faire l'effort de la reconstruire pour se convaincre de
ce que l'ordinateur a calculé ?
2) Un ordinateur va
démontrer quoi comme résultats ? Si on est d'accord qu'un "pur
vérificateur syntaxique" pourra prouver 1000 résultats avant qu'un
humain n'en démontre un seul, la question est, quels 1000 résultats ?
Tout exercice de mathématiques qui ne figure pas dans un cours sous
forme de théorème est une preuve valide, mais d'un résultat considéré
comme peu important. Donc il faut néanmoins guider l'ordinateur sur ce
qu'on veut qu'il fasse.
Là, tu parles de psychologie, pas de maths : quels résultats "te plaisent", "plaisent à la communauté", "te font gagner une médaille Fields", ça ne relève pas de la logique.
Ensuite, le fait qu'un ordinateur puisse produire des démonstrations est hors-sujet. L'important est qu'un ordinateur peut vérifier sans se tromper, en répondant dans tous les cas, si un texte qu'on lui montre est une démonstration.
Tu mélanges la beauté d'une partie d'échecs, le fait qu'un coup soit "novateur", le fait que les ordinateurs soient très forts aux échecs, et le fait qu'il est trivial, pour un ordinateur ou un humain, quand on lui montre une proposition de coup et une position, répond si le coup est licite ou non.
@Georges Abitbol j'apprends à comprendre ce dont vous autres parlez au fil de la conversation.
Ce que j'avais en tête dans mon dernier message, c'est qu'un humain qui fait des maths, en général il fait des maths "ciblées" : il a en tête un résultat précis qu'il essaie de démontrer. Sémantique comprise, donc. Et en général, ledit résultat "a un intérêt" : c'est une étape dans un raisonnement plus grand, par exemple. Un ordinateur, tout ça il en fait abstration, donc à la limite tu pourrais coder une IA qui essaie de fabriquer un million de "textes mathématiques" par minute et garde ceux qui sont des preuves valides, mais après il faudrait un humain pour faire le "tri sémantique des démonstrations qui servent effecctivement à quelque chose". Après, ce n'était pas de ça qu'il était question, visiblement le sujet était plutôt un assistant de preuve qui ne fait "que" de la vérification syntaxique.
J'ai une question sur ça : si je dispose d'une démonstration, par exemple une démonstration dans ZFC que $\Q$ est un corps archimédien. Admettons que je lla donne à un assistant de preuve, donc sous forme purement syntaxique. L'assistant de preuve vérifie-t-il "ce texte est une démonstration valide" ou bien "ce texte est une démonstration valide de [version purement syntaxique de "$\Q$ est un corps archimédien"] ? La distinction me parait importante.
J'ai une question sur ça : si je dispose d'une démonstration, par exemple une démonstration dans ZFC que $\Q$ est un corps archimédien. Admettons que je lla donne à un assistant de preuve, donc sous forme purement syntaxique. L'assistant de preuve vérifie-t-il "ce texte est une démonstration valide" ou bien "ce texte est une démonstration valide de [version purement syntaxique de "$\Q$ est un corps archimédien"] ? La distinction me parait importante.
@Homo Topi la distinction est inexistante, ton assistant de preuve vérifie que l'objet que tu lui a donné appartient bien à un certain ensemble (l'ensemble des démonstrations du langage). Selon le formalisme que tu prends pour définir ce qu'est une démonstration, définir une fonction qui à chaque démonstration associe sa conclusion n'est en rien un problème.
Un ordinateur, tout ça il en fait abstraction, donc à la limite tu pourrais coder une IA qui essaie de fabriquer un million de "textes mathématiques" par minute et garder ceux qui sont des preuves valides, mais après il faudrait un humain pour faire le "tri sémantique des démonstrations qui servent effectivement à quelque chose".
Dans les années 50-60 des mathématiciens russes avaient voulu générer des théories en choisissant "au hasard" des axiomes 'dans une banque d'axiomes): cela n'avait rien donné
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Dans les années 10 et 20, d'autres mathématiciens ont essayé à nouveau avec des outils plus sophistiqués et cela semble prometteur, cf. ici ou là par exemple.
J'ai l'impression que les liens parlent de démonstrations (et je n'ai aucun doute sur ce sujet) l'expérience russe portait sur la création de nouvelles théories.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Tu vas pinailler sur ce qu'est une « nouvelle théorie » ? Pour le deuxième lien, il n'est donc pas suffisant que l'IA amène à formuler puis démontrer une conjecture inédite en théorie des nœuds, « vraiment frappante et inattendue » (d'après un des referees de l'article de Nature, pas d'après les auteurs) ? ou fasse émerger un concept (une décomposition des intervalles) qui permet de démontrer une formule inédite pour calculer les polynômes de Kazhdan-Lusztig dans le groupe symétrique et d'attaquer la conjecture dite d'invariance combinatoire ?
1) Ce n'est pas pinailler que de ne pas confondre nouvelle théorie et nouveau théorème. 2) Je n'ai pas déconsidéré le travail des IA moderne. 3) Je n'ai pas fait de hiérarchie entre les deux, je dis juste : ce n'est pas pareil.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Une théorie, c'est une famille (finie) de théorèmes, non ? L'IA n'a pas fait émerger un corpus de la taille de la géométrie différentielle ou de la théorie des modèles mais je ne vois pas de différence de nature. C'est tout de même une nouveauté par rapport à la démonstration dans l'esprit du livre « $A=B$ » (et cela n'a pas grand-chose à voir avec la certification de preuve).
Une théorie, c'est une famille (finie) de théorèmes, non ?
Non, au faite une théorie c'est juste un ensemble d'énoncés du langage. Remarque: la théorie des ensembles ZF n'est pas finie. Aussi $\{\perp\}$ est une théorie tandis que $\perp$ est faux. Théorème: Soient $L$ et $T$ tels que $L$ est un langage du premier ordre et $T$ est une $L$-théorie, on appellera $(L,T)$-théorème toute conséquence de $T$.
Une théorie, c'est une famille (finie) de théorèmes, non ?
Effectivement : Non, cf. AP ou ZF (la théorie des groupes infinis, la théorie des relations d'équivalence possédant des classes de toutes tailles finies ...)
Je suis d'accord qu'il n'y a pas de différence de nature entre un axiome et un théorème (dans certains cas, ils sont interchangeables), mais je vois une différence entre partir d'un ensemble vide et inventer des prémices et partir d'un ensemble de prémices pour inventer un théorème (qui peut avoir ses propres prémices supplémentaires.
Une différence, à mon sens importante sinon fondamentale, c'est que pour inventer une théorie, il faut commencer par inventer le langage.
Il ne faut pas respirer la compote, ça fait tousser.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Commencer par, mais un langage ne va pas suffire. Pour moi, une théorie, c'est un ensemble de théorèmes. Un langage et un système de déduction étant fixés, on ne peut pas déduire des choses à partir de rien, donc, il faut aussi des axiomes pour pouvoir créer une théorie non vide. Une théorie devient alors "les résultats qui sont vrais quand on suppose [axiomes]".
La théorie des ensembles est une théorie en ce sens-là : on a un langage et un système de déduction fixés, on fixe une axiomatique (ZFC ou autre), et on construit la théorie constituée de ce qu'on peut déduire de ces axiomes. En ce sens-là, cette TDE c'est presque "toutes les mathématiques", puisque presque tout est fait dans ce cadre-là des ensembles.
La théorie des groupes, par exemple, n'est pas une autre théorie séparée en ce sens-là. On n'ajoute pas un nouvel axiome à une théorie ici, on définit un objet définissable dans la TDE, on lui donne un nom et on l'étudie pour lui-même.
Par contre, si on change l'axiomatique (par exemple remplacer ZFC par ZF sans C, ou remplacer ZFC par ZFC + hypothèse du continu, ou changer complètement d'axiomatique), alors la théorie change : des résultats vrais peuvent devenir faux, des résultats faux peuvent devenir vrais, des énoncés indécidables peuvent devenir décidables ou vice-versa. Donc la liste des résultats admis comme vrais/démontrés vrais change, c'est une autre théorie.
Réponses
Et de sous-discussion en sous-discussions, j'avais un peu perdu le fil
Cordialement.
C'est une conception parfaitement formaliste des mathématiques, qui, tu le dis, ravale les maths au niveau du fonctionnement du jeu d'échecs. Mais aux échecs, il y a un adversaire ; et plus grave, je ne connais pas d'application des échecs à la physique ou aux sciences de l'ingénieur. Sans être vraiment platonicien, je pense que l'applicabilité des maths à la réalité physique est une grande part de leur intérêt. Je n'ai jamais été convaincu du "pour l'honneur de l'esprit humain" qui est un peu "tour d'ivoire des mathématiciens formalistes".
Cordialement.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
désolé, mais comme ça peut se traiter uniquement par ordinateur (Foys dixit), ça ne parle pas de l'esprit humain en particulier. Seulement de ce qui est commun avec les ordinateurs. C'est pauvre !
Cordialement.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Quand je pense que c'est moi qu'on traitait de "formaliste" quand j'étais étudiant ...
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Personne n'a affirmé que "un ordinateur est à égal avec l'esprit humain pour faire avancer les mathématiques", et confondre un ordinateur et un lavabo, honnêtement, ce n'est pas sérieux, pour ne pas dire plus.
Encore une fois, je n'ai pas défendu les ordinateurs (ni n'en ai dit du mal) si je devais défendre quelque chose sur le sujet, ce serait la correspondance de Curry-Howard (en me fichant de l'implémentation).
Ce serait bien que vous lisiez les messages avant d'attribuer aux uns ou aux autres des pensées qu'ils n'ont jamais exprimé.
Bon j'attends toujours la correspondance de Curry-Howard, pour les lavabos
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Les échanges ayant lieu par écrit, il est facile de vérifier tous les points de mon message précédent
J'affirme péremptoirement que toute affirmation péremptoire est fausse
J'affirme péremptoirement que toute affirmation péremptoire est fausse
PS : je n'ai pas contredit Foys, au contraire, aurais-je été trop subtil ? Non, pourtant.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
J'affirme péremptoirement que toute affirmation péremptoire est fausse
J'affirme péremptoirement que toute affirmation péremptoire est fausse
J'affirme péremptoirement que toute affirmation péremptoire est fausse
J'affirme péremptoirement que toute affirmation péremptoire est fausse
2) Je n'ai pas déconsidéré le travail des IA moderne.
3) Je n'ai pas fait de hiérarchie entre les deux, je dis juste : ce n'est pas pareil.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Remarque: la théorie des ensembles ZF n'est pas finie.
Aussi $\{\perp\}$ est une théorie tandis que $\perp$ est faux.
Théorème: Soient $L$ et $T$ tels que $L$ est un langage du premier ordre et $T$ est une $L$-théorie, on appellera $(L,T)$-théorème toute conséquence de $T$.
Je suis d'accord qu'il n'y a pas de différence de nature entre un axiome et un théorème (dans certains cas, ils sont interchangeables), mais je vois une différence entre partir d'un ensemble vide et inventer des prémices et partir d'un ensemble de prémices pour inventer un théorème (qui peut avoir ses propres prémices supplémentaires.
Une différence, à mon sens importante sinon fondamentale, c'est que pour inventer une théorie, il faut commencer par inventer le langage.
J'affirme péremptoirement que toute affirmation péremptoire est fausse
Une théorie c'est juste un ensemble d'énoncés, je l'ai dit plus haut.