« Fondements des mathématiques/Construction finitaire de l’ensemble des vérités » : différence entre les versions
Contenu supprimé Contenu ajouté
m Fondements des mathématiques : la construction finitaire de l'ensemble des vérités déplacé vers Fondements des mathématiques/Des preuves de cohérence/Construction finitaire de l'ensemble des vérités: Tentative de réunification des feuill |
imported>Tavernierbot m Bot: Retouches cosmétiques |
||
Ligne 8 :
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.
Ligne 15 :
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.
Ligne 54 :
Pour que la suite soit plus compréhensible, nous introduisons les définitions suivantes :
rs =def so, r+ =def sso, r.
Si t erp u alors st erp a(rs)u
Ligne 76 :
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
Ligne 93 :
N =def Ensemble induit par Succ à partir de o
== La représentation des termes constants ==
La fonction d’addition erp Add
Ligne 108 :
Pour tout ensemble x de représentants de termes, Tprod(x) est l’ensemble des représentants obtenus à partir de ceux de x en appliquant une fois l’une des fonctions Succ, Add ou Mult.
Tprod =def Fonction Extension de (Il existe un Z’ tel que (Z Egale Im par Succ de Z’ Et Z’ Dans X)) Ou (Il existe un Z’ tel qu’Il existe un Z’’ tel que Z Egale Im par Add de CZ’Z’’ Et Z’ Dans X Et Z’’ Dans X) Ou (Il existe un Z’ tel qu’Il existe un Z’’ tel que Z Egale Im par Mult de CZ’Z’’ Et Z’ Dans X Et Z’’ Dans X)
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).
Ligne 125 :
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.
Ligne 148 :
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.
Ligne 173 :
PAF =def Ensemble somme de Ensemble induit par P-Prod à partir de PAF0
== La substitution des constantes aux occurences des variables libres ==
Pour définir la vérité des formules qui contiennent des quantificateurs on aura besoin de l’ensemble suivant.
Ligne 232 :
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
Ligne 243 :
tt-A-Prod =def Fonction Extension de (Il existe Z’, Z’’, Z’’’ tels que Z’ Dans Var Et Z’’ Dans X Et Z’’’ Dans PAF Et Z Dans PAF Et Z Egale assZ’Z’’’ Et CZ’’CoCZ’Z’’’ Dans Sub)
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.
Ligne 275 :
ex-F-Prod(X, X’, X’’) =def Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans X Et Z’’’ Dans PAF Et Z’’’’ Dans N Et Z Dans PAF Et Z Egale asZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub) Moins Ex-V-Prod(X, X’, X’’)
tt-F-Prod(X, X’, X’’) =def
tt-V-Prod(X, X’, X’’) =def Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans X Et Z’’’ Dans PAF Et Z’’’’ Dans N Et Z Dans PAF Et Z Egale assZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub) Moins tt-F-Prod(X, X’, X’’)
AVF-Prod =def Fonction C(A-Prod(X))C(Union(non-V-Prod(X, X’, X’’), et-V-Prod(X, X’, X’’), ou-V-Prod(X, X’, X’’), ex-V-Prod(X, X’, X’’), tt-V-Prod(X, X’, X’’) ))Union(non-F-Prod(X, X’, X’’), et-F-Prod(X, X’, X’’), ou-F-Prod(X, X’, X’’), ex-F-Prod(X, X’, X’’), tt-F-Prod(X, X’, X’’) )
AVF =def Ensemble induit par AVF-Prod à partir de C(AAF0)C(VAF0)(FAF0)
| |||