« Fondements des mathématiques/Preuve naturelle de la cohérence de l'arithmétique formelle » : différence entre les versions

m
Bot : Remplacement de texte automatisé (-\b([Cc][’'])est +[àa] +dire\b +\1est-à-dire)
m (cat)
m (Bot : Remplacement de texte automatisé (-\b([Cc][’'])est +[àa] +dire\b +\1est-à-dire))
Les éléments de VAF0 sont toutes les formules que l’on peut déduire de 0=0 en appliquant un nombre fini de fois les règles précédentes.
 
Pour obtenir les axiomes de AF, on peut commencer par traduire les règles de production en formules généralisées, c’est -à -dire qu’elles commencent par un opérateur de généralisation, et closes, c’est -à -dire sans variables libres.
 
Par exemple, la première règle est traduite par la formule suivante.
alors pour tout nombre x, P est vraie de x
 
Les propriétés P des nombres peuvent être identifiées aux prédicats de AF, c’est -à -dire aux formules arithmétiques qui contiennent des variables libres. Ces prédicats peuvent être considérés comme les ensembles de l’arithmétique formelle. (il existe un y tel que x=2.y) est par exemple un nom pour l’ensemble des nombres pairs.
 
On ne peut pas traduire le principe d’induction complète par une seule formule de l’arithmétique formelle parce que l’univers arithmétique est réduit aux nombres. Quand on dit, pour tout x, dans l’arithmétique formelle, cela veut dire, pour tout nombre x. On ne peut donc pas dire, pour toute propriété P des nombres. Pour résoudre ce problème, il faut alors traduire le principe d’induction complète par un schéma d’axiomes, un cadre formel qui détermine un nombre infini de formules qui sont toutes adoptées comme axiomes. Il y a autant d’axiomes d’induction complète qu’il y a de prédicats arithmétiques.
143 371

modifications