environ == Examples of satisfying and falsifying interpretations

reserve t, x, y, z, w for THING;

    == We will consider three different interpretations of Blob and
    == the universe of discourse (sort THING).

I1: for x, y holds (Blob[x, y] iff x=y);
I1': ex x, y st x <> y;

I2: for x, y holds (Blob[x, y] iff x=y);
I2': not (ex x, y st x <> y);

I3: for x, y holds (Blob[x, y] iff not contradiction);

begin
          == The following is always true, but requires a proof.

Tfor: for x holds x=x     proof let x be THING; thus x=x; end;

          == In Mizar, each sort always contains at least one member.
          == Thus we can always prove the following.

Tex: ex x st x=x          proof consider t; 1: t = t; thus thesis by 1; end;

          == Mizar does not need the above proof.

     consider t;
Tex: ex x st x=x;

    == Statement T0 is true no matter what interpretation we give to Blob,
    == but Mizar is not able to prove it itself.

T0: (ex x st for y holds Blob[x, y]) implies (for y ex x st Blob[x, y])
    proof assume A1: ex x st for y holds Blob[x, y];
          let z be THING;
             consider t such that
          1: for y holds Blob[t, y] by A1;
          2: Blob[t, z] by 1;
       thus  thesis by 2;
    end;

    == Note how in proving T0 we did not make any reference to the
    == interpretation axioms.

    == But the converse of T0 is not always true.
    == Under interpretation I1 it is false.

T1: not ((for y ex x st Blob[x, y]) implies (ex x st for y holds Blob[x, y]))
    proof
       assume A1: (for y ex x st Blob[x, y]) implies
                                        (ex x st for y holds Blob[x, y]);
          == The antecedent is true using interpretation I1

          1:  for y ex x st Blob[x, y] proof
                 let y be THING;
                   2: y=y;
                   3: Blob[y, y] by I1;
                 thus ex x st Blob[x, y] by 3;
              end;
          4: ex x st for y holds Blob[x, y] by 1, A1;
                         == Now get a contradiction
             consider t such that  
          5: for y holds Blob[t, y] by 4;
             consider w, z such that 
          6: w<>z by I1';
          7: Blob[t, w] & Blob[t, z] by 5;
          8: t=w by 7, I1;
          8': t=z by 7, I1;
          9: z=w by 8, 8';
       thus contradiction by 6, 9;
end;

         == But under interpretation I2 it is true.

T2: (for y ex x st Blob[x, y]) implies (ex x st for y holds Blob[x, y])
    proof
       assume A1: for y ex x st Blob[x, y];
             consider t; 
             consider w such that 
          2: Blob[w, t] by A1;
          3: for y holds Blob[w, y] proof
                 let y be THING;
                    4: y=t by I2';
                    5: Blob[w, y] by 2, 4;
                 thus thesis by 5;
             end;
       thus ex x st for y holds Blob[x, y] by 3;
    end;

           == Interpretation I3 is an even easier way to make it true.

T3: (for y ex x st Blob[x, y]) implies (ex x st for y holds Blob[x, y])
    proof
       assume A1: for y ex x st Blob[x, y];
             consider t;
             A2: for y holds Blob[t, y] proof
                 let y be THING;
                 thus Blob[t, y] by I3;
             end;
       thus ex x st for y holds Blob[x, y] by A2;
    end;