« Fondements des mathématiques/Construction finitaire de l’ensemble des vérités » : différence entre les versions

Aller à la navigation Aller à la recherche
m
Robot : Remplacement de texte automatisé (-\n(==={0,3})(?: *)([^\n=]+)(?: *)\1(?: *)\n +\n\1 \2 \1\n)
m (Robot : Remplacement de texte automatisé (-\n(==={0,3})(?: *)([^\n=]+)(?: *)\1(?: *)\n +\n\1 \2 \1\n))
}}
 
== La construction d’un ensemble de vérités ==
Pour prouver formellement qu’une théorie T est cohérente, il suffit de lui trouver un modèle. Autrement dit, il suffit de définir un ensemble M de formules atomiques et de prouver que tous les axiomes de T sont vrais si M est pris comme modèle.
 
Remarquons qu’en général T est inclus dans VM mais ne lui est pas égal, parce que T ne contient que les formules prouvables à partir des axiomes, et que pour toute théorie T suffisamment riche, il y a des formules vraies et non-prouvables.
 
== L’ensemble des vérités de l’arithmétique formelle ==
Au lieu d’une construction abstraite de VM à partir de M, nous allons construire VAF à partir de VAF0, l’ensemble des vérités de l’arithmétique formelle à partir de l’ensemble des vérités atomiques de l’aithmétique formelle. Mais cette construction a une valeur générale.
 
VAF0 = l’ensemble des vérités atomiques, par définition, puisque les formules de degré 0 sont atomiques.
 
== Le codage des formules ==
erp est une abréviation de est représenté par.
 
Si p erp P alors (pour tout x, p) erp a(rttx)P
 
== La représentation des nombres entiers ==
L’ensemble des nombres naturels erp N
 
N =def Ensemble induit par Succ à partir de o
 
== La représentation des termes constants ==
La fonction d’addition erp Add
 
Tconst =def Ensemble-somme de Ensemble induit par Tprod à partir de Singleton de o
 
== La représentation des assertions atomiques ==
Egal-const est l’ensemble des égalités arithmétiques entre termes constants (vraies ou fausses).
 
Inf-const =def Ensemble-image par Inf-Prod de (Tconst Pcart Tconst)
 
== La représentation des formules atomiques avec des variables libres ==
Var est l’ensemble des (représentants des) variables.
 
PAF0 =def Egal-var Union Inf-var
 
== La représentation des prédicats arithmétiques ==
L’ensemble des prédicats, c’est-à-dire les formules qui contiennent des variables libres, est défini par induction sur la complexité des formules.
 
PAF =def Ensemble somme de Ensemble induit par P-Prod à partir de PAF0
 
== La substitution des constantes aux occurrences des variables libres ==
Pour définir la vérité des formules qui contiennent des quantificateurs on aura besoin de l’ensemble suivant.
 
Sub-AF =def Extension de (CZCZ’CZ’’Z’’’ Dans Sub Et Z’’’ Dans PAF)
 
== La représentation des formules closes (vraies ou fausses) ==
AAF0 est l’ensemble des assertions de degré 0
 
A-Prod =def Fonction Union( Ensemble-image par non-P-Prod de X, Ensemble-image par et-P-Prod de (X Pcart X), Ensemble-image par ou-P-Prod de (X Pcart X), Im par ex-A-Prod de X, Im par tt-A-Prod de X ).
 
== La représentation des vérités ==
 
L’ensemble des vérités est défini par induction en même temps que l’ensemble des faussetés.
143 371

modifications

Menu de navigation