« Fondements des mathématiques/Preuve formelle de la cohérence de l'arithmétique formelle » : différence entre les versions

Une page de Wikiversité, la communauté pédagogique libre.
Contenu supprimé Contenu ajouté
m Bot : Remplacement de texte automatisé (-, *(…|\.\.\.) +…)
m Bot : Remplacement de texte automatisé (-<sub>1</sub> +₁)
Ligne 7 : Ligne 7 :
Les 13 axiomes de ''AF'' qui traduisent les 13 règles de production de ''VAF<sub>0</sub>'' sont évidemment vrais de ''VAF<sub>0</sub>''. Les moyens de preuve de ''Finitaire 1'' sont suffisants pour établir cette évidence. Quand on écrit une telle preuve formelle, on ne cherche qu’en apparence à prouver l’évidence. Mais ce qu’on fait en vérité c’est éprouver l’efficacité de la formalisation. Si les règles permettent de prouver des évidences, c’est un bon signe. Si elles ne le pouvaient pas, elles seraient très insuffisantes. En prouvant formellement des évidences on cherche à prouver la qualité de la formalisation mais pas les évidences que l’on prouve cependant.
Les 13 axiomes de ''AF'' qui traduisent les 13 règles de production de ''VAF<sub>0</sub>'' sont évidemment vrais de ''VAF<sub>0</sub>''. Les moyens de preuve de ''Finitaire 1'' sont suffisants pour établir cette évidence. Quand on écrit une telle preuve formelle, on ne cherche qu’en apparence à prouver l’évidence. Mais ce qu’on fait en vérité c’est éprouver l’efficacité de la formalisation. Si les règles permettent de prouver des évidences, c’est un bon signe. Si elles ne le pouvaient pas, elles seraient très insuffisantes. En prouvant formellement des évidences on cherche à prouver la qualité de la formalisation mais pas les évidences que l’on prouve cependant.


== La vérité de ''AF<sub>1</sub>'' ==
== La vérité de ''AF₁'' ==
La preuve suivante de la vérité de l’axiome ''AF1'' qui traduit la règle ''R<sub>1</sub>'' de ''VAF<sub>0</sub>'' a une valeur générale. N’importe quel axiome qui traduit une règle de production d’un modèle est vrai pour ce modèle, et la preuve de ceci peut être formalisée dans ''Finitaire 1''.
La preuve suivante de la vérité de l’axiome ''AF1'' qui traduit la règle ''R₁'' de ''VAF<sub>0</sub>'' a une valeur générale. N’importe quel axiome qui traduit une règle de production d’un modèle est vrai pour ce modèle, et la preuve de ceci peut être formalisée dans ''Finitaire 1''.


:''AF<sub>1</sub>'' (pour tout ''x'')(pour tout ''y'')(si ''x = y'' alors ''sx = sy'')
:''AF₁'' (pour tout ''x'')(pour tout ''y'')(si ''x = y'' alors ''sx = sy'')


''AF<sub>1</sub>'' est représenté par :
''AF₁'' est représenté par :


:<code>a(rttx)asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)</code>
:<code>a(rttx)asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)</code>


Il faut prouver que ''AF<sub>1</sub>'' est dans ''VAF''. Montrons qu’il est dans ''VAF<sub>5</sub>''.
Il faut prouver que ''AF₁'' est dans ''VAF''. Montrons qu’il est dans ''VAF<sub>5</sub>''.


:''VAF<sub>5</sub>'' <math>\overset{\overset{def}{=}}{\,}</math> Union(non-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), et-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), ou-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), ex-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), tt-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>'') )
:''VAF<sub>5</sub>'' <math>\overset{\overset{def}{=}}{\,}</math> Union(non-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), et-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), ou-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), ex-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>''), tt-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>'') )


Montrons que ''AF<sub>1</sub>'' est dans tt-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>'')
Montrons que ''AF₁'' est dans tt-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>'')


:tt-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>'') <math>\overset{\overset{def}{=}}{\,}</math> Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans ''AAF<sub>4</sub>'' 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(''FAF<sub>4</sub>'')
:tt-V-Prod(''AAF<sub>4</sub>'', ''VAF<sub>4</sub>'', ''FAF<sub>4</sub>'') <math>\overset{\overset{def}{=}}{\,}</math> Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans ''AAF<sub>4</sub>'' 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(''FAF<sub>4</sub>'')
Ligne 26 : Ligne 26 :
:tt-F-Prod(''FAF<sub>4</sub>'') =<math>\overset{\overset{def}{=}}{\,}</math> Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans ''FAF<sub>4</sub>'' Et Z’’’ Dans ''PAF'' Et Z’’’’ Dans ''N'' Et Z Dans PAF Et Z Egale assZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub)
:tt-F-Prod(''FAF<sub>4</sub>'') =<math>\overset{\overset{def}{=}}{\,}</math> Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans ''FAF<sub>4</sub>'' Et Z’’’ Dans ''PAF'' Et Z’’’’ Dans ''N'' Et Z Dans PAF Et Z Egale assZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub)


