Fondements des mathématiques/Des preuves de cohérence/Construction finitaire de l'ensemble des vérités

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.

Pour atteindre ce but, on peut définir l’ensemble VM de toutes les formules vraies pour M et essayer alors de prouver que tous les axiomes de T sont dans VM.

La construction de VM à partir de M est finitaire. On en déduit que si un modèle est finitaire alors l’ensemble de toutes les formules vraies pour ce modèle est lui aussi finitaire. Nous verrons plus loin (Paradoxes des mathématiques finitaires) que ce théorème est compatible avec le théorème d’incomplétude de Tarski et le théorème de complétude de Gödel.

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’arithmétique formelle. Mais cette construction a une valeur générale.

VAF va être défini par induction sur la complexité des formules. VAF est la réunion de tous les VAFn, pour n entier positif. VAFn est l’ensemble des vérités de degré n. Le degré n d’une formule est le nombre maximal d’opérateurs logiques emboités qu’elle contient. Deux opérateurs logiques sont emboités dans une formule, si l’un est contenu dans une sous-formule sur laquelle porte l’autre. Par exemple, dans (p ou q) et non r , “ou” est emboité dans le “et” mais pas dans le “non”.

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.

0 erp o

s erp so

+ erp sso

. erp ssso (3)

= erp sssso (4)

< erp ssssso (5)

Pour définir VAF, il faut représenter les opérateurs logiques

non erp sssssso (6)

et erp ssssssso (7)

ou erp sssssssso (8)

x erp ssssssssso (9)

(il existe un x tel que) erp sssssssssso (10)

(pour tout x) erp ssssssssssso (11)

x’ erp ssssssssssso (12)

(il existe un x’ tel que) erp ssssssssssssso (13)

(pour tout x’) erp sssssssssssssso (14)

et ainsi de suite pour les autres variables, x’’, x’’’, ...

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 t erp u et v erp w alors t+v erp a(r+)buw

Si t erp u et v erp w alors t.v erp a(r.)buw

Si t erp u et v erp w alors t=v erp a(r=)buw

Si t erp u et v erp w alors t<v erp a(r<)buw

Si p erp P alors (non p) erp a(rnon)P

Si p erp P et q erp Q alors (p et q) erp a(ret)bPQ

Si p erp P et q erp Q alors (p ou q) erp a(rou)bPQ

Si p erp P alors (il existe un x tel que p) erp a(rexx)P

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

0 erp o

1 erp a(so)o

2 erp a(so)(a(so)o)

...

La fonction de succession erp Succ

Succ =def Fonction a(so)X

N =def Ensemble induit par Succ à partir de o

La représentation des termes constants

La fonction d’addition erp Add

Add =def Fonction a(sso)bXX’

La fonction de multiplication erp Mult

Mult =def Fonction a(ssso)bXX’

L’ensemble des termes constants erp Tconst

De même que dans la preuve du théorème fondamental de l’énumérabilité, on définit Tconst à partir de Singleton de o et de la fonction Tprod.

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).

Egal-Prod =def Fonction a(r=)bXX’

Egal-const =def Ensemble-image par Egal-Prod de (Tconst Pcart Tconst)

Inf-const est l’ensemble des infériorités arithmétiques entre termes constants (vraies ou fausses).

Inf-Prod =def Fonction a(r<)bXX’

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.

S3 =def Fonction sssX

Var =def Ensemble induit par S3 à partir de rx

Tvar est l’ensemble des termes variables.

Tvar =def Ensemble-somme de Ensemble induit par Tprod à partir de (N Union Var)

Egal-var est l’ensemble des égalités arithmétiques entre termes variables (vraies, fausses et variables).

Egal-var =def Ensemble-image par Egal-Prod de (Tvar Pcart Tvar)

Inf-var est l’ensemble des infériorités arithmétiques entre termes variables (vraies, fausses et variables).

Inf-var =def Ensemble-image par Inf-Prod de (Tvar Pcart Tvar)

PAF0 est l’ensemble des prédicats de degré 0

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(n) est l’ensemble des prédicats de degré n

PAF(n+1) = P-Prod(PAF(n))

La fonction P-Prod est définie à partir des suivantes

non-P-Prod =def Fonction a(rnon)X

et-P-Prod =def Fonction a(ret)bXX’

ou-P-Prod =def Fonction a(rou)bXX’

Exist =def Ensemble induit par Singleton de S3 à partir de Singleton de rexx

Tout =def Ensemble induit par Singleton de S3 à partir de Singleton de rttx

P-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), Ensemble-image par Fonction aXX’ de (Exist Pcart X), Ensemble-image par Fonction aXX’ de (Tout Pcart X)).

PAF est l’ensemble des prédicats de l’arithmétique formelle.

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 est l’ensemble des quadruplets (q, n, y, p) où p est dans PAF, y est dans Var, n est dans N et q est obtenu par la substitution de n à toutes les occurences de y dans p.

Sub-AF est obtenu par l’intermédiaire de Sub, qui est défini par les règles suivantes.

S1 Si x est dans Var et n est dans N alors (n,n,x,x) est dans Sub

S2 Si x et y sont dans Var et x≠y et n est dans N alors (x,n,y,x) est dans Sub

