Les algorithmes permettent-ils de fabriquer automatiquement des théorèmes ?

[Deedee81]

Ou même sans constante

oui, oui, tu l'as fait plus haut Je voulais parler d'une situation "intermédiaire" mettant en évidence que le choix de 0 n'a rien de particulièrement spécial en dehors du fait qu'il est le seul élément qui n'est pas successeur. Et donc qu'il ne faut pas faire de fixette particulière sur le fait d'utiliser la constante 0.

Pour confirmer ce point, j'ai eu à intervenir sur une application écrite en PL-SQL et qui mettait 36 heures à traiter les données d'une journée, le "programmeur" avait totalement procéduraliser le traitement, en utilisant un peu mieux les requêtes SQL (qui traitent des ensembles de données) le traitement a été réduit à 3 mn (oui de 36h à 3mn !)

Tiens, c'est amusant car on a eut le même problème ici aussi en PL-SQL, on a dû s'y mettre à deux pour faire des traitements globalisés (le code était fort complexe et il prenait une semaine d'exécution.... réduit à une heure environ).
(je précise que le code initial était de moi mais marchait très bien et vite.... avant de vouloir améliorer le programme en le rendant full paramétrable par l'utilisateur)
(c'est pas vieux en fait, c'était juste avant la crise sanitaire)

Mais pour le prolog, penser "procédural" est presque une hérésie

Désolé pour ce petit tchat.
-----

[Médiat]

le choix de 0 n'a rien de particulièrement spécial en dehors du fait qu'il est le seul élément qui n'est pas successeur. Et donc qu'il ne faut pas faire de fixette particulière sur le fait d'utiliser la constante 0.

C'est bien la raison pour laquelle, la mythification de 0 et/ou de 1 m'énerve.

Mais pour le prolog, penser "procédural" est presque une hérésie

Absolument (sans le presque), de la même façon que raisonner en terme d'enregistrement au lieu de raisonner en terme d'ensemble de données est une hérésie en SQL

Désolé, moi aussi, pour ce petit tchat.

[Deedee81]

C'est bien la raison pour laquelle, la mythification de 0 et/ou de 1 m'énerve.

C'est un problème général qui ne concerne pas que la science d'ailleurs : les connaissances partielles tendent à conduire à des croyances erronées. Remplacer 0 par chaise à la Hilbert dans les axiomes n'y changerait rien. On se batera encore longtemps contre les moulins

[MissJenny]

(...) 0 n'a rien de particulièrement spécial en dehors du fait qu'il est le seul élément qui n'est pas successeur.

est-ce qu'il existe une axiomatisation de l'arithmétique dans laquelle on définit d'abord Z plutôt que N ? (et donc où 0 n'est pas sans prédécesseur)

[Deedee81]

est-ce qu'il existe une axiomatisation de l'arithmétique dans laquelle on définit d'abord Z plutôt que N ? (et donc où 0 n'est pas sans prédécesseur)

Je ne sais pas si ça existe déjà mais c'est assez évident, par exemple en modifiant légèrement A2 et en prenant A3.



En espérant que quelque chose ne m'échappe pas

[Médiat]

est-ce qu'il existe une axiomatisation de l'arithmétique dans laquelle on définit d'abord Z plutôt que N ? (et donc où 0 n'est pas sans prédécesseur)

Pas à ma connaissance, ce qui ne prouve rien, mais il y a une raison pour cela : le schéma d'axiomes de récurrence deviendrait plus compliqué à écrire et à utiliser (rien de fondamental) ainsi que + et x sans le 0.

Par contre je ne vois pas bien le gain ?

[Médiat]

En espérant que quelque chose ne m'échappe pas

H2G2 n'est pas l'arithmétique (définir + et x sans 0 nécessiterait de profond changements) et si on ajoute 0 au langage je trouve que Peano fait le job

[Deedee81]

H2G2 n'est pas l'arithmétique (définir + et x sans 0 nécessiterait de profond changements) et si on ajoute 0 au langage je trouve que Peano fait le job

Ah oui je pensais juste aux éléments mais effectivement il y a d'autres choses.

[Amanuensis]

Le point "nombre de théorèmes est fini" est discutable

Peut-être plus clair : le nombre de théorèmes qui ont été posés par écrit, de manière lisible par un humain, par au moins un humain ou une machine construite par des humains, à un instant donné, est fini.

[Amanuensis]

c'est évidemment le schéma de récurrence qui les élimine, saurez-vous le démontrer (pas compliqué, mais illustre bien les propriétés de l'implication) ?

Comme personne n'a osé, j'ose.

Faudrait indiquer la forme qui va bien du schéma. Rien qu'en prenant le wiki "Axiomes de Peano", la description n'est pas la même dans l'entrée en français et l'entrée en anglais !

