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

m
Bot : Remplacement de texte automatisé (-<sub>4</sub> +₄)
m (Bot : Remplacement de texte automatisé (-<sub>3</sub> +₃))
m (Bot : Remplacement de texte automatisé (-<sub>4</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>AAF₄'', ''VAF<sub>4</sub>VAF₄'', ''FAF<sub>4</sub>FAF₄''), et-V-Prod(''AAF<sub>4</sub>AAF₄'', ''VAF<sub>4</sub>VAF₄'', ''FAF<sub>4</sub>FAF₄''), ou-V-Prod(''AAF<sub>4</sub>AAF₄'', ''VAF<sub>4</sub>VAF₄'', ''FAF<sub>4</sub>FAF₄''), ex-V-Prod(''AAF<sub>4</sub>AAF₄'', ''VAF<sub>4</sub>VAF₄'', ''FAF<sub>4</sub>FAF₄''), tt-V-Prod(''AAF<sub>4</sub>AAF₄'', ''VAF<sub>4</sub>VAF₄'', ''FAF<sub>4</sub>FAF₄'') )
 
Montrons que ''AF₁'' est dans tt-V-Prod(''AAF<sub>4</sub>AAF₄'', ''VAF<sub>4</sub>VAF₄'', ''FAF<sub>4</sub>FAF₄'')
 
:tt-V-Prod(''AAF<sub>4</sub>AAF₄'', ''VAF<sub>4</sub>VAF₄'', ''FAF<sub>4</sub>FAF₄'') <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>AAF₄'' 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>FAF₄'')
 
:tt-F-Prod(''FAF<sub>4</sub>FAF₄'') =<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>FAF₄'' 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>AAF₄'' Et Z’’’ Dans ''PAF'' Et Z’’’’ Dans ''N'' Et Z Dans ''PAF'' Et Z Egale assZ’Z’’’ Et CZ’’CZ’’’’CZZ’’’ Dans Sub) .
 
:''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>
:Z’’’’ = <code>o</code>
 
Il reste à montrer que ''AF₁'' n’est pas dans tt-F-Prod(''FAF<sub>4</sub>FAF₄'').
 
Prouvons (''i'') :
 
:(''i'') Pour tout z’, z’’, z’’’, z’’’’, si z’ est dans Var, z’’ est dans ''FAF<sub>4</sub>FAF₄'', 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’’’.
:z’’= <code>asss(rttx)a(rnon)a(ret)b(a(r=)bz’’’sss(rx))a(rnon)a(r=)b(a(rs)z’’’a(rs)sss(rx)</code>
 
On veut déduire une contradiction à partir de ''hyp''. Il suffit de prouver que z’ n’est pas dans ''FAF<sub>4</sub>FAF₄''.
 
:''FAF<sub>4</sub>FAF₄'' =def Union(non-F-Prod(''AAF₃'', ''VAF₃'', ''FAF₃''), et-F-Prod(''AAF₃'', ''VAF₃'', ''FAF₃''), ou-F-Prod(''AAF₃'', ''VAF₃'', ''FAF₃''), ex-F-Prod(''AAF₃'', ''VAF₃'', ''FAF₃''), tt-F-Prod(''FAF₃'')
 
Montrons que z’ n’est pas dans tt-F-Prod(''FAF₃'').
143 371

modifications