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

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

Montrons que ''AF₁'' est dans tt-V-Prod(''AAF₄AAF₄'', ''VAF₄VAF₄'', ''FAF₄FAF₄'')

:tt-V-Prod(''AAF₄AAF₄'', ''VAF₄VAF₄'', ''FAF₄FAF₄'') <math>\overset{\overset{def}{=}}{\,}</math> Extension de (Il existe Z’, Z’’, Z’’’, Z’’’’ tels que Z’ Dans Var Et Z’’ Dans ''AAF₄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₄FAF₄'')

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

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

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

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

:''FAF₄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₃'')