Montrons d’abord que ''AF<sub>1</sub>'' est dans Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans ''AAF<sub>4</sub>'' Et Z’’’ Dans ''PAF'' Et Z’’’’ Dans ''N'' Et Z Dans ''PAF'' Et Z Egale assZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub) .
Montrons d’abord que ''AF₁'' est dans Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans ''AAF<sub>4</sub>'' Et Z’’’ Dans ''PAF'' Et Z’’’’ Dans ''N'' Et Z Dans ''PAF'' Et Z Egale assZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub) .


:''AF<sub>1</sub>'' = <code>ass(rx)asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)</code>
:''AF₁'' = <code>ass(rx)asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)</code>


Il suffit de choisir :
Il suffit de choisir :
Ligne 40 : Ligne 40 :
:Z’’’’ = <code>o</code>
:Z’’’’ = <code>o</code>


Il reste à montrer que ''AF<sub>1</sub>'' n’est pas dans tt-F-Prod(''FAF<sub>4</sub>'').
Il reste à montrer que ''AF₁'' n’est pas dans tt-F-Prod(''FAF<sub>4</sub>'').


Prouvons (''i'') :
Prouvons (''i'') :


:(''i'') Pour tout z’, z’’, z’’’, z’’’’, si z’ est dans Var, z’’ est dans ''FAF<sub>4</sub>'', z’’’ est dans ''PAF'', z’’’’ est dans ''N'' et Cz’’Cz’’’’Cz’z’’’ est dans Sub, alors ''AF<sub>1</sub>'' ≠ assz’z’’’.
:(''i'') Pour tout z’, z’’, z’’’, z’’’’, si z’ est dans Var, z’’ est dans ''FAF<sub>4</sub>'', z’’’ est dans ''PAF'', z’’’’ est dans ''N'' et Cz’’Cz’’’’Cz’z’’’ est dans Sub, alors ''AF₁'' ≠ assz’z’’’.


On peut prouver facilement si z ≠ rx alors ''AF<sub>1</sub>'' ≠ assz’z’’’, il reste à montrer que ''AF<sub>1</sub>'' ≠ ass(rx)z’’’.
On peut prouver facilement si z ≠ rx alors ''AF₁'' ≠ assz’z’’’, il reste à montrer que ''AF₁'' ≠ ass(rx)z’’’.


Supposons ''AF<sub>1</sub>'' = ass(rx)z’’’ (''hyp'').
Supposons ''AF₁'' = ass(rx)z’’’ (''hyp'').


Alors
Alors
Ligne 74 : Ligne 74 :
On veut alors montrer que <code>a(ret)b(a(r=)bxy)a(rnon)a(r=)b(a(rs)x)a(rs)y</code> n’est pas dans ''VAF<sub>2</sub>''.
On veut alors montrer que <code>a(ret)b(a(r=)bxy)a(rnon)a(r=)b(a(rs)x)a(rs)y</code> n’est pas dans ''VAF<sub>2</sub>''.


La définition de ''VAF<sub>2</sub>'' conduit à vouloir montrer que <code>a(r=)bxy</code> et <code>a(rnon)a(r=)b(a(rs)x)a(rs)y</code> ne sont pas tous les deux dans ''VAF<sub>1</sub>''.
La définition de ''VAF<sub>2</sub>'' conduit à vouloir montrer que <code>a(r=)bxy</code> et <code>a(rnon)a(r=)b(a(rs)x)a(rs)y</code> ne sont pas tous les deux dans ''VAF₁''.


La définition de ''VAF<sub>1</sub>'' conduit à vouloir montrer que ou <code>a(r=)bxy</code> n’est pas dans ''VAF<sub>0</sub>'' ou <code>a(r=)b(a(rs)x)a(rs)y</code> est dans ''VAF<sub>0</sub>'', pour tous x et y dans N.
La définition de ''VAF₁'' conduit à vouloir montrer que ou <code>a(r=)bxy</code> n’est pas dans ''VAF<sub>0</sub>'' ou <code>a(r=)b(a(rs)x)a(rs)y</code> est dans ''VAF<sub>0</sub>'', pour tous x et y dans N.


