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

Contenu supprimé Contenu ajouté
m Robot : Remplacement de texte automatisé (-(\n)A +\1À )
m Robot : Remplacement de texte automatisé (-[“”] *([^“”]*) *[“”] +« \1 »)
Ligne 48 :
Les ensembles finitaires sont d’abord des systèmes, ou ensembles, formels, c’est-à-dire des ensembles de formules, et ensuite d’autres ensembles que l’on peut construire progressivement en partant des systèmes formels. Ils peuvent être des ensembles d’ensembles formels, des ensembles d’ensembles d’ensembles formels…
 
Un ensemble est finitaire s’il peut être défini en un nombre fini d’étapes finitaires à partir des objets de base de la théorie. Une étape est finitaire si elle respecte une règle finitaire. Une définition du concept “finitaire”« finitaire » requiert donc une liste des règles finitaires. On exige de ces règles qu’elles ne permettent de construire que des ensembles bien définis.
Définir ou construire un ensemble c’est la même chose. Comme les prédicats, auxquels ils sont étroitement apparentés, un ensemble est construit par sa définition.
Ligne 71 :
Cette méthode du langage semi-naturel présente un grand avantage dans le cas présent, parce que 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.
 
Les prédicats fondamentaux de la théorie des ensembles sont “est« est élément de”de », ou “est« dans”est dans » et « = ». Mais on introduit dans Enum d’autres prédicats fondamentaux pour les constructions auxiliaires, les fonctions et les prédicats, principalement.
 
Les logiciens sont en général des minimalistes. On ne veut pas plus de principes qu’il n’est nécessaire. On veut un nombre minimal d’objets de base, d’opérateurs et de prédicats fondamentaux, d’axiomes et de règles de déduction. Un petit nombre est en général considéré comme suffisant.
Ligne 156 :
Les 15 opérateurs fondamentaux de Finitaire1 sont les 14 de Enum plus Non.
 
Les deux notions premières, ou prédicats fondamentaux, les plus importantes, de Finitaire1 sont “être« dans”être dans », ou “être« être élément de”de », et « = ». Les autres prédicats fondamentaux servent à définir les constructions auxiliaires.
 
Les 27 prédicats fondamentaux sont ceux de Enum plus “est« faux”est faux » et “est« est un prédicat sans variables liées”liées ».
 
=== Les axiomes de Finitaire1 ===
Ligne 178 :
 
==== Les axiomes d’existence des ensembles ====
Parmi les 27 prédicats fondamentaux de Finitaire1, tous sauf quatre (« = », “être« dans”être dans », “être« vrai”être vrai » et “être« être faux faux”») conduisent à des ensembles énumérables de vérités atomiques qui interviennent dans les raisonnements seulement pour justifier les constructions auxiliaires. Nous verrons qu’on peut s’en passer en les remplaçant par deux, ou même un, schéma d’axiomes, mais celui-ci requiert la compréhension de la notion de prédicat finitaire, qui doit être définie séparément. La plupart des règles de Enum et de la négation dans les prédicats finitaires servent justement à définir avec précision cette notion.
 
Les ensembles sont définis et remplis avec les règles de de production de Enum, les règles ou pseudo-règles associées à l’opérateur Non, et les trois formules initiales de Enum.