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

[andretou]

Je récapitule : pour obtenir l'ensemble ordonné des entiers naturels, il faut nécessairement partir, non des axiomes de Peano, mais d'un modèle de Peano auquel il faut adjoindre l'addition.
C'est correct ?
-----

[Médiat]

Comment un modèle de Peano pourrait-il ne pas avoir d'addition définie ?

[gg0]

Ou dit autrement : On peut définir l'ensemble ordonné des entiers naturels sans définir l'addition. Ni la multiplication, ni l'exponentiation. Inversement, l'usage des axiomes de Peano permet de définir l'addition, la multiplication, ... On voyait ça autrefois en terminale Math élem.

[Amanuensis]

Je reviens, après avoir laissé tomber la discussion (et zapper plein de messages, mais j'imagine qu'aucun n'était sur les points 4 et 5 ce ce message-ci), à une voie parallèle, sans rapport direct avec les messages juste avant.

1) Si on accepte les réalisation avec le 0 du modèle ayant plusieurs représentations, on pourrait penser qu'il y a une "méta-règle" comme quoi si A et B sont deux représentations, alors l'union disjointe de A et B en est une aussi. Est-ce le cas (en espérant, comme pour la suite, que ma terminologie naïve soit comprise) ?

2) Si la méta-règle s'applique, alors je ne vois aucune limite au nombre de possibilités, c'est plus que beth_1, plus que n'importe quel cardinal. Correct ?

3) Il me semble qu'un postulat supplémentaire suffit pour réduire aux cas avec un seul 0 du modèle (et donc se rapprocher des entiers), genre qqs x et y, (x n'a pas de prédécesseur et y n'a pas de prédécesseur) <=> (x=y).

Correct ?

4) La représentation que j'avais proposée était par l'union (normale, non disjointe) de Z/2Z et N, ce qui n'entre pas dans ce qui précède puisque Z/2Z seul n'est pas (il me semble) une représentation du modèle. Est-ce bien une représentation du modèle ?

5) Et ma question reste, si on peut éliminer ces cas en rajoutant un seul axiome ? (Je n'en trouve pas, mais cela ne concerne que mes limitations.)

[Médiat]

1) Je vous avoue que je ne suis pas sûr de comprendre : s'il y a un symbole de constante 0 dans le langage, il ne peut y avoir qu'un seul 0 dans le modèle, et même si l'ensemble sous-jacent contient plusieurs éléments que l'on serait tenté d'appeler 0, il ne peut y en avoir qu'un qui possède ce nom dans l'ensemble (parce que c'est un ensemble), et qu'un seul dans le modèle (pas forcément identiques).Qu'appelez-vous "représentation" exactement ?

2) cette remarque me fait penser qu'il y a une confusion quelque part, il ne peut pas y avoir plus de modèles dénombrables si le langage est fini.

3) cet axiome est conséquence des 3 axiomes donnés

4) j'ai bien parlé d'isomorphisme : avec vos règles pour s est bien isomorphe à

5) Non, il y a un théorème (très beau lui-aussi) qui dit que si une théorie axiomatisée avec une infinité d'axiomes, est en fait finiment axiomatisable, alors on peut extraire une axiomatisation finie de toutes axiomatisations (et de celle que j'ai fournie, il est triviale que c'est impossible)

En espérant avoir apportée quelques éclairages, n'hésitez pas à en demander plus.

[Superbenji]

Bonsoir,

5) Non, il y a un théorème (très beau lui-aussi) qui dit que si une théorie axiomatisée avec une infinité d'axiomes, est en fait finiment axiomatisable, alors on peut extraire une axiomatisation finie de toutes axiomatisations (et de celle que j'ai fournie, il est triviale que c'est impossible)

Quel est le nom de ce théorème ? Ou pouvez vous en dire plus ?

[Médiat]

Bonsoir,

Quel est le nom de ce théorème ? Ou pouvez vous en dire plus ?

Je ne lui connais pas de nom, mais c'est un classique de la logique classique du 1er ordre, c'est une conséquence directe du théorème de compacité

[Médiat]

Bonjour,

Je rajoute un détail en espérant que cela éclaire un peu les choses :

Dans l'exemple de la théorie H2G2, le modèle représenté par la suite (5, 0, 1, 2, 3, 4, 6, 7, ...) signifiant que l'ensemble sous-jacent de ce modèle est IN, que l'interprétation du symbole de constante dans ce modèle est le 5 de IN, et l'interprétation de s est définie (sur IN, bien sûr) par :