S3 Si n et m sont dans N et x est dans Var alors (n,m,x,n) est dans Sub

S4 Si (q,n,y,p) et (w,n,y,v) sont dans Sub alors (bqw,n,y,bpv) est dans Sub

S5 Si (q,n,y,p) est dans Sub alors (asoq,n,y,asop) est dans Sub

S6 Si (q,n,y,p) est dans Sub alors (assoq,n,y,assop) est dans Sub

S7, S8, jusqu’à S12 correspondent de même à la préfixation de assso, asssso jusqu’à asssssssso.

S13 Si (q,n,y,p) est dans Sub et x est dans Var et x≠y alors (asxq,n,y,asxp) est dans Sub

S14 Si (q,n,y,p) est dans Sub et x est dans Var et x≠y alors (assxq,n,y,assxp) est dans Sub

S15 Si p est dans PAF et x est dans Var alors (asxp,n,x,asxp) est dans Sub

S16 Si p est dans PAF et x est dans Var alors (assxp,n,x,assxp) est dans Sub

On définit Sub par induction à partir des ensembles et des fonctions suivantes.

SubS1 =def Ensemble-image par Fonction CXCXCX’X’ de (N Pcart Var)

SubS2 =def Ensemble-image par Fonction CX’CXCX’’X’ de (N Pcart VarDif)

où VarDif =def Extension de (Z Dans Var Et Z’ Dans Var Et Non(Z Egale Z’))

SubS3 =def Ensemble-image par Fonction CXCX’CX’’X de (N Pcart(N Pcart Var))

ProdS4 =def Fonction (Ensemble-image par (Fonction CbXX’’’’CX’CX’’CbX’’’X’’’’’) de (Ensemble-image par Fonction Extension de (CZCZ’CZ’’Z’’’ Dans X et CZ’’’’CZ’CZ’’Z’’’’’ Dans X) de X))

ProdS5 =def Fonction Ensemble-image par Fonction CasoXCX’CX’’asoX’’’ de X

On définit de même ProdS6 jusqu’à ProdS12.

ProdS13 =def Fonction Ensemble-image par Fonction CasX’’’’XCX’CX’’asX’’’’X’’’ de Extension de (CZCZ’CZ’’Z’’’ Dans X Et Z’’’’ Dans Var Et Non(Z’’’’ Egale Z’’))

ProdS14 =def Fonction Ensemble-image par Fonction CassX’’’’XCX’CX’’assX’’’’X’’’ de Extension de (CZCZ’CZ’’Z’’’ Dans X Et Z’’’’ Dans Var Et Non(Z’’’’ Egale Z’’))

SubS15 =def Ensemble-image par Fonction CasXX’CX’’CXasXX’ de (Var Pcart(PAF Pcart N))

SubS16 =def Ensemble-image par Fonction CassXX’CX’’CXassXX’ de (Var Pcart(PAF Pcart N))

ProdS =def Fonction Union(Im par ProdS4 de X, Im par ProdS5 de X, ..., Im par ProdS14 de X)

Sub =def Ensemble-somme de Ensemble induit par ProdS à partir de Union(SubS1, SubS2, SubS3, SubS15, SubS16)

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

AAF0 =def Egal-const Union Inf-const

AAF(n+1) = A-Prod(AAFn) est l’ensemble des assertions de degré n+1. C’est l’ensemble des formules closes qui contiennent n opérateurs logiques emboités. Une formule est close si toutes ses variables sont liées.

ex-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 asZ’Z’’’ Et CZ’’CoCZ’Z’’’ Dans Sub)

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.

FAF0 est l’ensemble des faussetés atomiques.

FAF0 =def AAF0 Moins VAF0

AVF est l’ensemble des triplets CxCyz où x est AAFn, y est VAFn et z est FAFn.

AVFn= C(AAFn)C(VAFn)(FAFn)

AVF(n+1) = AVF-Prod(AVFn)

non-V-Prod(X, X’, X’’) =def Ensemble-image par non-P-Prod de X’’

non-F-Prod(X, X’, X’’) =def Ensemble-image par non-P-Prod de X’

et-V-Prod(X, X’, X’’) =def Ensemble-image par et-P-Prod de X’ Pcart X’

et-F-Prod(X, X’, X’’) =def (Ensemble-image par et-P-Prod de X Pcart X’’) Union (Ensemble-image par et-P-Prod de X’’ Pcart X)

ou-V-Prod(X, X’, X’’) =def (Ensemble-image par ou-P-Prod de X’ Pcart X) Union (Ensemble-image par ou-P-Prod de X Pcart X’)

ou-F-Prod(X, X’, X’’) =def Ensemble-image par ou-P-Prod de X’’ Pcart X’’

ex-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 asZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub)

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)

VAF =def Ensemble-somme de Extension de (Il existe Z’, Z’’ tels que CZ’CZZ’’ Dans AVF)

Cela termine cette construction de VAF à partir de VAF0. La même construction peut être faite pour n’importe que ensemble initial de formules atomiques. Cela montre que si une théorie a un modèle finitaire, alors l’ensemble de toutes ses vérités est lui aussi finitaire.