« 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
Bot: Retouches cosmétiques
imported>Tavernierbot
m (Bot: Retouches cosmétiques)
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.
 
Pour que la suite soit plus compréhensible, nous introduisons les définitions suivantes :
 
rs =def so, r+ =def sso, r. =def ssso, r= =def sssso, r< =def ssssso, rnon =def sssssso, ret =def ssssssso, rou =def sssssssso, rx =def ssssssssso, rexx =def sssssssssso, rttx = def ssssssssssso
 
Si t erp u alors st erp a(rs)u
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
 
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).
 
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 occurences 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
 
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.
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 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)
 
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)
Utilisateur anonyme

Menu de navigation