Énumérer les théories axiomatiques

reuns
reuns
dans Fondements et Logique
[small]Contexte : en gros les seules choses que j'arrive à comprendre en logique c'est quand j'arrive à transformer les concepts impliqués en terme de machines de Turing et du problème de l'arrêt. On suppose donc que le langage et les théorèmes d'une théorie axiomatique doivent être énumérables, par un algorithme.[/small]

Est-il possible de définir le concept de "théorie axiomatique" de telle manière qu'on puisse énumérer toutes les théories axiomatiques ? Je sais énumérer les grammaires de tous les langages, mais une théorie axiomatique c'est un peu plus que ça.
Car le but est de voir ce que ça génère comme structure, par exemple est-ce qu'on peut définir "$T$ prouve que $T_2$ est consistante" ou encore "$T$ formalise $T_2$" et "$T$ formalise l'arithmétique" ?

Réponses

  • Maxtimax
    Maxtimax
    Si tu te fixes disons un langage dénombrable et un codage pour les formules dans ce langage, alors comme il y a une fonction récursive "universelle", tu peux "énumérer les fonctions récursives", et comme, via le codage susmentionné,chaque théorie peut être vue comme une fonction récursive, tu peux en quelque sorte énumérer les théories récursives.

    Mais ça n'a pas un grand rapport avec ce dont tu parles après : puisque $T$ et $T_2$ sont fixées, il ne s'agit que d'énumérer les théorèmes de $T_2$ disons pour parler de la cohérence de $T_2$ (dans une théorie $T$ contenant par exemple PA); quant à la "formalisation de $T_2$ dans $T$", je pense qu'on appelle ça l'interprétabilité en général, et que ça n'a rien à voir avec la récursivité
  • reuns
    reuns
    Je n'ai pas compris ce que tu veux me dire. Je sais énumérer les langages, ou les fonctions récursives, pas de problème.

    Je sais aussi énumérer les théorèmes de $T$ pour voir si celle-ci prouve $P \land \lnot P$, si on trouve un tel $P$ alors ça prouve que $T$ est inconsistante.

    Mais pour prouver que $T$ est consistante, il faut prouver (donc dans une autre théorie $T_2$) que ce programme qui énumère ses théorèmes de $T$ en cherchant une contradiction, ne s'arrête pas.

    Ensuite le but c'est d'énumérer les théories $T$, et à chacune, de demander si elle formalise l'arithmétique, ou si elle prouve que chacune des autres est consistante ou non. Et ça je ne sais pas le faire.
  • Maxtimax
    Maxtimax
    Eh bien si tu sais énumérer les fonctions récursives tu sais énumérer les théories :-S (ce qui était quand même ta question en gras)
    Ensuite pour prouver $T_2 \vdash Cons(T)$ il faut énumérer les théorèmes de $T_2$, avec le risque de ne jamais t'arrêter.
    Ce que tu appelles "demander à chacune" c'est à la suite les unes des autres ?
  • samok
    samok
    Toute chose égale par ailleurs, sauf erreur et cordialement :

    tu connais les poursuites entre points sieur reuns : genre au départ 3 fusées puis elles se courent après.

    Bon ben là tu peux émuler l'infini en un temps fini, mais bon c'est théorique, dans un monde platonicien tout ça tout ça.

    J'ai la flemme de formaliser tout ça, ah ah ah.

    (bonjour Albertine et fluorhydrique)
    S
  • Shah d'Ock
    Shah d'Ock
    Ça dépend quand même de ce que tu appelles "théorie axiomathique". Tu auras du mal à énumérer l'ensemble des théories défini comme suit:
    On fixe une énumération $(\phi_n)$ des formules d'un langage du premier ordre.
    $T_x$ est la théorie dont les axiomes sont toutes les formules $\phi_n$ telles que la $n$-ème décimale en base $2$ de $x$ est $1$.
    Et ce, pour tout $x \in \mathbb R$.
  • samok
    samok
    la nième décimale en base 2 ?

    Appelons un bit un bit sieur Shah !

    S
  • Shah d'Ock
    Shah d'Ock
    Oui, je sais, mais je n'aime pas les bits. Et vous sieur Samok, que pensez-vous de commander une glace aux bits?
  • christophe c
    christophe c
    Bonjour reuns, je ne comprends pas non plus vraiment ton problème, mais j'ai l'impression que tu te compliques la vie et surtout, il y a, à plusieurs reprises un passage qui n'a pas de sens mathématique dans ce que tu dis, qui est le suivant:
    et à chacune, de demander si elle formalise (?) l'arithmétique

    Le mot "formaliser" n'a pas de sens mathématique (il est synonyme de "mathématiser" si tu préfères, c'est à dire que les maths traitent de quelque chose qui a DEJA été mathématisé avant)

    Si on ne se soucie de choses pratiques, on peut faire les choses très simplement avec des entiers naturels (je t'ajoute une couche pour démystifier les choses):

    une théorie T est un ensemble d'énoncés appelés alors "axiomes de T"
    une évidence de T est une conjonction d'axiomes de T
    un théorème de T est un énoncé P tel qu'il existe E qui soit une évidence de T et telle que E=>P est un axiome de T

    Bien entendu, on utilise "leur description" pour parler des ensembles d'énoncés (qui sont des ensembles d'entiers). Mais, tu dis le savoir, il existe une relation récursivement énumérable $R$ incluse dans $\N^2$ telle que pour toute partie récursivement énumérable $A$ de $\N$, il existe $a\in \N$ tel que $A=\{x\in \N \mid (a,x)\in R\}$. On dit souvent que $R$ est "universelle" quand elle a cette propriété. On peut tout coder en utilisant juste $R$ (et quelques bricoles).

    Si j'interprète ce qui semble être ton appel, étant donnée une théorie T (récursive) j'ai envie de dire que tu te demandes au nom de quelle objectivité on prétend que tel énoncé X "mérite de s'appeler" l'énoncé cons(T)? Est-ce bien ça qui te gêne?
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • reuns
    reuns
    J'aurais aimé que quelqu'un propose un algorithme qui énumère plein de théories axiomatiques $T_i$ et un autre qui définit "$T_i$ prouve que $Cons(T_j)$ ou $\lnot Cons(T_j)$", mais bon puisque vous dites que ma question n'est pas claire, je vais écrire un peu de blabla :

    Enumérer les fonctions récursivement énumérables, ou écrire la relation universelle $R$ de CC, c'est trivial pour un informaticien comme moi, qui maîtrise parfaitement les notions de "langage Turing universel qui en interprète un autre", donc aucun problème pour encoder une fonction récursive dans un entier et écrire un algorithme qui la décode.

    Pour moi $Cons(T)$ c'est deux choses en même temps : c'est d'une part la question "est-ce que le programme qui énumère les théorèmes de $T$ et cherche une contradiction, s'arrête". Si ce programme s'arrête, alors le fait qu'il s'arrête, donc $\lnot Cons(T)$, est une vérité absolue, qui ne dépend d'aucune axiomatisation et ne peut être remis en question.
    Par contre si ce programme ne s'arrête pas, il faut bien essayer de le démontrer, dans une certaine théorie axiomatique $T_2$, qui peut-être n'est pas consistante. Donc ce que dit $T_2$ de $Cons(T)$ ne peut pas être considéré comme une vérité absolue.

    D'où l'idée d'énumérer "les théories axiomatiques" $T_i$, et de demander à chacune ce qu'elle dit de $Cons(T)$
    (demander à $T_i$ ça veut dire évidemment énumérer les théorèmes de $T_i$ pour voir s'ils démontrent $Cons(T)$ ou $\lnot Cons(T)$. cette énumération peut très bien ne jamais s'arrêter)

    Aucun problème pour lancer plein d'énumérations en même temps : on peut énumérer des théories axiomatiques $T_i$, et pour chacune, énumérer ses théorèmes, ça ne pose aucun problème (l'ordonnanceur qui simule une machine de Turing non-déterministe sur une seule machine de Turing déterministe, c'est le cœur d'un OS comme windows ou linux)

    Pourquoi c'est intéressant ? Parce que savoir écrire des algorithmes qui énumèrent, c'est savoir définir précisément. Si on sait faire tout ça, alors on sait définir et parler des théories axiomatiques et de leur consistance en général, ce qui est intéressant.
  • Shah d'Ock
    Shah d'Ock
    reuns a écrit:
    Si on sait faire tout ça, alors on sait définir et parler des théories axiomatiques et de leur consistance en général, ce qui est intéressant.
    Tu as déjà entendu parler des travaux d'un certain Kurt Gödel?
  • Shah d'Ock
    Shah d'Ock
    Par ailleurs si $T_1$ est une théorie qui ne décide pas $Cons(T)$ alors $T_1+Cons(T)$ et $T_1+\neg Cons(T)$ sont deux théories cohérentes... On est bien avancé!
  • Shah d'Ock
    Shah d'Ock
    reuns a écrit:
    Enumérer les fonctions récursivement énumérables, ou écrire la relation universelle $R$ de CC, c'est trivial pour un informaticien comme moi, qui maîtrise parfaitement les notions de "langage Turing universel qui en interprète un autre", donc aucun problème pour encoder une fonction récursive dans un entier et écrire un algorithme qui la décode.
    Ben dans ce cas répondre à ta question devrait être trivial aussi. Tu fixes une bonne fois pour toutes un langage du premier ordre et une énumération récursive $(\phi_k)$ de ses formules, tu écris la relation universelle $R$, et pour chaque $n$ tu considère la théorie dont les axiomes sont donnés par les $\phi_k$ tels que $(n,k) \in R$.
  • reuns
    reuns
    Oui je suis assez d'accord avec ça, pour se fixer un langage (décidable) $L$ qui contient $\lnot$, et ensuite d'énumérer les algorithmes qui énumèrent des mots/formules du langage.

    Mais ensuite on veut parler de la cohérence de ces théories $T_n$ et de "est-ce que $T_n$ démontre $Cons(T_i)$".

    Est-ce que ça veut dire qu'on doit aussi se fixer une façon unique de décrire et de parler d'une fonction récursive (ou d'une machine de Turing) dans le langage $L$ ?

    (Par exemple dans PA, pour parler de "telle machine de Turing $M$ s'arrête", j'encode la suite des états de $M$ dans une suite d'entiers $u_n$ que je décris dans une formule $F$ du langage de PA, ce qui me permet de regarder la formule $F, \exists n, u_n = 0$")

    Et dans ce cas, à quoi pourrait correspondre "$T_n$ formalise $T_i$", ie. tous les théorèmes de $T_i$ sont aussi des théorèmes de $T_n$ ?
  • Shah d'Ock
    Shah d'Ock
    Je pense que le plus simple c'est de procéder comme suit:
    On fixe un langage $L$, on lui ajoute les symboles de l'arithmétique de Péano, et on énumère les théories dont les axiomes contiennent au moins ceux de Péano.
    De la sorte, on a une définition uniforme de $Cons(T)$ qui est celle de $PA$, et on n'a pas à se demander si pour chaque système d'axiomes la théories obtenue $T_n$ est suffisament expressive (ce qui est probablement indécidable, quoique je n'ai pas trouvé de preuve en moins de trois minutes), ni, le cas échéant, comment se traduit $PA$ - et donc $Cons$ - dans $T_n$ (ce qui dépend bien évidemment des axiomes choisis. Ainsi, par exemple, sur le langage $\{\in\}$, si l'on considère les axiomes de $ZF$ dans lesquels on remplace systématiquement $x \in y$ ($x$ et $y$ étant des variables de variables) par $y \in x$, alors il faut faire les remplacement en conséquences dans la traduction de $PA$ dans $ZF$. Dans le cas général, trouver le bonne traduction est probablement beaucoup moins trivial).
  • christophe c
    christophe c
    De mon téléphone : tu as enfin, à ton dernier post, précisé ce que tu appelles "X formalise Y". Mais du coup faut que je relises tout pour trouver quelle est ta question.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Bon j'ai répondu à mon premier post. C'est un énoncé de la forme "pour toute preuve p de conclusion c dont les axiomes sont dans X il existe une preuve q de même conclusion c dont les axiomes sont dans Y"

    Mais je ne vois pas trop pourquoi ça te posait problème. Et oui si tu veux parler de TOUTES les théories c'est quand même plus confortable de fixer définitivement un langage plutôt que jouer au yoyo. Mais celui de Peano est maladroit il n'a servi historiquement que pour permettre à Gödel de taper fort donc de faire "calcul école primaire" mais il n'y a pas de raison de ne pas mettre "en dur" les listes (finies) dans le langage (plutôt qu'utiliser le théorème chinois).
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Et trouve une autre tournure que X formalise Y :-D.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Shah d'Ock
    Shah d'Ock
    Oui enfin ceci dit je ne suis pas sûr que la proposition de reuns corresponde à ce qu'il a en tête: avec cette définition, ZF ne formalise pas PA (puisqu'elles n'ont pas le même vacabulaire: les énoncés de PA ne sont même pas des énoncés de ZF).
    Je pense qu'il s'agirait plutôt d'un truc du genre "tout modèle de $T_1$ contient un modèle définissable de $T_2$".
    Ou alors tout symbole du vocabulaire de $T_2$ peut être remplacé par une formule de $T_1$ de sorte à ce que que la traduction axiomes de $T_2$ soit des théorèmes de $T_1$.
    Si je ne dis pas de bêtise les deux notions sont équivalentes.
  • reuns
    reuns
    Merci beaucoup, je crois que je n'avais pas envisagé de fixer autant de choses dès le départ.
    Mais parler d'un certain langage défini d'avance sur lequel on a des théories de la forme $T_i = PA+S_i$ dans lesquelles on peut utiliser $PA$ comme sémantique commune, ça a l'avantage de tout définir précisément, avant d'essayer de comprendre ce que signifierait partir de quelque de chose de plus général.

    Oui je crois que c'est ta seconde formulation Shah D'Ock que j'avais en tête de $ZF$ formalise $PA$,
    Parce que je me représentais une théorie plutôt comme un algorithme qui étant donné un ensemble fini de formules, te donne un ensemble fini un peu plus grand de formules obtenues en appliquant les axiomes,
    donc un algorithme de parcours en largeur de l'arbre des théorèmes.
    Sauf que cet algorithme doit (plus ou moins) s'arrêter pour toute entrée, problème car énumérer les algorithmes qui s'arrêtent pour toutes les entrées, on ne sait pas faire (le plus ou moins c'est que le problème se pose quand on essaye de parler de réécriture des phrases d'un langage dans un autre).
  • Shah d'Ock
    Shah d'Ock
    Euh attention: l'ensemble des théorèmes déductibles dun ensemble fini d'axiomes n'est pas fini...
    Et on n'applique pas les axiomes, mais des règles de déductions.
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 1

Alexique