s(5) = 0
s(0) = 1
s(1) = 2
s(2) = 3
s(3) = 4
s(4) = 6
et pour tout n > 5 s(n) = n + 1 (*)

Dans ce contexte, il y a trois "choses" méritant le nom "zéro" :

1) le 0 du langage, c'est un symbole de constante qui va être utiliser dans l'établissement de la théorie
2) le 0 de IN, qui ne va pas servir à grand chose ici, mais qui peut être utilisé
3) le 0 du modèle, c'est à dire l'élément de IN qui interprète le 0 du langage, ici, c'est donc le 5 de IN, qui va être utilisé pour des particularités de ce modèle (démontrer des théorèmes vrais dans ce modèle mais indécidable dans la théorie)

Il est important de faire la différence (e statut) entre 2) et 3), surtout quand (et c'est le plus courant) ils sont égaux (le 0 du modèle est le 0 de IN)


(*) J'ai bien écrit "pour tout" et non , car (cf. message #85), n, ici, n'est pas un objet mathématique (c'est un entier naïf, ou intuitif)

[Liet Kynes]

Bonjour,

Je travail un peu sur ce qui est dit et j'avoue que j'ai l'impression de comprendre mais je reste à mon avis scotché dans un ancrage limitatif qui parasite ma réflexion bref j'avance pas vraiment.

Prenons un exemple simple Le langage est (0, s) où 0 est un symbole de constantes, et s une fonction appelé successeur, et 3 axiomes (ceux de Peano)


Si je prends comme ensemble de base IN = {0, 1, 2, ...}, à votre avis il y a combien de façon de définir la fonction successeur ?

Avec ce qui a pu être dit et notamment le dernier message dans mon esprit je reste sur l'idée que ces trois axiomes définissent la fonction successeur et que donc il n'y a qu'une façon de la définir mais que l'on peut très bien remplacer dans le langage le symbole 0 par tout autre nombre. 0 ou tout autre symbole aurra un sens quand on pose x-y=0 (ou autre chose).
Je ne sais pas si je suis dans un début de commencement d'un amorçage vague de bonne compréhension cependant

[gg0]

Bonjour.

"ces trois axiomes définissent la fonction successeur" ??? Pour définir une fonction, il faut connaître toutes les images. Quelle est l'image par s de 15414 ? (qui est s(15414) ?). Bien sûr, ta réponse ne doit utiliser que les trois axiomes, puisque tu dis "ces trois axiomes définissent la fonction successeur".

[Médiat]

Bonjour,

Les axiomes définissent les propriétés que doit avoir une fonction pour que l'on ait envie de l'appeler successeur.

Dans certains ensembles bien connus, , , , il y a des fonctions naturelles, qui méritent d'être appelées successeur, vérifient-elles tous les axiomes ?

Dans , muni des relations et opérations usuelles une telle fonction n'existe pas naturellement, et il est impossible d'en définir une.

Dans , muni des relations et opérations usuelles une telle fonction n'existe pas naturellement, mais il est possible d'en définir une.

[Amanuensis]

1) Je vous avoue que je ne suis pas sûr de comprendre : s'il y a un symbole de constante 0 dans le langage, il ne peut y avoir qu'un seul 0 dans le modèle, et même si l'ensemble sous-jacent contient plusieurs éléments que l'on serait tenté d'appeler 0, il ne peut y en avoir qu'un qui possède ce nom dans l'ensemble (parce que c'est un ensemble), et qu'un seul dans le modèle (pas forcément identiques).Qu'appelez-vous "représentation" exactement ?

= modèle. J'ai toujours eu un problème (purement langagier) entre "langage" (= ? "théorie") et "modèle" (= représentation). J'ai un mauvais câblage sémantique, pour moi un modèle est quelque chose dont peut faire différentes "représentations" (comme des portraits par exemple) ...

Mais cela répond à ma question : un seul élément qu'on appelle 0 (du langage). Donc on ne peut pas prendre ω+ω comme modèle, en prenant comme 0 du langage les deux éléments sans prédécesseur. Pourtant cela respecterait les axiomes !

2) cette remarque me fait penser qu'il y a une confusion quelque part, il ne peut pas y avoir plus de modèles dénombrables si le langage est fini.

Oui, mais c'est (pour moi) conséquence de l'interdiction ("méta-règle") du 0 multiple.

3) cet axiome est conséquence des 3 axiomes donnés

