143 371
modifications
m (Lydie Noria a déplacé la page Fondements des mathématiques/Construction finitaire de l'ensemble des vérités vers Fondements des mathématiques/Construction finitaire de l’ensemble des vérités sans laisser de redirection : changement d...) |
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.
|