« Précis d'épistémologie/Les fondements des mathématiques » : différence entre les versions
Contenu supprimé Contenu ajouté
Aucun résumé des modifications |
→Une théorie des ensembles bien définis : compléments |
||
Ligne 176 :
Si ''f'' est une constructrice de première espèce à un argument, ''l'ensemble-image par f de'' est une constructrice de première espèce qui pour tout ensemble ''x'' construit ''l'ensemble de tous les y tels qu'il existe z dans x tel que y=f(z)''. ''L'ensemble infini par f de x'' est l'ensemble dont les éléments sont ''x, f(x), f(f(x)), f(f(f(x)))'' ... pour toutes les itérations finies de ''f''.
Une constructrice ''f'' peut
''L'ensemble-somme de x = y'' est défini par ''Pour tout z, z est élément de y si et seulement s'il existe w tel que (w est élément de x et z est élément de w)''.
''
Soit ''A(w, y<sub>1</sub> ... y<sub>n</sub>)'' une formule dont toutes les variables libres sont ''w, y<sub>1</sub> ... y<sub>n</sub>''. On suppose que les variables liées dans ''A(w, y<sub>1</sub> ... y<sub>n</sub>)'' sont toujours bornées par l'un des ''y<sub>1</sub> ... y<sub>n</sub>''. L'axiome de séparation affirme que ''Pour tous les y<sub>1</sub> ... y<sub>n</sub> et tout x, il existe z tel que pour tout w, w est élément de z si et seulement si w est élément de x et A(w, y<sub>1</sub> ... y<sub>n</sub>)''. Cela revient à affirmer l'existence d'une constructrice ''f'' à n+1 arguments définie par la relation ''f(x,y<sub>1</sub> ... y<sub>n</sub>)=z si et seulement si pour tout w, w est élément de z si et seulement si (w est élément de x et A(w, y<sub>1</sub> ... y<sub>n</sub>))''. Toutes les constructrices définies avec l'axiome de séparation sont donc définissables par des relations dans une théorie pure des ensembles.
''x est clos pour R'' (ou pour ''f'') veut dire ''pour tout y et tout z si y est élément de x et Ryz alors z est élément de x''▼
Une constructrice obtenue par composition de constructrices définissables dans la théorie est elle aussi définissable dans la théorie. Par exemple ''g(f(x))=y'' peut être défini par ''Il existe z tel que f(x)=z et g(z)=y''.
Soit ''f'' une constructrice de première espèce à un argument et ''R'' la relation qui la définit : ''Rxy si et seulement si f(x)=y''
''x est élément de y et y est clos pour R et pour tout z si x est élément de z et z est clos pour R alors y est inclus dans z'' ▼
''y est l'ensemble-image par f de x'' est défini par ''Pour tout z (z est élément de y si et seulement si il existe w tel que (w est élément de x et Rwz))''
▲''x est clos pour R'' (ou pour ''f'')
▲''y est l'ensemble infini par f de x'' est défini par ''x est élément de y et y est clos pour R et pour tout z si (x est élément de z et z est clos pour R) alors y est inclus dans z''
On en conclut que toutes les constructrices de première espèce de la présente théorie peuvent être définies par des relations dans une théorie pure des ensembles.
Pour fonder une théorie des ensembles bien définis, on retient tous les axiomes de Zermelo, sauf l'axiome de l'infini, et on leur ajoute deux schémas d'axiomes : l'axiome de remplacement et l'axiome de l'infini généralisé.
*'''L'axiome de remplacement''' : ''Si R est une relation
*'''L'axiome de l'infini généralisé''' : ''Si R est une relation
Toutes les constructrices de première espèce sont obtenues par composition finie des constructrices fondamentales : ''la paire de, l'ensemble-somme de, l'ensemble des parties de, l'ensemble infini par, l'ensemble-image par'' et toutes les constructrices définies avec l'axiome de séparation pourvu que tous les quantificateurs soient bornés dans la définition des ensembles.
| |||