Je ne vois pas comment. Je le verrais comme une "méta-règle". Si je prends ω+ω (et qu'on accepte les "0 multiples"), tous les axiomes me semblent s'appliquer : les zéros n'ont pas de prédécesseurs, tout élément est un zéro ou un successeur, même successeur <=> égalité. Cette interprétation est interdite par la méta-règle.

4) j'ai bien parlé d'isomorphisme : avec vos règles pour s est bien isomorphe à

Oui, message que je n'avais pas lu.

5) Non, il y a un théorème (très beau lui-aussi) qui dit que si une théorie axiomatisée avec une infinité d'axiomes, est en fait finiment axiomatisable, alors on peut extraire une axiomatisation finie de toutes axiomatisations (et de celle que j'ai fournie, il est triviale que c'est impossible)

Mon problème vient de l'idée de "schéma d'axiomes", que je prends pour une multiplicité dénombrable d'axiomes. Et c'est bien la "solution" que je voyais.

Le côté bizarre reste : comment définir cette notion de "schéma d'axiomes", qui fait apparaître un "n", pour ensuite parler de l'axiomatisation des entiers ? Ne sont-ils pas "déjà là" à cause de cette idée de schéma ?

Ma question reste : peut-on ajouter un axiome unique (pas un schéma d'axiomes) virant les Z/nZ ?

[Amanuensis]

Pour les "zéros" multiples, l'obstruction vient peut-être de (une règle ?) la transitivité de l'égalité ? C'est évidemment violé avec cette idée de "zéro multiple".

[Médiat]

= modèle. J'ai toujours eu un problème (purement langagier) entre "langage" (= ? "théorie") et "modèle" (= représentation). J'ai un mauvais câblage sémantique, pour moi un modèle est quelque chose dont peut faire différentes "représentations" (comme des portraits par exemple) ...

Mais cela répond à ma question : un seul élément qu'on appelle 0 (du langage). Donc on ne peut pas prendre ω+ω comme modèle, en prenant comme 0 du langage les deux éléments sans prédécesseur. Pourtant cela respecterait les axiomes !

Langage + axiomes "génèrent" les théorèmes, c'est à dire la théorie (le raccourci langage + axiomes = théorie, n'est pas "criminel")

-structure = ensemble + interprétation (*) du langage dans cet ensemble

Modèle = -structure qui vérifie les axiomes.

Oui, mais c'est (pour moi) conséquence de l'interdiction ("méta-règle") du 0 multiple.

C'est lié à la fonction d'interprétation : l'interprétation d'un symbole de constante est un (*) élément de l'ensemble sous-jacent (votre méta-règle)

Le côté bizarre reste : comment définir cette notion de "schéma d'axiomes", qui fait apparaître un "n", pour ensuite parler de l'axiomatisation des entiers ? Ne sont-ils pas "déjà là" à cause de cette idée de schéma ?

C'est parce qu'il s'agit d'un entier naïf, je pourrais facilement remplacer ma définition des par


et espérer que tout le monde comprenne la signification des ...

