Explications complementaires a propos du defi de Médiat

[syborgg]

Salut,
ceux et celles qui ont suivit la discussion du "defi" de Mediat auront compris que la classe des groupes monogenes n'est pas axiomatizable dans la logique du premier ordre. La raison invoquee ici est que Z est le seul groupe infini qui appartient a la classe, et qu'une theorie du premier ordre (disons dans un langage fini pour simplifier les choses) qui contient un modele infini contient egalement des modeles en toute cardinalite infinie. C'est un resultat assez surprenant a premiere vue.

Je vais essayer de faire comprendre aux non logiciens pourquoi il en est ainsi. Je suppose juste connu dans un premier temps le theorme de compacite du calcul des predicats (si un chaque partie finie d'un ensemble de formules du premier ordre admet un modele, alors l'ensemble de formules lui meme admet un modele).

Partons donc d'une theorie du premier ordre T dans le langage L qui admet un modele infini M (peu importe sa cardinalite). Une premiere approche consiste a se rendre
compte que pour tout cardinal infini k, aussi grand soit il, T admet un modele de cardinal superieur ou egal a k.

L'astuce ici est caracteristique de ce qui se fait en theorie des modeles, et revient souvent avec des variantes selon les contextes : on introduit un ensemble de symboles de constantes (disjoint de l'ensemble des symboles utilises pour le langage inicial) c_i, indexee par i dans k. Et on considere la theorie T_0 (dans le langage L augmente des nouveaux symboles) suivante :

T_0 = T + "c_i different de c_j, pour tout i,j dans k" (excusez moi pour cette facon horrible d'ecrire, mais je suis ce matin sur un ordi portable et je ne sais pas ou sont les touches qui me permettraient d'ecrire en Tex)

