« Fondements des mathématiques/Des preuves de cohérence » : différence entre les versions
Contenu supprimé Contenu ajouté
m Bot : Remplacement de texte automatisé (-\b([Cc][’'])est +[àa] +dire\b +\1est-à-dire) |
m Bot : Remplacement de texte automatisé (-\b(d|D)(é|e|è)j(a|à)\b +\1éjà) |
||
Ligne 81 :
Nous donnerons d’abord une preuve naturelle de la cohérence de l’arithmétique formelle AF. L’ontologie de l’arithmétique formelle n’est pas adaptée à la formalisation de cette preuve, mais celle de Finitaire1 oui.
Nous montrerons que la théorie Finitaire1 permet de formaliser la preuve naturelle de la cohérence de l’arithmétique formelle. L’ontologie de Finitaire1 est limitée mais elle est cependant très riche. Elle permet de définir beaucoup plus d’ensembles que l’arithmétique formelle, qui est
On donnera ensuite une preuve de la cohérence de Finitaire1 et on complétera son ontologie pour définir une théorie Finitaire2 qui permet de formaliser la preuve de la cohérence de Finitaire1.
Ligne 89 :
La méthode qui vient d’être exposée rencontre l’objection suivante. On prouve la cohérence d’une théorie T avec une théorie T+ plus compliquée que T. Il se pourrait que T soit incohérente, que T+ le soit également et qu’elle permette quand même de prouver que T est cohérente. Ces preuves de cohérence ne prouveraient donc rien du tout.
Cette objection n’est ici pas valable. Avant de définir Finitaire1, on sait
Comme on sait que Finitaire1 et d’autres théories finitaires élargies sont cohérentes, on peut s’en servir pour prouver la cohérence d’autres théories. Nous prouverons que les méthodes finitaires sont en un sens toujours suffisantes, au sens où si une théorie est cohérente alors elle a un modèle finitaire. C’est une conséquence, ou plus exactement une reformulation, du théorème de complétude de Gödel. Mais on ne peut pas déduire de ce théorème l’existence d’une théorie finitaire complète, au sens où elle suffirait pour toutes les preuves de cohérence.
| |||