La chose totalement interdite (j'ai du mal à l'écrire tellement c'est affreux) :

Je serais damné sur 50 générations pour avoir écrit cela

Ma question reste : peut-on ajouter un axiome unique (pas un schéma d'axiomes) virant les Z/nZ ?

Il me semble avoir répondu non, si ma réponse n'est pas clair, j'expliciterai volontiers, mais je ne sais pas, ce qui vous ennuie dans ma réponse


(*) Je pourrais développer si nécessaire

[Amanuensis]

Encore une question, toujours en relation avec ce qu'on peut faire ou pas (et pourquoi).

Au message 73, j'ai proposé un modèle "non-standard", je ne l'ai pas mis "complet" pour ne pas alourdir, je vous la mets ici : où et les sont des cardinaux (dénombrables si on veut utiliser IN comme ensemble sous-jacent.

Qu'est ce qui limite α et les β à des cardinaux dénombrables ? (Je ne comprends pas "si on veut utiliser IN comme ensemble sous-jacent" ; il y aurait une autre possibilité ?)

[Amanuensis]

Il me semble avoir répondu non, si ma réponse n'est pas clair, j'expliciterai volontiers, mais je ne sais pas, ce qui vous ennuie dans ma réponse

Juste pas lue. Un truc m'a énervé dans cette discussion.

[Médiat]

Qu'est ce qui limite α et les β à des cardinaux dénombrables ? (Je ne comprends pas "si on veut utiliser IN comme ensemble sous-jacent" ; il y aurait une autre possibilité ?)

IN est dénombrable, donc dire que je veux que IN soit mon ensemble sous-jacent cela veut dire que je veux des modèles dénombrables, or si ou l'un des n'est pas dénombrable, l'ensemble sous jacent ne le sera pas, par exemple est bien un modèle non dénombrable de H2G2

[Médiat]

Juste pas lue. Un truc m'a énervé dans cette discussion.

Quoi donc ? Elle m'a semblé plutôt paisible

[Amanuensis]

C'est parce qu'il s'agit d'un entier naïf, je pourrais facilement remplacer ma définition des par


et espérer que tout le monde comprenne la signification des ...

Cela m'était clair, y compris l'interdiction mentionnée après.

Mon sentiment de bizarrerie reste, exprimable comme la distinction entre "entier naïf" et entier formalisé. Ou encore "signification des ..." = récursion implicite dans la tête du lecteur, et donc "présence" a priori du concept des entiers. On utilise la présence préalable du concept pour le formaliser, il me semble. Un appel à la "nature humaine" ? Ne pourrait-on imaginer un être qui a un langage suffisant pour comprendre la théorie des modèles expliquée en langage courant, mais qui n'aurait pas le concept de récursion (d'entier naïf), qui ne comprendrait pas les "..." ? Comment lui expliquerait-on alors ? Par la formalisation de la récursion ?

Ou encore que signifie le "tout le monde"... Tout les humains ?

[Médiat]

Je comprends ce qui vous dérange, j'aimerais vous "prouver" que ce n'est pas grave (et qu'il y a pire)

D'abord il y a pire : le schéma de récurrence dans Peano, comment expliciter ce que veut dire "pour toute formule "


Ensuite ce n'est pas grave :

Imaginons que dans H2G2 vous ayez démontré un théorème, cela veut dire que les 3 axiomes initiaux plus l'infinité des axiomes supplémentaires démontrent votre théorème.
Par compacité j'en déduis qu'une partie finie des hypothèses démontrent votre théorème, c'est à dire qu'il existe un plus grand n (naïf) qui apparaît dans cette démonstration disons pour simplifier que le plus grand nécessaire soit 4, alors les axiomes dont vous avez besoin pour votre démonstration sont :

Il n'y a plus d'entier naïf, ni de ...

C'est à dire que les entiers naïfs ou et ... sont juste un moyen de communication

Ou encore que signifie le "tout le monde"... Tout les humains ?

Tous les humains qui ont la (bonne) volonté de comprendre

[Amanuensis]

Ensuite ce n'est pas grave :

Imaginons que dans H2G2 vous ayez démontré un théorème, cela veut dire que les 3 axiomes initiaux plus l'infinité des axiomes supplémentaires démontrent votre théorème.
Par compacité j'en déduis qu'une partie finie des hypothèses démontrent votre théorème

Pas mal. Nombre d'axiomes infini, mais démonstrations finies. Et comme l'humanité ne saura proposer des théorèmes qu'en nombre fini (y compris ceux débités par des algorithmes), on n'aura besoin au total que d'un nombre fini d'axiomes du schéma. Bel exemple d'infini potentiel.

[Médiat]

Bel exemple d'infini potentiel.

Absolument, ce qui est la marque des entiers naïfs qui ne peuvent apparaître en acte.

Le point "nombre de théorèmes est fini" est discutable, mais en tout état de cause, c'est bien parce que c'est aussi un infini potentiel que ce n'est pas grave.

[andretou]

Non, au mieux on peut dire les entiers naturels sont un modèle de Peano

Pour bien comprendre, est-ce que les entiers naturels sont à l'arithmétique ce que les points (tels que définis par Hilbert) sont à la géométrie euclidienne, c'est-à-dire des "systèmes d'êtres" dont l'existence est acceptée sans discussion ni préalable ?
http://www.pedagogie.ac-aix-marseill...-02-31_973.pdf

"Concevons trois différents systèmes d'êtres : les êtres du PREMIER système, nous les nommerons "points" et nous les désignerons par A, B, C... ; les êtres du DEUXIEME système, nous le nommerons "droites" et nous les désignerons par a, b,c... ; les êtres du TROISIEME système, nous les nommerons plans et nous les désignerons par alpha, béta, ..."

[Médiat]

Pour bien comprendre, est-ce que les entiers naturels sont à l'arithmétique ce que les points (tels que définis par Hilbert) sont à la géométrie euclidienne, c'est-à-dire des "systèmes d'êtres" dont l'existence est acceptée sans discussion ni préalable ?

Système d'êtres : vocabulaire peut-être en vogue en 1900 mais totalement abandonné depuis.
Existence : Qu'est-ce que cela veut dire ?
Discussion (ou préalable) : avec qui ? pourquoi ?


Sinon, les entiers naturels sont à l'arithmétique de Peano, ce que tous les éléments d'un modèle d'une théorie sont à cette théorie. Pour la géométrtie c'est un peu plus compliqué puisque les éléments d'un modèle se répartissent dans 3 sous ensembles distincts (3 prédicats unaires)

[Médiat]

Bonsoir,

Je reviens quelques secondes sur ce point :

Pour éviter les boucles, il faudrait ajouter le schéma d'axiomes

Cette solution est parfaitement adaptée ici, mais ces axiomes n'apparaissent pas dans Peano, et pourtant les modèles, même non-standard, ne possèdent pas de boucle(s), 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) ?

[Liet Kynes]

Bonjour,

tout le monde est tombé en panne de compréhension ?
Perso toujours j'ai un gros soucis avec le zéro du langage et je me demande si ce n'est pas simplement le fait que je ne comprends pas vraiment ce qu'est un symbole de constante.
En même temps j’intègre bien le fait que dans R cela ne peut pas marcher.
Pour l'image de 15414 peut être n'importe quel élément de l'ensemble sous-jacent?

[Médiat]

Bonsoir,

Avant de choisir un langage, les seuls choses que l'on peut écrire sont les tautologies de la logique choisie (classique du premier ordre).

Si je reprends l'exemple :

Le langage est (0, s) où 0 est un symbole de constantes, et s une fonction appelé successeur, et 3 axiomes (ceux de Peano)
0 n'est pas successeur
Tous les autres élément sont successeurs


On pourrait les remplacer par
Le langage est ( s) où s est une fonction appelé successeur,
Il existe un élément qui n'est pas successeur
Il n'y a qu'un seul élément qui n'est pas successeur


C'est la même chose, sans symbole de constante (qui n'est donc pas obligatoire), mais c'est un peu plus cryptique, et les axiomes pour empêcher les boucles deviennent illisible ; Ne sachant pas, à ce stade, dans quel ensemble je vais travailler, pour manipuler cet élément unique, qui n'est pas successeur, le plus simple est de lui donner un nom, c'est à dire créer un symbole de constante

[Liet Kynes]

Merci pour le détail, l'approche cryptique complète bien. Le B2 est particulièrement fin. Je vais reprendre l'ensemble de ce qui est dit; je pense être capable d'accéder à une vision claire.
Dans mon flou actuel, le symbole de constante me semble être l'action de poser un repère.

[Deedee81]

Salut,

Dans mon flou actuel, le symbole de constante me semble être l'action de poser un repère.

C'est plutôt une étiquette, un simple nom collé à un des éléments définis par les axiomes. On pourrait d'ailleurs écrire des axiomes en utilisant la constante 1, ce n'est pas très difficile (un rien plus lourd dans la formulation sans plus).

Mais le fait est qu'il existe dans cette axiomatique un élément qui n'est le successeur d'aucun, il est tout de même un peu particulier. Et ça simplifie les choses de le nommer et de l'utiliser pour écrire les axiomes. Si c'est ça que tu appelles "poser un repère", alors oui on peut dire ça.

As-tu déjà eut l'occasion de programmer en Prolog ? Ca peut aider car on a la même chose : des variables et des constantes qui ne sont que des noms attribués à deux objets du langage (c'est vrai aussi des autres langages mais avec le prolog un programme a la forme d'une suite d'axiomes et donc c'est plus proche de ce qu'on discute ici).
(EDIT PS : chose amusante, quand je programmais en prolog la plus grosse difficulté était de constamment devoir éviter la "pensée procédurale".... c'est à croire qu'on est biologiquement programmé nous aussi, programmé pour penser de manière procédurale Désolé pour ce petit aparté psycho-personnel )

[Médiat]

Bonjour,

On pourrait d'ailleurs écrire des axiomes en utilisant la constante 1, ce n'est pas très difficile (un rien plus lourd dans la formulation sans plus).

Ou même sans constante

(EDIT PS : chose amusante, quand je programmais en prolog la plus grosse difficulté était de constamment devoir éviter la "pensée procédurale".... c'est à croire qu'on est biologiquement programmé nous aussi, programmé pour penser de manière procédurale Désolé pour ce petit aparté psycho-personnel )

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 !)