5) La compaction des introductions

   Éxaminons maintemant le début et la fin du texte :

Considérons un ensemble E quelconque.   Considérons un terme R quelconque de type (Rel E)     Posons par hypothèse (Trans R E) (H).       Considérons un élément E quelconque de x.         Considérons un élément y quelconque de E.           Considérons un élément z quelconque de E.             Posons par hypothèse (Inv E R x y) (H1).               Posons par hypothèse (Inv E R y z) (H2).                       ·                       ·                       ·               Nous avons montré (Inv E R y z)(R z x).             Nous avons montré (Inv E R x y)(Inv E R y z)(R z x).           Nous avons montré z:E.(Inv E R x y)(Inv E R y z)(R z x).         Nous avons montré y,z:E.(Inv E R x y)(Inv E R y z)(R z x).       Nous avons montré x,y,z:E.(Inv E R x y)(Inv E R y z)(R z x).     Nous avons montré (Trans E R)x,y,z:E.(Inv E R x y)(Inv E R y z)(R z x).   Nous avons montré R:(Rel E).(Trans E R)x,y,z:E.(Inv E R x y)(Inv E R y z)(R z x). Nous avons montré E:Set.R:(Rel E).(Trans E R)x,y,z:E.(Inv E R x y)(Inv E R y z)(R z x).

   Chaque nouvel élément (ensemble, relation, hypothèse) est introduit un à un. Cela n'est pas du tout la façon de faire habituelle. Cela est dû à une approche assez minimaliste du formalisme (cf curryfication des -abstractions). Il est possible réduire ce flot de paroles en utilisant des phrases un peut plus complexes. Nous regroupons maintenant l'explication de plusieurs opérateurs du formalisme en une seule phrase.

Considérons un ensemble E quelconque ; un terme R quelconque de type (Rel E) ; posons par hypothèse (Trans R E) (H) ; considérons trois éléments x, y, et z quelconques de E ; posons par hypothèse (Inv E R x y) (H1) et (Inv E R y z) (H2).       ·       ·       · Nous avons montré E:Set.R:(Rel E).(Trans E R)x,y,z:E.(Inv E R x y)(Inv E R y z)(R z x).

   Ce texte à un style assez haché et plutôt lourd, mais nous en contenterons momentanément. (Suite)

Retour

Sommaire

Suite

Yann Coscoy