Il est alors evident de voir que toute partie finie de T_0 admet un modele (M en l'occurence), et donc le theoreme de compacite nous dit que T_0 admet un modele : ce modele est en particulier un modele de T, et comme on interprete dedans les constantes c_i comme etant deux a deux distinctes, il est forcement de cardinal au moins k.

Mais on peut faire encore mieux : on peut montrer que T a un modele de cardinalite exactement k, en invoquant le fameux theoreme de Lowenhein et Skolem (qui date de 1920, donc fort ancien).
Mediat, je te laisse la main si tu veux bien (je dois m'en aller en week end et ma famille est sur les starting blocks en train de pietiner a m'attendre...)
-----

[albanxiii]

Bonjour,

Pour référence, je redonne le lien du défi de Médiat : https://forums.futura-sciences.com/m...etit-defi.html

[Médiat]

Bonjour,

Pour donner un petit exemple parlant : une théorie (dans le sens du premier ordre) des groupes finis, aurait (si elle existait) des modèles infinis

[syborgg]

Une question legitime qu'un non logicien peut se poser apres avoir compris que la classe des groupes monogene n'est pas axiomatizable au premier ordre, c'est de se demander si il existe au contraire des classes de structures bien connues qui sont axiomatizables. La reponse est oui : corps algebriquement clos, corps separablement clos, corps K qui ont la prorpriete que toute variete irreductible definie sur K possede un point K-rationnel (appellés corps pseudo algebriquement clos, classe qui contient les corps algebriquement clos), diverses classes de corps values (Henseliens etc..), groupes divisibles, groupes sans torsion, etc....

[A voir en vidéo sur Futura]

[Médiat]

groupes sans torsion

Exemple très, très intéressant, dans la mesure où la classe des groupes de torsion n'est pas axiomatisable au premier ordre.

Je laisse les lecteurs réfléchir à l'axiomatisation des groupes sans torsion, cela permettra de voir certains points (dont un sur les théories finiment axiomatisables)


PS je rajoute à la liste de sybborg la classe (particulièrement simple) des ordres totaux denses sans extremums

[syborgg]

Ah tiens au fait, on peut se rendre compte assez facilement que l'argument invoque pour la non axiomatizabilite des groupes monogenes ne fonctionne pas pour la classe des groupes de torsion : il existe des groupes de torsion en toute cardinalite infinie.
Cependant, cette classe n'est pas axiomatizable : il faut en chercher la raison ailleurs....

[invite23cdddab]

 Cliquez pour afficher

Pour les groupes sans torsion, je suppose qu'il faut une infinité (dénombrable) d'axiomes (ou un schéma), du type



etc.

Pareil pour les corps algébriquement clos :



etc.

[syborgg]

 Cliquez pour afficher

Pour les groupes sans torsion, je suppose qu'il faut une infinité (dénombrable) d'axiomes (ou un schéma), du type



etc.

Pareil pour les corps algébriquement clos :



etc.

Exact (sauf que la premiere, par exemple, s'ecrit plutot , et idem pour les autres).
La question se pose alors : existe t il des axiomatisations finies de ces theories ?
La logique sait repondre a cette question.

[syborgg]

Une premiere approche facile pour voir cela : les groupes sans torsion peuvent ils s'axiomatiser avec un nombre fini d'axiomes parmi ceux proposes par Tryss2 ?

[azizovsky]

De manière récursive? (ou définition par récurrence)

j'essaye de comparer la logique du 1ère et 2ème ordre ......pour comprendre Médiat .

[Médiat]

Pour les groupes sans torsion, je suppose qu'il faut une infinité (dénombrable) d'axiomes (ou un schéma), du type



etc.

J'ai enlevé le spoiler qi n'a plus de raison d'être, j'ajouterais que l'on a ici un schéma d'axiomes que je pourrais écrire :

pour tout entier non nul :

ou encore mieux : pour tout entier non nul :

On pourrait me reprocher d'utiliser IN dans mon axiomatisation, mais ce n'est pas le cas (indice : le "pour tout " est en dehors de la formule, ce n'est qu'une façon "naïve" de lister les axiomes qui ne contiennent pas de , le plus important à comprendre, dans tous les cas d'axiomatisation infinie, c'est qu'une démonstration est un processus fini qui ne va donc utiliser qu'un nombre fini d'occurrences du schéma ; un bon exemple est Peano, personne n'a jamais écrit tous les axiomes, mais chaque fois que l'on en a besoin, il est trivial d'écrire l'axiome dont on a besoin (c'est ce que font les élèves de lycée)

[azizovsky]

Qu'est ce qu'on peut dire de :

[Médiat]

Mieux vaudrait



D'une façon générale quand on écrit des axiomes, on est dans la partie syntaxique, il n'est donc pas utile de préciser l'appartenance (pas besoin de ZF) sinon, oui c'est bien un schéma d'axiomes légitime

[azizovsky]

un vrai prof, Merci .

ps: plus de 6h de recherche pour comprendre un petit peu ....

[Médiat]

les groupes sans torsion peuvent ils s'axiomatiser avec un nombre fini d'axiomes parmi ceux proposes par Tryss2 ?

En écrivant cela syborgg tient compte du théorème (bien sympa) auquel je faisais allusion au message #5

[azizovsky]

En écrivant cela syborgg tient compte du théorème (bien sympa) auquel je faisais allusion au message #5

je pense à

finiment axiomatisables

[Médiat]

Oui, et au théorème qui dit qu'une théorie est finiment axiomatisable ssi on peut extraire une axiomatisation finie de toutes axiomatisations (et donc de celle proposée par Tryss2)

[azizovsky]

Merci médiat, j'ai appris beaucoup aujourd'hui ....

[syborgg]

Bon donc resumons : un resultat dit qu'une qu'une théorie est finiment axiomatisable ssi on peut extraire une axiomatisation finie de toutes axiomatisations (et donc de celle proposée par Tryss2). Ce resultat (pas evident a priori quand on y reflechit) est une consequence directe du theoreme de compacite.

Mais pour terminer encore faudrait il verifier qu'aucune partie finie des axiomes de Tryss2 n'axiomatise les groupes sans torsion : voyez vous pourquoi ?

[azizovsky]

Mais pour terminer encore faudrait il verifier qu'aucune partie finie des axiomes de Tryss2 n'axiomatise les groupes sans torsion : voyez vous pourquoi ?

D'une façon non formelle, si pour un certain fini, il existe un tel que avec , est d'ordre fini, donc le groupe est un groupe de torsion ce qui contredit ce qu'on veut comme modèle des axiomes .

[syborgg]

D'une façon non formelle, si pour un certain fini, il existe un tel que avec , est d'ordre fini, donc le groupe est un groupe de torsion ce qui contredit ce qu'on veut comme modèle des axiomes .

Ce qu'on veut verifier, c'est qu'aucune partie finie du schema d'axiomes de Tryss2 n'axiomatize les groupes sans torsion. En d'autres termes, pour une telle partie finie S (qu'on peut clairement supposer etre constituee des axiomes T_1, ...T_n dans la terminologie de Tryss2 ci dessus), il existe un groupe qui verifie S mais qui n'est pas sans torsion. Vois tu lequel ?

[azizovsky]

C'est le groupe des classes résiduelles modulo n:

[syborgg]

C'est le groupe des classes résiduelles modulo n:

L'idee est bien celle la, mais en prenant plutot un Z/pZ avec p premier plus grand que n, pour etre sur que les n premiers axiomes soient bien verifies.

[azizovsky]

L'idee est bien celle la, mais en prenant plutot un Z/pZ avec p premier plus grand que n, pour etre sur que les n premiers axiomes soient bien verifies.

Oui,je vois..., Merci, ce qui est étonnant c'est le mot compacité, il est partout... comme tu l'a remarqué dans une ancienne discussion....

Je doit m'arrêter quand des détails m'échappe ....(un petit repos)

[Médiat]

Salut,

Toujours avec la compacité, on peut facilement montrer que l'existence d'un élément plus grand que tous les entiers n'est pas incompatible avec AP (Arithmétique de Peano)

[syborgg]

Oui,je vois..., Merci, ce qui est étonnant c'est le mot compacité, il est partout... comme tu l'a remarqué dans une ancienne discussion....

Je doit m'arrêter quand des détails m'échappe ....(un petit repos)

Sans ce fameux theoreme de compacite, la logique du premier ordre n'aurait aucun interet. C'est une pierre angulaire. Le terme compacite dans ce contexte vient du fait que parmi les nombreuses preuves de ce theoreme, une utilise la compacite au sens topologique. Mais on peut egalement justifier l'utilisation du terme "compacite" en remarquant (c'est trivial) qu'une formulation equivalente est que "de tout ensemble de formule non consistent (i.e. qui n'admet aucun modele) ont peut extraire une partie finie non consistente". Cela ressemble a la definition de la compacite topologique.

[syborgg]

D'ailleurs au passage : en utilisant cette formulation equivalente du theoreme de compacite, ont peut prouver facilement le chainon manquant de la preuve du fait que la theorie des groupes sans torsion n'est pas finiment axiomatizable (c'est a dire que si une theorie est finiment axiomatizable, alors on peut l'axiomatiser en utilisant une partie finie d'une axiomatisation donnee a l'avance). Voyez vous pourquoi ?

[Médiat]

Salut,

Toujours avec la compacité, on peut facilement montrer que l'existence d'un élément plus grand que tous les entiers n'est pas incompatible avec AP (Arithmétique de Peano)

J'aurais pu prendre un exemple encore plus frappant : l'existence d'un élément divisible par tous les entiers n'est pas incompatible avec AP

[azizovsky]

Bonjour, désolé, j'ai un engouement pour plusieurs sujets en même temps , le dernier c'est logique (je m'accroche cette fois..) , je vais essayé de répondre d'après ce que j'ai compris:

Déjà dans la formulation des axiomes des groupes sans torsion par Médiat, il y'avait quelque chose qui m'interpellais, pourquoi insistait vous sur le n qui est à l'extérieur , j'ai pensé qu'on peu aximatiser avec ça , mais le n'est pas encore définit, j'ai pensé au transfinis , càd , d'après ce qui j'ai compris de l'AP (même axiomatisation du 1 er ordre) , là je suis largué car dans les formules le n 'est pas encore défini ...

Pour la compacité, on'a déjà extraire (avec torsion) pour une partie finie d' axiomatisation des groupes sans torsion, donc l'axiomatisation avec une partie fini donne un autre modèle, mon raisonnement n'est pas ''compacte'' ?

[azizovsky]

le 'est pas encore défini ...

dans l'axiomatisation de l'AP car d'après ce que j'ai compris de l'insistance de Médiat sur ..., il doit être absent dan l'AP car avec cette axiomatisation qu'il va être défini .