Je vais prendre l'anglais (même si ce n'est pas une formalisation correcte d'un axiome, comme présenté dans cette discussion) :

If φ is a unary predicate such that:

φ(0) is true, and for every natural number n, φ(n) being true implies that φ(S(n)) is true,

then φ(n) is true for every natural number n.

Pour éliminer les boucles on peut prendre φ comme le fait d'être 0 ou qu'en remontant les prédécesseurs on trouve 0. C'est vrai pour 0, et si vrai pour n alors c'est vrai pour s(n).

Un modèle avec une boucle ne respectera pas ce résultat, car les éléments de la boucle n'ont pas la propriété φ, en contradiction avec le schéma de récurrence.

(Je ne l'écris pas en langage formel, j'ai perdu la pratique, mais je ne doute pas que cela soit formalisable.)

Est-ce correct "dans l'esprit" ?

[Amanuensis]

Hmm... Il doit y avoir un loup, dans la définition même de φ. À vérifier/revoir.

[Médiat]

Que le lecteur de passage se rassure, les définitions du schéma d'axiomes de récurrence sont identiques en français et en anglais :

Français

Anglais

[Amanuensis]

Quel est le rôle de y barre dans la seconde formulation ? (Ou de la série des x_i dans la première, pareil.)

[Merlin95]

