« Axiomes des théories des ensembles/Les ensembles finitaires » : différence entre les versions
Contenu supprimé Contenu ajouté
Création |
Compléments |
||
Ligne 155 :
==Les négations des faussetés atomiques et le principe d’induction complète==
Les prédicats à partir desquels les ensembles de Enum sont définis ne contiennent pas la négation. Cela permet à Enum d’être une théorie complète, au sens où elle peut prouver toutes ses vérités, mais ce n’est pas suffisant pour une théorie générale des ensembles finitaires parce qu’on veut pouvoir y définir des ensembles à partir de prédicats qui contiennent des négations.
Pour remplir les ensembles définis avec la négation dans leurs prédicats, il faut pouvoir prouver des négations de faussetés atomiques. Explicitons le processus de production de ces négations.
===Quelques négations de faussetés atomiques de base===
Quelques formules sont évidemment des négations de faussetés atomiques.
Les premières d’entre elles nient l’égalité entre des objets de base différents, s’il y a au moins deux objets de base. Avec les trois objets de base o , X , Z , on obtient trois négations de faussetés atomiques initiales, non(o=X) , non(o=Z), non(X=Z)
Quelques règles de production pour les non-équations, ou négations d’équations, suffisent pour engendrer toutes les non-équations vraies entre expressions formelles, parce que par définition, deux expressions formelles ne sont égales que si elles sont toutes les deux des combinaisons des mêmes objets de base, avec les mêmes opérateurs appliqués dans le même ordre.
A partir des non-équations vraies on peut engendrer des non-appartenances vraies. Par exemple on a la règle suivante, si non(x=y) alors non(x est dans Singleton de y).
De telles non-appartenances vraies sont les négations de faussetés atomiques les plus élémentaires pour une théorie des ensembles parce qu’on peut les produire sans faire usage du principe d’induction complète. Celui-ci est le principe finitaire le plus important. Il nous donne la capacité de prouver presque tout ce qu’on veut prouver sur les ensembles infinis, pourvu qu’ils soient finitaires. On peut l’énoncer de la façon suivante.
===Le schéma d’axiomes du principe d’induction complète===
Soit E un ensemble défini par induction à partir d’un élément initial i et d’une fonction génératrice g. Cela veut dire que E contient i et toutes ses images, g(i), g(g(i)), g(g(g(i))), ...obtenues par un nombre fini d’applications de g . E est l’ensemble induit par g à partir de i.
Soit P(x, y1,...,yn) un prédicat d’une théorie des ensembles finitaires, avec n+1 variables libres. La formule suivante est un axiome.
Pour tous y1,...,yn, tout i et toute fonction g
si P(i, y1,...,yn)
et si pour tout x si P(x, y1,...,yn) alors P(g(x), y1,...,yn)
alors pour tout x, si x est dans Ensemble induit par g à partir de i alors P(x, y1,...,yn)
Cet axiome peut servir à prouver la négation d’une fausseté atomique. Si on sait déjà que P(c, y1,...,yn) est faux, on peut déduire que c n’est pas dans E.
Tel qu’il a été explicité, c’est un schéma d’axiomes qui montre comment formuler un nombre infini d’axiomes en remplaçant P(x, y1,...,yn) par les prédicats d’une théorie.
On peut considérer le principe d’induction complète comme une définition de la notion d’ensemble induit, au sens où il fixe la signification de cette notion.
Les vérités atomiques, ou singulières, de l’arithmétique élémentaire, peuvent toutes être connues, ainsi que les négations des faussetés atomiques, sans faire usage de la puissance déductive de la logique du premier ordre. Des règles de production suffisent, parce que l’ensemble des vérités singulières est décidable. On l’apprend tout simplement en apprenant à compter, à faire des additions et des multiplications. En revanche la connaissance des vérités atomiques ensemblistes ne peut pas se passer des lois générales et de la logique du premier ordre. Des raisonnements fondés sur des lois générales permettent parfois de prouver des vérités singulières.
==La négation dans les prédicats finitaires==
Cette section montre comment élargir l’ontologie de Enum pour introduire la négation dans les prédicats finitaires. Elle expose aussi des règles, et des pseudo-règles, de production pour les négations des faussetés atomiques.
[[Fondements des mathématiques : La négation dans les prédicats finitaires|Texte de cette section]]
==Les axiomes d’une théorie élémentaire des ensembles finitaires==
Cette section expose les axiomes de Finitaire1, qui est une théorie élementaire des ensembles finitaires. Finitaire1 est ainsi nommée parce qu’elle peut servir de base pour développer des théories plus puissantes.
===L’ontologie de Finitaire1===
L’ontologie de Finitaire1, c’est à dire l’ensemble de tous les êtres nommés dans la théorie, contient principalement des expressions formelles et des ensembles. Les autres êtres, les fonctions les prédicats, les X-termes, les Z-termes, sont des objets auxiliaires qui servent à construire des ensembles. Finitaire1 emprunte donc à Enum son ontologie en la complétant avec les négation dans les prédicats.
Les trois objets de base de Finitaire1 sont ceux de Enum, o, X et Z.
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”, ou “être élément de”, et “être égal à”. Les autres prédicats fondamentaux servent à définir les constructions auxiliaires.
Les 27 prédicats fondamentaux sont ceux de Enum plus “est prouvablement faux” et “est un prédicat sans variables liées”.
===Les axiomes de Finitaire1===
Les axiomes sont des formules de la logique du premier ordre, définies avec les objets de base, les opérateurs et les prédicats fondamentaux. Nous verrons plus loin comment le nombre d’opérateurs et de prédicats fondamentaux de Finitaire1 peut être réduit sans modifier véritablement la théorie.
====L’axiome d’extensionalité====
L’axiome d’extensionalité est un axiome nécessaire pour toutes les théories des ensembles. Il dit que deux ensembles sont égaux s’ils ont les mêmes éléments. Si un être n’obéit pas à cet axiome alors il ne peut pas être un ensembleSous la forme suivante, c’est un axiome de Finitaire1.
Pour tout x et tout y, si (x et y sont des ensembles et si pour tout z, (z est dans x équivaut à z est dans y) ) alors x = y
L’inclusion entre ensembles est définie de la façon suivante.
x est inclus dans y =def (x et y sont des ensembles et pour tout z, si z est dans x alors z est dans y)
On peut alors énoncer l’axiome d’extensionalité d’une façon plus brève.
Pour tout x et tout y, si (x est inclus dans y et y est inclus dans x) alors x=y
====Les axiomes d’existence des ensembles====
Parmi les 27 prédicats fondamentaux de Finitaire2, tous sauf quatre (“=”, “être dans”, “être prouvable” et “être prouvablement 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.
Toutes les règles de production de Enum ainsi que les pseudo-règles associées à l’opérateur Non, peuvent être traduites par des formules closes du calcul des prédicats. Il suffit de les compléter avec des quantificateurs universels pour toutes leurs variables libres. Par exemple, la règle Eform2 est traduite par la formule suivante.
Pour tout x, si x est une expression formelle alors sx est une expression formelle
Il s’agit bien d’une loi générale.
====Le principe d’induction complète====
Le schéma d'axiomes du principe d'induction complète a déjà été énoncé. Tous les axiomes, en nombre infini, obtenus à partir de ce schéma sont des axiomes de Finitiare1.
La théorie Finitaire1 est l’ensemble de tous les axiomes qui viennent d'être cités et de toutes les formules que l’on peut déduire par les règles de déduction du calcul des prédicats.
===Autres formulations des axiomes de Finitaire1===
==L’incomplétude des théories finitaires==
==L’élargissement ontologique==
| |||