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

Contenu supprimé Contenu ajouté
m Robot : Remplacement de texte automatisé (- d'être + d’être )
m Robot : Remplacement de texte automatisé (-\n(==={0,3})(?: *)([^\n=]+)(?: *)\1(?: *)\n +\n\1 \2 \1\n)
 
Ligne 12 :
Les mathématiques finitaires consistent à mettre en pratique un principe de progression ontologique, commencer par ce qui est simple, évident, élémentaire, pour poursuivre sur des bases solides.
 
== L’esprit des mathématiques finitaires : commencer par ce qui est simple et évident ==
 
L’ensemble des nombres entiers est le plus illustre de tous les ensembles finitaires. Il est à raison considéré comme la base de toute ontologie mathématique. Pour donner une idée de l’importance des nombres entiers, on peut rappeler ces propos, de Kronecker, que Dieu a créé les nombres entiers et qu’à partir de là les mathématiciens ont créé tout le reste de l’univers mathématique.
Ligne 42 :
Nous verrons que de telles évidences suffisent pour trouver presque tous les axiomes des théories des ensembles finitaires. Un nombre relativement petit d’axiomes évidents permet de prouver toutes les évidences intuitives, et à partir d’elles on peut prouver presque toutes les vérités mathématiques .Cela montre que la raison est capable de se connaître elle-même, au moins en partie, et qu’il n’est même pas très difficile de la dire puisqu’il suffit d’énoncer des évidences. Celles-ci sont simples, claires et acceptables pour tout être rationnel.
 
== Qu’est-ce qu’un ensemble finitaire ? ==
Le principe des principes des mathématiques finitaires, c’est de s’en tenir à des ensembles bien définis, c’est-à-dire qu’ils peuvent être déterminés complètement à l’intérieur d’une théorie.
 
Ligne 55 :
La liste des règles finitaires ne peut jamais être complète, pour les raisons suivantes. La règle d’après laquelle on peut construire à partir d’une liste L bien définie de règles finitaires et d’un ensemble E0 d’objets de base, l’ensemble U de tous les ensembles constructibles en un nombre fini d’étapes à partir des éléments de E0 et des règles de L, est une règle finitaire. Si L était la liste de toutes les règles finitaires, U serait l’ensemble de tous les ensembles finitaires et il serait lui-même finitaire. Il serait donc élément de lui-même. La règle d’après laquelle à partir de tout prédicat finitaire, on peut construire son extension conceptuelle, est aussi une règle finitaire, sachant qu’un prédicat est finitaire lorsque toutes ses variables, libres ou liées, sont restreintes à des ensembles finitaires déjà construits. On pourrait alors définir à partir de U l’ensemble BR de tous les ensembles finitaires qui ne sont pas éléments d’eux-mêmes. BR serait finitaire, il serait et ne serait pas élément de lui-même. Cette contradiction oblige à renoncer à l’hypothèse de l’existence d’une liste de toutes les règles finitaires. Une liste des règles finitaires est donc nécessairement incomplète même si elle est très élargie. L’ensemble de tous les ensembles finitaires s’il existe, est indicible.
 
== L’énumérabilité selon Smullyan ==
Le chapitre précédent a rappelé l’équivalence entre l’existence d’une machine universelle et l’énumérabilité de toutes les vérités atomiques d’appartenance aux ensembles énumérables. Cette section expose une autre définition de l’énumérabilité, issue des travaux de Post et Smullyan, qui repose sur la notion de règle de production.
 
[[Fondements des mathématiques : l'énumérabilité selon Smullyan|Texte de cette section]]
 
== Les vérités atomiques sur les ensembles énumérables ==
Les vérités atomiques sur les ensembles énumérables sont les vérités d’appartenance d’un élément à un ensemble énuméralbles et les égalités entre ensembles énumérables. Les secondes peuvent être définies à partir des premières avec l’axiome d’extensionalité et elles sont beaucoup moins élémentaires. On peut prouver qu’elles ne forment pas un ensemble énumérable
 
Ligne 91 :
La plupart des axiomes des théories des ensembles sont traduits dans Enum par quelques règles de production. Les axiomes de la somme, de l’infini, de compréhension et de remplacement en font partie. Certaines règles de production de Enum sont donc des versions élémentaires des axiomes ensemblistes. La cohérence et la vérité de Enum prouvent qu’il est possible de donner une formalisation fiable de la théorie des ensembles. Mais Enum est trop élémentaire pour aller loin en mathématiques.
 
== Formules initiales et règles de production pour les vérités atomiques d’appartenance aux ensembles énumérables ==
Cette section définit une théorie complète des ensembles énumérables, au sens où elle contient toutes les vérités atomiques d’appartenance à tous les ensembles énumérables. La preuve de sa complétude est donnée dans la section suivante.
 
[[Fondements des mathématiques:Formules initiales et règles de production pour les vérités atomiques d’appartenance aux ensembles énumérables|Texte de cette section]]
 
== Les théorèmes fondamentaux de l’énumérabilité et de l’indécidabilité ==
Le premier de ces théorèmes montre en quel sens l’ensemble de tous les ensembles énumérables est complètement connu. On pourrait l’appeler le théorème de complétude de l’énumérabilité. Il est équivalent à la preuve d’existence d’une machine universelle, donnée par Turing en 1936, qui est à l’origine de l’invention des ordinateurs.
 
Ligne 103 :
[[Fondements des mathématiques:Théorèmes fondamentaux de l’énumérabilité et de l’indécidabilité|Texte de cette section]]
 
== 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.
 
Ligne 119 :
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 qu'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.
 
Ligne 140 :
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 élémentaire 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.
 
Ligne 159 :
Les 27 prédicats fondamentaux sont ceux de Enum plus « est 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 ensemble.
 
Ligne 176 :
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 Finitaire1, tous sauf quatre (« = », « être dans », « être vrai » et « être 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.
 
Ligne 187 :
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 Finitaire1.
 
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 de la logique du premier ordre.
 
=== Autres formulations des axiomes de Finitaire1 ===
== L’incomplétude des théories finitaires ==
==L’élargissement ontologique==