« Fondements des mathématiques/Cohérence des théories 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 10 :
L’axiome supplémentaire de Finitaire2 permet de définir des fonctions qui incluent une ou plusieurs inductions infinies dans leur définition. Cela permet de construire des ensembles par des inductions infinies sur des constructions par induction infinie. C’est exactement ce dont nous aurons besoin pour définir un modèle de Finitaire1.
 
Parmi les 27 prédicats fondamentaux de Finitaire1, tous sauf quatre, “est« dans”est dans », « = », “est« vrai”est vrai » et “est« est faux faux”» ne posent aucune difficulté. L’ensemble de toutes les vérités atomiques formulées avec ces 23 prédicats est énumérable. Il est engendré avec les règles de production de Enum et les règles supplémentaires de Finitaire1. Tous les axiomes de Finitaire1 qui traduisent ces règles sont évidemment vrais quand on prend cet ensemble de vérités atomiques comme modèle.
 
Les vérités atomiques formulées avec “est« vrai”est vrai » et “est« est faux faux”» peuvent toutes être obtenues à partir des vérités atomiques d’égalité et d’appartenance, par la même technique qui sert à construire l’ensemble des vérités à partir d’un modèle
 
Les égalités entre expressions formelles, qu’elle soient nommées directement ou par l’intermédiaire d’une fonction numérique, sont également toutes énumérables.