« Axiomes des théories des ensembles/Les ensembles finitaires » : différence entre les versions

Cette méthode du langage semi-naturel présente un grand avantage dans le cas présent, parce que qu'Enum est défini avec un grand nombre d’opérateurs et de prédicats fondamentaux. Pour faire une théorie purement formelle, il faudrait un glossaire assez volumineux pour donner aux symboles formels leur signification dans une langue naturelle.

En tant que théorie Enum est évidemment cohérente. Puisqu’elle ne contient pas de négations, elle ne peut pas contenir de contradictions. Puisqu’elle est un ensemble de formules atomiques, on peut la considérer comme un modèle d’elle-même. Mais cela ne suffit pas pour prouver que qu'Enum est vraie en tant que théorie des ensembles. Si ses formules initiales ou ses règles étaient mal choisies, elle ne cesserait pas d’être cohérente, mais ses formules ne pourraient plus être interprétées comme des vérités sur les ensembles. Comment être sûr que ses formules initiales et ses règles ont été bien choisies ? Comment le prouver ?

Dès qu’on a compris ces notions, la vérité des formules initiales de Enum est évidente. Il en va de même pour la vérité des règles de production. Il suffit de s’assurer que dans tous les cas, si les prémisses sont vraies, la conclusion l’est aussi. Cela suffit pour prouver que qu'Enum est valide, qu’elle ne contient que des vérités. La section suivante prouvera qu’il y a un sens à dire qu’elle est complète, qu’elle contient toutes les règles, en nombre fini, dont on a besoin pour dire des vérités sur les ensembles infinis.

Soit E un ensemble défini par induction à partir d’un élément initial i et d’une fonction génératrice g. Cela veut dire que qu'E contient i et toutes ses images, g(i), g(g(i)), g(g(g(i)))…obtenues par un nombre fini d’applications de g . E est l’ensemble induit par g à partir de i.