Satisfaire la première partie de la formule (celle avant l'implication de la "conclusion", répond à la question ?

Sinon j'ai essayé de suivre, j'en suis à essayer de comprendre ce qu'il faut démontrer précisément.

[Amanuensis]

Sinon j'ai essayé de suivre, j'en suis à essayer de comprendre ce qu'il faut démontrer précisément.

À ce que j'en comprends, que le schéma de récurrence empêche que le modèle ait des éléments x tels que s^n(x) = x. (Ils ne peuvent pas être atteints avec une récurrence partant de 0.)

[Le schéma doit aussi virer Z comme modèle, j'imagine. Ne reste plus que N....]

[Superbenji]

Bonsoir,
Les x_i représentent simplement des paramètres de la formule considérée, des variables autres que celle sur laquelle on applique la récurrence. La petite barre du y est un raccourci d'écriture pour les y_i.

[Merlin95]

Ok pourrait-on un peu rendre plus concret un axiome pour commencer de ce schéma d'axiomes ? Mais je ne sais même pas si ça s'exemplifie ?

Sinon mon idée à partir de ma compréhension partielle est que s'il existe x tel que s(x) = x alors le schéma d'axiomes devient fini et donc ne peut plus s'étendre à N qui est infini.

[Médiat]

Ok pourrait-on un peu rendre plus concret un axiome pour commencer de ce schéma d'axiomes ? Mais je ne sais même pas si ça s'exemplifie ?

Vous voulez dire un exemple de récurrence ? Vous pouvez tenter de démontrer que l'arithmétique de Presburger (Peano sans multiplication) permet de démontrer par récurrence que

Sinon mon idée à partir de ma compréhension partielle est que s'il existe x tel que s(x) = x alors le schéma d'axiomes devient fini et donc ne peut plus s'étendre à N qui est infini.

Non c'est faux, pour H2G2,
avec marche bien

[Merlin95]

Je voulais dire un exemple explicite de phi, de x0, x1,x2, etc.

[Médiat]

L'exemple que je vous ai fourni est un exemple est , donc avec un seul paramètre

[Amanuensis]

Bonsoir,
Les x_i représentent simplement des paramètres de la formule considérée, des variables autres que celle sur laquelle on applique la récurrence. La petite barre du y est un raccourci d'écriture pour les y_i.

Je pense que l'inclusion des "paramètres" est juste là pour ne pas réduire le schéma aux prédicats unitaires, comme le fait l'article anglais du Wiki "Peano axioms", mais permettre tout prédicat, même si les autres "objets" n'ont aucun rôle dans le schéma.

[Amanuensis]

Sinon mon idée à partir de ma compréhension partielle est que s'il existe x tel que s(x) = x alors le schéma d'axiomes devient fini et donc ne peut plus s'étendre à N qui est infini.

L'idée est différente, c'est de montrer qu'il ne peut pas y avoir de tel élément si le modèle respecte le schéma de récurrence.

Au fond, c'est assez trivial : une récurrence démarrant à 0 (l'élément sans prédécesseurs) ne peut atteindre que des s^n(0), et comme le schéma parle de "tous les éléments", le modèle se réduit aux s^n(0). Ce qui exclut les x=s(x) et plus généralement les boucles, ainsi que Z.

La difficulté est de formaliser cela en exhibant un prédicat amenant la conclusion. Peut-être que "être de la forme s^n(0)" suffit, s'il n'y avait cette bizarrerie qu'un tel prédicat soit défini par récurrence. Cela fait un peu tautologie !

Mais bon, je n'y connais rien, c'est juste des idées naïves, mal exprimées car je ne prends pas le temps de les formaliser de la manière qu'il faudrait.

[Superbenji]

Je pense que l'inclusion des "paramètres" est juste là pour ne pas réduire le schéma aux prédicats unitaires, comme le fait l'article anglais du Wiki "Peano axioms", mais permettre tout prédicat, même si les autres "objets" n'ont aucun rôle dans le schéma.

Au contraire, ils en ont un. Par exemple prenons une formule . Les x, y, z, w représentent les variables libres de la formule, c'est à dire les variables qui ne sont pas rattachées à un quantificateur à l'intérieur de la formule. La satisfaction de la formule dépends des valeurs données à ces variables libres. Dans le schéma de récurrence plus haut, on lie les variables "paramètres" à des quantificateurs pour dire que la formule vérifie la récurrence quelque soit les paramètres de la formule.

[Merlin95]

Ok je crois que vous tenez l'idée.

Si x = s^n(0) et s(x)=x alors s(x)=s^n(0) donc x=s^n-1(0) donc s^n(0)=s^n-1(0) donc 0=s(0) ce qui est absurde car 0 n'est un successeur.

[Superbenji]

Je pense que l'inclusion des "paramètres" est juste là pour ne pas réduire le schéma aux prédicats unitaires [...]

Mais après, dans Peano, on pourrais très bien restreindre le schéma de récurrence aux formules à une seule variable libre, et c'est équivalent.
Je reprends ma formule , et je créer à partir de celle-ci une nouvelle formule en gardant la variable x et remplaçant toutes les occurrences libres de y, z, w à l'intérieur de la formule par exemple par S0, SSSSSS0, SSS0. J'obtiens alors une formule à une seule variable libre.

[Médiat]

Si x = s^n(0) et s(x)=x alors s(x)=s^n(0) donc x=s^n-1(0) donc s^n(0)=s^n-1(0) donc 0=s(0) ce qui est absurde car 0 n'est un successeur.

Vous démontrez quoi là ?

[Merlin95]

Mon but était de démontrer que'il ne peut exister x tel que s(x) = x. Ce n'est pas rigoureux peut-être mais j'ai juste voulu tenter.

[Médiat]

Mon but était de démontrer que'il ne peut exister x tel que s(x) = x. Ce n'est pas rigoureux peut-être mais j'ai juste voulu tenter.

C'est très bien, mais ce n'est pas ce que vous avez fait ; ce que vous avez démontré c'est qu'il ne peut exister d'élément, de la forme s^n(0) qui soit sont propre successeur, mais comme vous n'avez pas démontré que tous les éléments sont de la forme s^n(0), vous ne pouvez pas conclure

[Amanuensis]

Mais après, dans Peano, on pourrais très bien restreindre le schéma de récurrence aux formules à une seule variable libre, et c'est équivalent.
Je reprends ma formule , et je créer à partir de celle-ci une nouvelle formule en gardant la variable x et remplaçant toutes les occurrences libres de y, z, w à l'intérieur de la formule par exemple par S0, SSSSSS0, SSS0. J'obtiens alors une formule à une seule variable libre.

Je suis bien d'accord. Après, c'est un choix pour chaque auteur, non ? Comme je l'ai indiqué, la page du wiki anglais fait le choix d'un prédicat à un seul paramètre, rendant la formulation plus simple, plus lisible, mais c'est équivalent.

La satisfaction de la formule dépends des valeurs données à ces variables libres. Dans le schéma de récurrence plus haut, on lie les variables "paramètres" à des quantificateurs pour dire que la formule vérifie la récurrence quelque soit les paramètres de la formule.

Oui, bien sûr. Mais quand ils sont répétés à l'identique dans toutes les occurrences du prédicat, on peut les enlever (en définissant un nouveau prédicat) sans changer la validité de la formule, comme vous l'avez ensuite remarqué, non ?

[Amanuensis]

Ok je crois que vous tenez l'idée.

Il faut utiliser le schéma de récurrence, puisque sans lui N union disjointe Z/kZ est un modèle. (C'est Z/nZ qui amène une boucle.)

L'application du schéma au prédicat "x est un s^n(0)", en admettant que c'est un prédicat bien formé, permet de conclure.

Car 0 vérifie le prédicat, si x vérifie le prédicat alors s(x) vérifie le prédicat, donc le prédicat est vérifié par tout élément, i.e., tout élément est un s^n(0), par application du schéma de récurrence.

Ensuite, ce que vous avez montré permet de conclure qu'aucun élément ne vérifie x=s^n(x) avec n>0.