Pythagore: un théoréme ?

[Médiat]

Bonjour
En tout état de cause, un métaxiome, cela n'existe pas dans le langage courant de la logique, et un théorème qui ne se démontre pas n'est pas un théorème, mais un axiome (si on le considère comme "vrai"), et un axiome qui se démontre n'est pas un axiome mais un théorème !

Ne pas respecter la terminologie usuelle est une faute.

De plus j'ai du mal à comprendre l'intérêt d'une telle hiérarchie, puisqu'elle dépend du choix des axiomes, du choix des théorèmes, voir de l'ordre dans lequel on démontre ces théorèmes, la seule chose qui soit "canonique"* (et qui est un travail courant en mathématique) est de donner, pour chaque théorème d'une théorie, les axiomes utiles à sa démonstration ; les exemples les plus usuels, sont les théorèmes de ZF avec ou sans axiome du Choix, avec ou sans axiome de Fondation, avec ou sans hypothèse du continu (éventuellement généralisée) on peut d'ailleurs noter qu'il est rare (si jamais cela existe) de préciser si tel théorème utilise ou non l'axiome de la paire (et il y a une bonne raison pour cela).

(*) Et encore.
-----

[taladris]

Bonjour
En tout état de cause, un métaxiome, cela n'existe pas dans le langage courant de la logique, et un théorème qui ne se démontre pas n'est pas un théorème, mais un axiome (si on le considère comme "vrai"), et un axiome qui se démontre n'est pas un axiome mais un théorème !

Juste pour clarifier la terminologie en logique que je ne maitrise pas bien: un systeme d'axiomes engendrant une theorie est-il necessairement minimal, au sens ou aucun axiome n'est une consequence des autres? A partir d'un systeme non contradictoire de propositions, je peux etudier la theorie engendree par ce systeme, c'est-a-dire toutes les propositions que l'on peut deduire de ce systeme par un nombre fini d'operations logiques. Existe-t-il un nom pour le systeme initial de propositions?

Par exemple, si je veux etudier le theoreme des valeurs intermediaires (TVI), qui est un theoreme de ZF, je peux me contenter des axiomes de ZF. Mais, si je veux lister tous les theoremes de ZF qui permettent de prouver le TVI, cela devient un travail gigantesque et plus tres instructif. Par soucis pratique, j'aurais envie de lister la proposition "R est l'unique (a isomorphisme pres) corps totalement ordonne archimedien et verifiant l'axiome de la borne superieure" (un theoreme de ZF) comme proposition de mon systeme generateur initial. C'est ce que Mateo_13 appelle un "metaxiome", meme si je trouve la terminologie problematique. Existe-t-il un nom pour designer cela?

Cordialement

[Médiat]

Bonjour,

un systeme d'axiomes engendrant une theorie est-il necessairement minimal, au sens ou aucun axiome n'est une consequence des autres?

Non, un système d'axiomes se doit d'être générateur, on ne lui demande pas d'être libre ou minimal, d'ailleurs cette dernière notion est difficile à définir, puisque toute théorie finiment axiomatisable peut s'axiomatiser avec un seul axiome !

S'intéresser à l'indépendance des axiomes peut, par contre, être intéressant ; cf. les résultats de Gödel et Cohen concernant AC et HC. Cela peut éviter d'étudier des théories contradictoires.

A partir d'un systeme non contradictoire de propositions, je peux etudier la theorie engendree par ce systeme, c'est-a-dire toutes les propositions que l'on peut deduire de ce systeme par un nombre fini d'operations logiques. Existe-t-il un nom pour le systeme initial de propositions?

Oui : une axiomatique, ou système d'axiomes

Par exemple, si je veux etudier le theoreme des valeurs intermediaires (TVI), qui est un theoreme de ZF, je peux me contenter des axiomes de ZF. Mais, si je veux lister tous les theoremes de ZF qui permettent de prouver le TVI, cela devient un travail gigantesque et plus tres instructif. Par soucis pratique, j'aurais envie de lister la proposition "R est l'unique (a isomorphisme pres) corps totalement ordonne archimedien et verifiant l'axiome de la borne superieure" (un theoreme de ZF) comme proposition de mon systeme generateur initial. C'est ce que Mateo_13 appelle un "metaxiome", meme si je trouve la terminologie problematique. Existe-t-il un nom pour designer cela?

Oui : c'est un théorème ; ce qui n'a aucun impact sur ce que l'ont peut en déduire (ZF seul ou ZF + "n'importe quel théorème de ZF" ont les mêmes théorèmes).


Cordialement

[PlaneteF]

Bonjour,

(...) un systeme d'axiomes engendrant une theorie (...=

(...) la theorie engendree (...)

Juste une remarque de terminologie :

Une théorie n'est pas en soi "engendrée" par un système d'axiomes, elle est le système d'axiomes lui-même. Revenons à la définition même d'une théorie : "On appelle théorie un ensemble de formules closes, appelés aussi axiomes."

