Différences entre les versions de « Précis d'épistémologie/Les fondements des mathématiques »

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 toujours être traduitedéfinie par une relation fonctionnelle : ''f(x)=y'' ou ''f(x,y)=z'' ou ...
 
ToutesMontrons que toutes les constructrices de première espèce de la présente théorie peuvent être traduitesdéfinies par des relations fonctionnelles dans une théorie pure des ensembles.
 
Soit ''f{x,y}=z'' uneest constructricedéfini depar première espèce à un argument et ''R''Pour latout relationw, fonctionnellew quiest laélément traduitde : ''Rxyz si et seulement si f(w=x) ou w=y)''.
 
''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)''.
''y est l'ensemble-image par f de x'' est défini par :
 
''pourL'ensemble des parties de x = y'' est défini par ''Pour tout z, (z est élément de y si et seulement si il existe w tel que (wz est élémentinclus dedans x et Rwz))''.
 
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''.
''y est l'ensemble infini par f de x'' est défini par :
 
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'') veutest diredéfini par ''pourPour tout y et tout z si y est élément de x et Ryz alors z est élément de x''
 
''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 fonctionnelle qui traduitdéfinit une constructrice de première espèce f à un argument alors pour tout x il existe y tel que ypour tout z (z est l'ensemble-imageélément parde fy si et seulement si il existe w tel que (w est élément de x et Rwz))''
*'''L'axiome de l'infini généralisé''' : ''Si R est une relation fonctionnelle qui traduitdéfinit une constructrice de première espèce f à un argument alors pour tout x il existe y tel que (x est élément de y et y est l'ensembleclos infinipour parR fet depour tout z si (x est élément de z et z est clos pour R) alors y est inclus dans z)''
 
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.
4 741

modifications