« Fondements des mathématiques/Cohérence des théories finitaires » : différence entre les versions

AÀ partir de Vat(n) il est aisé de produire Vat1(n+1), l’ensemble de toutes les vérités atomiques sur les éléments de O1(n+1) pour les raisons suivantes. Comme la complexité d’un X-terme est arbitrairement grande, les images d’un élément de O(n) par une fonction itérée un nombre de fois aussi grand que l’on veut sont toujours dans O(n). On peut donc produire à partir de Vat(n) toutes les vérités atomiques d’appartenance à (Ensemble induit par f à partir de x) pour n’importe quel x dans O(n) et n’importe quel f qui satisfait aux conditions citées en (ii). On peut alors définir l’ensemble de toutes les égalités entre ces ensembles induits et avec les éléments de O(n) et finalement toutes les égalités entre les listes finies d’éléments de O1(n+1).