Ainsi par exemple généralement quand on parle de la théorie des groupes on ne parle pas de l'ensemble des théorèmes "générés" à partir des axiomes de la théorie, en prenant par exemple les axiomes d'associativité (assoc), d'élément neutre (en) et d'élément symétrique (sym), mais de l'ensemble de ces 3 axiomes. On a ainsi :


Cordialement

[Médiat]

Bonjour PlaneteF,

Je ne suis pas forcément d'accord, certains auteurs utilisent comme définition d'une théorie que c'est un ensemble de formules clos par inférence, et c'est la définition qui me semble la meilleure, puisqu'elle ne fait pas dépendre une théorie d'une de ses axiomatiques particulières.

[PlaneteF]

(...) certains auteurs utilisent comme définition d'une théorie que c'est un ensemble de formules clos par inférence (...)

Bonjour Médiat,

De mon côté, jusqu'à maintenant il ne me semble pas avoir rencontré cette définition, et avant d'écrire mon précédent message j'avais fait une vérif. sur 3 cours différents. Maintenant il y a tellement de cours et d'écrits dispos (et on ne va pas s'en plaindre), ... et c'est un domaine tellement vaste (et on ne va pas s'en plaindre non plus)

Maintenant quand on manipule par exemple la notion de modèle, on parle bien de modèle d'une théorie qui pour le coup est définie uniquement par ses axiomes. Si l'on reprend l'exemple de , et si l'on veut savoir si une interprétation définie sur le langage des groupes est un modèle de , on va regarder uniquement si satisfait (assoc), (en) et (sym). Dans ce cas on considère bien que .

Maintenant il y a peut-être d'autres cas de figure où l'on utilise une définition plus large de la notion de théorie ?!


Cordialement

[Médiat]

De mon côté, jusqu'à maintenant il ne me semble pas avoir rencontré cette définition, et avant d'écrire mon précédent message j'avais fait une vérif. sur 3 cours différents. Maintenant il y a tellement de cours et d'écrits dispos (et on ne va pas s'en plaindre), ... et c'est un domaine tellement vaste (et on ne va pas s'en plaindre non plus)

De mon côté j'ai plutôt vu le contraire (surtout pendant mes études, mais c'est il y a très longtemps) .

Ce qui me gène avec la définition qui a votre préférence, c'est que deux systèmes d'axiomes différents correspondent à deux théorie différentes, alors qu'elle ont peut-être les mêmes théorèmes alors qu'avec la définition que je préfère, les théories sont égales si et seulement si elles ont les mêmes théorèmes.

Maintenant quand on manipule par exemple la notion de modèle, on parle bien de modèle d'une théorie qui pour le coup est définie uniquement par ses axiomes.

Je ne suis pas convaincu par cet argument, puisqu'un modèle d'une théorie vérifie bien tous les théorèmes de cette théorie (quelque soit la définition choisie), par contre je suis d'accord qu'il n'est nécessaire de "démontrer" que telle structure est un modèle des axiomes d'une théorie pour qu'elle soit modèle de tous ses théorèmes.

Cordialement

[PlaneteF]

Ce qui me gène avec la définition qui a votre préférence, c'est que deux systèmes d'axiomes différents correspondent à deux théorie différentes, alors qu'elle ont peut-être les mêmes théorèmes alors qu'avec la définition que je préfère, les théories sont égales si et seulement si elles ont les mêmes théorèmes.

Je ne suis pas convaincu par cet argument, puisqu'un modèle d'une théorie vérifie bien tous les théorèmes de cette théorie (quelque soit la définition choisie), (...)

Pour le coup je n'ai pas forcément de préférence particulière, je constate comme souvent qu'il y a des différences de terminologie d'une source à l'autre. Ainsi si je rencontre le cas je ne verrai pas de sujet à ce que l'on différencie système d'axiomes et théorie, ... Et puis le fait que d'un cours à l'autre la terminologie ne soit pas forcément exactement la même, bah cela veut dire que l'on a la très grande chance de pouvoir accéder à différentes ressources (souvent très nombreuses) pour être capable de le constater !!!

Maintenant le point sur lequel tout le monde convergera, est que quelle que soit la définition que l'on donne à une théorie, pour savoir si une interprétation est un modèle d'une théorie il serait "ballot" de se palucher la vérification de la totalité des théorèmes


Cdt

[minushabens]

A ce propos je me pose la question suivante : quand on développe une théorie, on commence par poser certains axiomes, puis on en déduit des théorèmes, puis on démontre d'autres théorèmes en s'appuyant sur les premiers, donc sans faire référence explicitement aux axiomes, ou du moins pas tous. Bref on construit peu à peu un graphe avec des chaînes qui partens des axiomes vers des théorèmes de plus en plus éloignés. Mais la notion de "théorème qu'on démontre à partir d'un théorème obtenu précédemment" si elle est claire dans la pratique des mathématiciens, ne me semble pas bien fondée : il peut y avoir plusieurs chemins possibles pour démontrer un théorème. Est-ce que ce genre de choses a été étudié et formalisé?