La théorie ZF est-elle consistante ?

[invitebdf515f4]

Bonjour,

J'ai cherché cela sur Google, sans succès: La théorie ZF est-elle consistante ?

Beaucoup d'articles parlent de ce sujet, soit pour définir ZF, définir la notion de consistance, etc
Il y a aussi beaucoup d'affirmation du genre, "Si ZF est consistante, alors ...", "PA est consistante au sein de ZF" (consistance relative), etc.

Mais, je n'ai pas encore trouvé de réponse à cette question qui me semble fondamentale "ZF est-elle consistante ?".
Je ne parle pas de consistance relative à une autre théorie (genre "Si XX est consistante, alors ZF l'est aussi"), mais de consistance "absolue".

Mon intuition après quelques recherche est qu'on ne sait pas si ZF est consistante. Me trompe-je ?
-----

[Médiat]

Mon intuition après quelques recherche est qu'on ne sait pas si ZF est consistante. Me trompe-je ?

Parfaitement exact, on ne connaît que des résultats de co-consistance et le théorème d'incomplétude de Gödel nous dit que l'on ne pourra pas faire mieux.

Par contre on sait que ZF - axiome de l'infini est consistante, on en connaît même un modèle.

[invite97d79020]

Je confirme ce qu'a dit Médiat à propos des résultats de co-consistance de ZF.

[Tiky]

Je précise que je ne suis pas à l'aise avec ces notions. Toutefois je me pose la question suivante.

Si on parvenait à construire une théorie T' qui contient ZF et telle que T' est consistante et ZF est consistante relativement à T', alors ZF serait consistante ?
Bien sûr il faut que T' ne vérifie pas toutes les hypothèses du second théorème de Godel, et comme elle serait consistante et capable d'axiomatiser l'arithmétique (puisqu'elle contient ZF), elle devrait ne pas être récursivement axiomatisable ?

J'ai lu sur Wikipédia, que si une théorie est récursivement aximatisable, alors on peut déterminer si une démonstration est valide ou non ? Le risque serait alors que le ne puisse pas déterminer si la preuve de la consistance de ZF dans T' est valide et cela
même si on la possède ?

[A voir en vidéo sur Futura]

[Médiat]

Si on parvenait à construire une théorie T' qui contient ZF et telle que T' est consistante et ZF est consistante relativement à T', alors ZF serait consistante ?
Bien sûr il faut que T' ne vérifie pas toutes les hypothèses du second théorème de Godel, et comme elle serait consistante et capable d'axiomatiser l'arithmétique (puisqu'elle contient ZF), elle devrait ne pas être récursivement axiomatisable ?

Oui

J'ai lu sur Wikipédia, que si une théorie est récursivement aximatisable, alors on peut déterminer si une démonstration est valide ou non ? Le risque serait alors que le ne puisse pas déterminer si la preuve de la consistance de ZF dans T' est valide et cela
même si on la possède ?

C'est même pire que cela, car même une théorie récursivement axiomatisable n'est pas obligatoirement décidable (vérifier qu'une démonstration est valide n'est pas le même problème que trouver une démonstration).

[Tiky]

Pourtant il est écrit ceci sur Wikipédia :

dans une théorie récursivement axiomatisable, "être une preuve" est décidable.

Peut-être qu'ils entendent par "être une preuve" le fait que le texte soit correctement formulé dans la théorie mais pas qu'il soit vrai ?

[Médiat]

Si dans Peano je vous donne une formule en vous affirmant que c'est une preuve de la conjecture de Goldbach, vous allez pouvoir le vérifier, car c'est décidable.
Si je vous demande de m'exhiber une démonstration de la conjecture de Goldbach, cela va être plus dur, car AP n'est pas décidable.

[Tiky]

Si j'ai bien compris, une théorie T est décidable si on peut répondre toujours par oui ou non à la question : "l'énoncé A dans T est démontrable" ? Donc on pourrait trouver la théorie T' en question dans mon premier message, mais on serait
incapable de dire si l'énoncé "ZF est consistant dans T'" est démontrable dans T'.

[Médiat]

Très exactement, s'il existe un algorithme capable de répondre à cette question par oui ou par non en un temps fini.

[Tiky]

Oui, je ne connaissais pas la décidabilité algorithmique, d'où mon incompréhension. Merci bien pour vos réponses.