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

[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

Voici les liens :
Axiomes de Peano — Wikipédia (wikipedia.org)
Peano axioms - Wikipedia
-----

[Amanuensis]

Comme on peut le voir la page en français donne (au moins) trois versions du schéma de récurrence, toutes équivalentes mais avec des approches différentes. Les deux premières sont :

Si un ensemble d'entiers naturels contient 0 et contient le successeur de chacun de ses éléments, alors cet ensemble est N.

[...]

Toute partie F de E contenant c et stable par f (c'est-à-dire telle que f(F) ⊂ F) est égale à E.

La troisième version est la plus sophistiquée (le cadre est la théorie des modèles, sans le dire ?), c'est celle pointé par le message précédent.

De même dans la page anglaise on constate factuellement plusieurs versions, certaines mais pas toutes en correspondance avec la page française, dont celle que j'ai citée message #130.

---

Bien sûr, toutes les présentations sont équivalentes.

There are many different, but equivalent, axiomatizations of Peano arithmetic.

[Amanuensis]

PS: Une phrase utile, extraite de la page en anglais, pour suivre les différentes versions :

In Peano's original formulation, the induction axiom is a second-order axiom. It is now common to replace this second-order principle with a weaker first-order induction scheme. There are important differences between the second-order and first-order formulations, as discussed in the section § First-order theory of arithmetic below.

Je ne traduis pas, n'ayant pas le bon vocabulaire en français, même si je comprends bien l'idée. Le texte oppose le "langage du second ordre" au "langage du premier ordre", ou quelque chose du genre.

Je note le "il est maintenant usuel" (it is now common) indiquant que ce n'est pas une obligation (d'utiliser le premier ordre).

[Superbenji]

Bonjour,
C'est logique (ou on peut dire arithmétique, dans le cas présent) du premier ordre, ou du second ordre.
La différence entre les deux, c'est qu'en arithmétique du second ordre, on a deux types de variables distinct. Un type de variable pour les entiers, et l'autre pour les ensembles d'entiers. Le premier est usuellement représenté par des lettres minuscules, l'autre par des majuscules. Il faut ajouter au langage le symbole mettant en relation les deux, sous la forme , et un schéma d'axiomes de compréhension pour les ensembles.
Au premier ordre, l'univers du discours n'est donc fait que d'entiers. Au second ordre, on a les entiers et les ensembles d'entiers, et au second ordre l'induction peut s'exprimer en un seul axiome, au lieu d'un schéma.

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.

C'est bien ça.

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 ?

Je ne suis pas sur de comprendre ce que vous voulez dire. Pourquoi les enlever ?

[Médiat]

Bonjour,

La différence entre les deux, c'est qu'en arithmétique du second ordre, on a deux types de variables distinct. Un type de variable pour les entiers, et l'autre pour les ensembles d'entiers.

La grosse différence c'est qu'en logique du second ordre on n'a pas tout un tas de théorèmes très importants, voire cruciaux (pas de théorème de complétude, au contraire)

[Deedee81]

Salut,

La grosse différence c'est qu'en logique du second ordre on n'a pas tout un tas de théorèmes très importants, voire cruciaux (pas de théorème de complétude, au contraire)

Il me semblait avoir lu que la logique du second ordre était formellement équivalente au premier ordre (après réécriture). Mais si je comprend bien ton "au contraire" il semblerait que non. Est-ce exact ?

[Médiat]

Salut,

Je persiste et signe, je ne vois pas comment une logique complète et robuste pourrait-être équivalente à une logique pour laquelle il n'existe pas de système où elle est à la fois robuste et complète. plus simplement une logique avec Löwenheim-Skolem équivalente à une logique sans.

[Superbenji]

Bonjour,

Bonjour,
La grosse différence c'est qu'en logique du second ordre on n'a pas tout un tas de théorèmes très importants, voire cruciaux (pas de théorème de complétude, au contraire)

Effectivement, oui. Mais de ce que j'en avais lu et cru comprendre cela dépend de la sémantique utilisée, si le domaine des ensembles est P(IN) tout entier, alors oui, et il n'y a même qu'un seul modèle. Mais si on considère des structures ou le domaine des ensembles est restreint à certains sous ensembles de P(IN), on retrouve bien ces théorèmes fondamentaux. Ou j'ai raté quelque chose ?

[Deedee81]

Je persiste et signe

D'accord merci. Ma mémoire m'a probablement joué des tours (ou alors ce que j'avais lu était faux).

[Médiat]

Salut

si le domaine des ensembles est P(IN) tout entier, alors oui, et il n'y a même qu'un seul modèle.

Absolument

Ou j'ai raté quelque chose ?

Le problème est double : pouvoir définir ce domaine (on joue avec un ensemble de cardinal (voire ) avec un langage dénombrable} et de toute façon il ne peut exister de domaine où la logique deviendrait complète et robuste (c'est celui-là le théorème dont je me souviens, mais si vous avez des références ...)

[Superbenji]

Qu'est ce que la robustesse d'une logique ? Il me manque cette notion.

[Médiat]

C'est la réciproque de la complétude (sound en anglais)

PS : cela nous éloigne de la suppression des boucles dans H2G2 + schéma de récurrence (FOL,, bien sûr)

[Superbenji]

Ah oui, la correction ? Je ne savais pas qu'on disais comme ça aussi.

[Médiat]

Ah oui, la correction ? Je ne savais pas qu'on disais comme ça aussi.

C'est peut-être dû à mon âge (pas beaucoup de livres de référence en français, à l'époque)

[Médiat]

C'est peut-être dû à mon âge (pas beaucoup de livres de référence en français, à l'époque)

Je viens de me rappeler un détail : un de mes profs de M2 était américain ...

[stefjm]

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

Je suis embêté par le fait que 0 est le successeur d'un entier relatif.
Dans la définition de l'addition, on s'arrête à 0 parce qu'il n'y a pas de prédécesseur.

Bon, j'y connais pas grand chose en logique formelle, donc je dis peut-être une connerie...

[Médiat]

Je suis embêté par le fait que 0 est le successeur d'un entier relatif.
Dans la définition de l'addition, on s'arrête à 0 parce qu'il n'y a pas de prédécesseur.

Bon, j'y connais pas grand chose en logique formelle, donc je dis peut-être une connerie...

Je n'ai pas envie d'aller trop dans cette direction, mais cela veut seulement dire que la définition de l'addition dans Peano doit être changée pour marcher ici.

[Médiat]

Dans la définition de l'addition, on s'arrête à 0 parce qu'il n'y a pas de prédécesseur.

Je reviens sur ce point : que voulez-vous dire par "on s'arrête à 0"

[Médiat]

Bonjour,

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.

Si vous penser avoir terminé vos réflexions, je posterai deux réponses

[Merlin95]

Oui merci Médiat c'est bon pour moi.

[Médiat]

Ok,

Dans les deux cas ci-dessous, on va montrer que la formule, pour n un entier naïf est valide.

1ère démonstration, purement syntaxique :
Si n'était pas valide, on ne pourrait pas la démontrer et donc la formule serait fausse, sinon l'axiome de récurrence démontrerait , or est valide (sinon 0 serait successeur), c'est donc la partie , qui est fausse, autrement dit il existe un élément tel que et c'est à dire , autrement dit est le successeur de deux éléments distincts, ce qui est impossible cf. les axiomes (je n'ai pas tout écrit, pour vous laisser de quoi réfléchir un peu ).

2ième démonstration, plus intéressante dans la mesure où elle donne un bon exemple de la mauvaise idée que l'on peut avoir de l'implication, même longtemps après le lycée :
Si la structure était un modèle, alors on aurait, dans ce modèle :

est vraie
Dans la partie , est vraie (puisque est vraie pour tous les éléments de
Dans la partie , est vraie (puisque est fausse pour tous les éléments de

L'axiome de récurrence permettrait de conclure : , ce qui est contradictoire.

PS : la aussi il y a quelques non-dits, mais rien de vital, et je voulais garantir la compréhension
PPS : j'ai bien écrit "axiome de récurrence" et non "schéma d'axiomes de récurrence", c'et parfaitement volontaire et justifié

[stefjm]

Je reviens sur ce point : que voulez-vous dire par "on s'arrête à 0"

Quand je me suis amuser à programmer en objet les entiers de Peano avec les successeurs de 0, l'addition était définie différemment pour additionner 0 et récursivement pour les entiers non nuls.
Exemple:
2+3=1+4=0+5=5

public class CPNum {
   protected CPNum pred; // Predessesseur
   protected CPNum succ; // Successeur

   public virtual CPNum Add(CPNum num) {
      return this.pred.Add(num.succ); //addition du prédécesseur et du successeur
   }
}
public class CZero : CPNum{ //Entier particulier sans prédécesseur 
   public override CPNum Add(CPNum num){
      return num; 
   }
}

[Médiat]

...

C'est une implantation de l'addition dans IN, pas une définition de l'addition dans l'arithmétique de Peano, par exemple vous ne dites rien du modèle . Cela fait partie es choses dont on doit se méfier.

[stefjm]

Ah mince, je pensais avoir implémenter la définition

https://fr.wikipedia.org/wiki/Axiomes_de_Peano

Du coup, il y a une couche qui m'échappe.

[Médiat]

Ce n'est pas tout à fait cela que que vous avez implémenté, vous devriez avoir :

2 + 3 = (2 + 2) + 1 = ((2 + 1) + 1) + 1 = (((2 + 0) + 1) + 1) + 1)

Mais surtout, que se passe-t-il si n'est pas de la forme ?

[stefjm]

Pour moi, cela revenait au même et j'avoue que je ne vois pas la différence logique.
Je vois dans votre exemple l'arrêt de la récurrence par le zéro (ou le point de départ).

Les x et y que je manipule sont de la bonne forme : le constructeur de la classe CPNum les construit pour que cela soit le cas.

[Médiat]

Pour moi, cela revenait au même et j'avoue que je ne vois pas la différence logique.
Je vois dans votre exemple l'arrêt de la récurrence par le zéro (ou le point de départ).

On peut démontrer que c'est pareil je faisais juste remarquer que votre implémentation n'est pas les axiomes de Peano, mais un équivalent, mais ce n'est pas le point important

Les x et y que je manipule sont de la bonne forme : le constructeur de la classe CPNum les construit pour que cela soit le cas.

Qu'est-ce que la bonne forme ? Si vous voulez dire que la bonne forme ce sont les élément de la forme , alors ce n'est pas l'arithmétique de Peano que vous avez implémenté

[stefjm]

Qu'est-ce que la bonne forme ? Si vous voulez dire que la bonne forme ce sont les élément de la forme , alors ce n'est pas l'arithmétique de Peano que vous avez implémenté

Du coup, je ne comprends pas en quoi mes objets de classe CPNum ne correspondent pas aux entier de l'arithmétique de Peano?
Je les instancient au fur et à mesure des besoins.

[Médiat]

Je ne dis pas que ce que vous construisez ne respecte pas Peano (il faudrait que je vois tout ce que vous avez fait et que je possède les compétences informatiques adéquates pour en juger), je dis que vous n'avez pas implémenté tout ce qui respecte Peano, par exemple l'existence d'un élément divisible par tous les entiers naïfs (ce qui est compatible avec Peano)

[stefjm]

Je me suis juste créer une classe pour jouer avec les axiomes de Peano, en instanciant un nombre fini d'entiers, sans aucune implémentation formelle. Sans autre prétention que de jouer un peu avec une logique minimale et un peu de programmation objet.