:''VAF<sub>0</sub>'' =def Ensemble-somme de Ensemble induit par Prod à partir de Singleton de a(r=)boo
:''VAF<sub>0</sub>'' =def Ensemble-somme de Ensemble induit par Prod à partir de Singleton de a(r=)boo
Ligne 102 : Ligne 102 :
On en conclut que <code>a(r=)b(a(rs)x)a(rs)y</code> est dans Im par Prod1 de w et donc dans ''VAF<sub>0</sub>''.
On en conclut que <code>a(r=)b(a(rs)x)a(rs)y</code> est dans Im par Prod1 de w et donc dans ''VAF<sub>0</sub>''.


Cela termine cette preuve de la vérité de ''AF<sub>1</sub>'' dans ''VAF<sub>0</sub>''. Toutes les étapes n’ont pas toujours été explicitées mais il s’agit à chaque fois de la même technique, expliciter les définitions des ensembles étudiés et déduire avec la logique du premier ordre et les axiomes de ''Finitaire 1'' les énoncés que l’on veut prouver. Toutes les étapes de ces preuves, longues à écrire mais rapides à trouver, sont également triviales. Elles consistent essentiellement à vérifier qu’on n’a pas oublié de mentionner toutes les règles évidentes dans les axiomes de ''Finitaire 1''.
Cela termine cette preuve de la vérité de ''AF₁'' dans ''VAF<sub>0</sub>''. Toutes les étapes n’ont pas toujours été explicitées mais il s’agit à chaque fois de la même technique, expliciter les définitions des ensembles étudiés et déduire avec la logique du premier ordre et les axiomes de ''Finitaire 1'' les énoncés que l’on veut prouver. Toutes les étapes de ces preuves, longues à écrire mais rapides à trouver, sont également triviales. Elles consistent essentiellement à vérifier qu’on n’a pas oublié de mentionner toutes les règles évidentes dans les axiomes de ''Finitaire 1''.


== La vérité de AF14 ==
== La vérité de AF14 ==

Version du 27 décembre 2008 à 16:31

La théorie Finitaire 1 permet de formaliser la preuve naturelle de la cohérence de l’arithmétique formelle AF.

Il faut montrer que l’ensemble des axiomes de AF est inclus dans l’ensemble VAF des vérités du modèle VAF0. Tous ces ensembles sont constructibles dans Finitaire 1.

Pourquoi prouver des évidences ?

Les 13 axiomes de AF qui traduisent les 13 règles de production de VAF0 sont évidemment vrais de VAF0. Les moyens de preuve de Finitaire 1 sont suffisants pour établir cette évidence. Quand on écrit une telle preuve formelle, on ne cherche qu’en apparence à prouver l’évidence. Mais ce qu’on fait en vérité c’est éprouver l’efficacité de la formalisation. Si les règles permettent de prouver des évidences, c’est un bon signe. Si elles ne le pouvaient pas, elles seraient très insuffisantes. En prouvant formellement des évidences on cherche à prouver la qualité de la formalisation mais pas les évidences que l’on prouve cependant.

La vérité de AF₁

La preuve suivante de la vérité de l’axiome AF1 qui traduit la règle R₁ de VAF0 a une valeur générale. N’importe quel axiome qui traduit une règle de production d’un modèle est vrai pour ce modèle, et la preuve de ceci peut être formalisée dans Finitaire 1.

AF₁ (pour tout x)(pour tout y)(si x = y alors sx = sy)

AF₁ est représenté par :

a(rttx)asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)

Il faut prouver que AF₁ est dans VAF. Montrons qu’il est dans VAF5.

VAF5 Union(non-V-Prod(AAF4, VAF4, FAF4), et-V-Prod(AAF4, VAF4, FAF4), ou-V-Prod(AAF4, VAF4, FAF4), ex-V-Prod(AAF4, VAF4, FAF4), tt-V-Prod(AAF4, VAF4, FAF4) )

Montrons que AF₁ est dans tt-V-Prod(AAF4, VAF4, FAF4)

tt-V-Prod(AAF4, VAF4, FAF4) Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans AAF4 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(FAF4)
tt-F-Prod(FAF4) = Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans FAF4 Et Z’’’ Dans PAF Et Z’’’’ Dans N Et Z Dans PAF Et Z Egale assZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub)

Montrons d’abord que AF₁ est dans Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans AAF4 Et Z’’’ Dans PAF Et Z’’’’ Dans N Et Z Dans PAF Et Z Egale assZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub) .

AF₁ = ass(rx)asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)

Il suffit de choisir :

Z’ = rx
Z’’ = asss(rttx)a(rnon)a(ret)b(a(r=)bosss(rx))a(rnon)a(r=)b(a(rs)oa(rs)sss(rx)
Z’’’ = asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)
Z’’’’ = o

