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

Comme toutes les définitions de Finitaire1 sont prédicatives, nous pourrons montrer que les éléments d’un ensemble de O(n) sont toujours ou bien des expressions formelles ou bien des ensembles de O(n). On voit ici l’importance des définitions prédicatives dans la définition de notre ontologie progressive. Elles permettent d’associer à la progression ontologique un ordre dans la production des vérités.

 

 

Vat(n) est l’ensemble des vérités atomiques de degré n (appartenances et égalités) associées à O(n).

Vat(n+1, i, j+1) peut être construit à partir de Vat(n+1, i, j) et Fat(n+1, i, j). La même technique qui sert à définir l’ensemble des vérités à partir d’un modèle sert ici à remplir tous les ensembles définis avec des prédicats de complexité formelle j+1. Les égalités entre ces ensembles et avec les ensembles précédemment définis sont alors déterminées par l’axiome d’extensionalité.

 

 

Vat(n+1) =def Somme des Vat(n+1, i, j) pour i et j entiers positif

Vat est définie avec une induction infinie par la fonction qui produit Vat(n+1) à partir de Vat(n). Mais cette fonction requiert elle-même une induction infinie dans sa définition. Cela montre le rôle de l’axiome supplémentaire de Finitaire2 pour cette construction du modèle Vat de Finitaire1.

 

 

==Remarques générales sur la cohérence des théories finitaires==