Il reste à montrer que AF₁ n’est pas dans tt-F-Prod(FAF4).

Prouvons (i) :

(i) Pour tout z’, z’’, z’’’, z’’’’, si z’ est dans Var, z’’ est dans FAF4, z’’’ est dans PAF, z’’’’ est dans N et Cz’’Cz’’’’Cz’z’’’ est dans Sub, alors AF₁ ≠ assz’z’’’.

On peut prouver facilement si z ≠ rx alors AF₁ ≠ assz’z’’’, il reste à montrer que AF₁ ≠ ass(rx)z’’’.

Supposons AF₁ = ass(rx)z’’’ (hyp).

Alors

z’’’ = asss(rttx)a(rnon)a(ret)b(a(r=)b(rx)sss(rx))a(rnon)a(r=)b(a(rs)(rx))a(rs)sss(rx)
z’’= asss(rttx)a(rnon)a(ret)b(a(r=)bz’’’sss(rx))a(rnon)a(r=)b(a(rs)z’’’a(rs)sss(rx)

On veut déduire une contradiction à partir de hyp. Il suffit de prouver que z’ n’est pas dans FAF4.

FAF4 =def Union(non-F-Prod(AAF3, VAF3, FAF3), et-F-Prod(AAF3, VAF3, FAF3), ou-F-Prod(AAF3, VAF3, FAF3), ex-F-Prod(AAF3, VAF3, FAF3), tt-F-Prod(FAF3)

Montrons que z’ n’est pas dans tt-F-Prod(FAF3).

Le même raisonnement que ci-dessus peut être répété et on est conduit à vouloir prouver que :

Si x et y sont dans N alors a(rnon)a(ret)b(a(r=)bxy)a(rnon)a(r=)b(a(rs)x)a(rs)y n’est pas dans FAF3.
FAF3 =def Union(non-F-Prod(AAF2, VAF2, FAF2), et-F-Prod(AAF2, VAF2, FAF2), ou-F-Prod(AAF2, VAF2, FAF2), ex-F-Prod(AAF2, VAF2, FAF2), tt-F-Prod(AAF2, VAF2, FAF2)
non-F-Prod(AAF2, VAF2, FAF2) =def Ensemble-image par non-P-Prod de VAF2
non-P-Prod =def Fonction a(rnon)X

On veut alors montrer que a(ret)b(a(r=)bxy)a(rnon)a(r=)b(a(rs)x)a(rs)y n’est pas dans VAF2.

La définition de VAF2 conduit à vouloir montrer que a(r=)bxy et a(rnon)a(r=)b(a(rs)x)a(rs)y ne sont pas tous les deux dans VAF₁.

La définition de VAF₁ conduit à vouloir montrer que ou a(r=)bxy n’est pas dans VAF0 ou a(r=)b(a(rs)x)a(rs)y est dans VAF0, pour tous x et y dans N.

VAF0 =def Ensemble-somme de Ensemble induit par Prod à partir de Singleton de a(r=)boo
Prod =def Fonction Prod1(X) Union (Prod2(X) Union (Prod3(X) Union … Prod13(X) ))

Supposons que a(r=)bxy soit dans VAF0.

Il y a un w tel que a(r=)bxy est dans w et w est dans Ensemble induit par Singleton de Prod à partir de Singleton de Singleton de a(r=)boo

Im par Prod de w est aussi dans Ensemble induit par Singleton de Prod à partir de Singleton de Singleton de a(r=)boo

Prod =def Fonction Prod1(X) Union (Prod2(X) Union (Prod3(X) Union … Prod13(X) ))

Im par Prod1 de w est donc inclus dans Im par Prod de w

Prod1 =def Fonction Extension de (Il existe un Z’ tel que Z’ Dans X Et CZ’Z Dans Inst-R1)
Inst-R1 =def Ensemble-image par Rep-R1 de Produit cartésien de Tconst et Tconst
Rep-R1 =def Fonction C(a(r=)bXX’)(a(r=)b(a(rs)X)a(rs)X’)

C(a(r=)bxy)a(r=)b(a(rs)x)a(rs)y est dans Inst-R1 puisque x et y sont dans N et que N est inclus dans Tconst.

On en conclut que a(r=)b(a(rs)x)a(rs)y est dans Im par Prod1 de w et donc dans VAF0.

Cela termine cette preuve de la vérité de AF₁ dans VAF0. Toutes les étapes n’ont pas toujours été explicitées mais il s’agit à chaque fois de la même technique, expliciter les définitions des ensembles étudiés et déduire avec la logique du premier ordre et les axiomes de Finitaire 1 les énoncés que l’on veut prouver. Toutes les étapes de ces preuves, longues à écrire mais rapides à trouver, sont également triviales. Elles consistent essentiellement à vérifier qu’on n’a pas oublié de mentionner toutes les règles évidentes dans les axiomes de Finitaire 1.

La vérité de AF14

Il reste à prouver que les représentants de AF14, AF15 et des axiomes d’induction complète sont dans VAF.

AF14 Pour tous x et y, si x<y alors non(x=y)

AF14 est représenté par

a(rttx)asss(rttx)a(rnon)a(ret)b(a(r<)b(rx)sss(rx))a(r=)b(rx)sss(rx)

Le même raisonnement que pour AF1 conduit à vouloir montrer que a(r<)bxy n’est pas dans VAF0 ou a(r=)bxy n’est pas dans VAF0, pour tous x et y dans N.

On va prouver que VAF0 est inclus dans VAF0 Moins Absurd1

Absurd1 =def Im par Egal-P-Prod de Extension de (Z Dans N Et Z’ Dans N Et Non Z Egale Z’).

Soient PVAF =def Ensemble induit par Prod à partir de Singleton de a(r=)boo.

Montrons que pour tout z dans PVAF z = z Moins Absurd1

Comme o = o, a(r=)boo n’est pas dans Absurd1, donc Singleton de a(r=)boo = Singleton de a(r=)boo Moins Absurd1

Soit z dans PVAF tel que z = z Moins Absurd1.

On peut montrer Prod2(z) Moins Absurd1 =Prod2(z) parce que les éléments de Prod2(z) sont tous de la forme a(r<)buv. De même pour Prod3(z), Prod12(z) et Prod13(z). Pour Prod4(z) à Prod9(z), leurs éléments sont tous de la forme a(r=)b(a(r+)buv)w ou a(r=)b(a(r.)buv)w et ne sont donc pas dans Absurd1. Les éléments de Prod1(z), Prod10(z) et Prod11(z) ne sont pas dans Absurd1 parce que les éléments de z ne sont pas dans Absurd1. On en conclut que Prod(z) Moins Absurd1 = Prod(z).

Par induction complète on conclut que pour tout z dans PVAF z = z Moins Absurd1.

Il est alors facile de prouver que VAF0 = Ensemble-somme de PVAF = VAF0 Moins Absurd1

On peut prouver de la même façon que VAF0 = VAF0 Moins Absurd2 Absurd2 =def Im par <-P-Prod de Extension de Z Dans N et Z’ Dans N et Z Egale Z’.

Supposons alors que a(r=)bxy soit dans VAF0 et que x et y sont dans N.

Comme a(r=)bxy n’est pas dans Absurd1, x = y. Comme a(r<)bxx est dans Absurd2, a(r<)bxy n’est pas dans VAF0. Cela termine cette preuve abrégée de la vérité de AF14. La vérité de AF15 peut être prouvée par un raisonnement semblable.

La vérité des axiomes d’induction complète

Soit AxIC l’ensemble des (représentants des) axiomes d’induction complète.

AxIC= Ensemble-somme de Image par IC-Prod de PAF

Si P est dans PAF, IC-Prod(P) est l’ensemble fini des axiomes d’induction complète qu’il définit. Ic-Prod(P) contient autant d’éléments que le prédicat P a de variables libres. La construction de AxIC est laborieuse mais elle ne pose pas de difficultés de principes parce qu’il s’agit d’une question décidable. Une démarche semblable aux preuves de vérités des autres axiomes conduit alors à vouloir prouver que les trois hypothèses suivantes sont mutuellement contradictoires pour un élément P de PAF, et n+1 éléments c, c1…., cn de N,

(i) la formule qui traduit P(0, c1…., cn) , c’est-à-dire la substitution de 0 à l’une des variables x de P et de c1…., cn aux autres variables, est un élément de VAF.

(ii) la formule qui traduit (pour tout x, si P(x, c1…., cn) alors P(sx, c1…., cn) ) est dans VAF

(iii) la formule qui traduit non P(c, c1…., cn) est dans VAF

La preuve de cette contradiction est rendu aisée par le fait que VAF est clos par l’opération de conséquence logique, autrement dit, si une formule est la conséquence logique de formules qui sont dans VAF alors elle est aussi dans VAF.

Toutes ses preuves sont longues à écrire mais elles ne posent pas de véritables difficultés autres que la précision des définitions. Le raisonnement est une simple traduction formalisée du raisonnement mis en œuvre dans la preuve naturelle.

Cela termine cette preuve abrégée que Finitaire1 permet de prouver la cohérence de AF.