The truth value of tautologies and contradictions does not depend on the current interpretation. However, if a formula is a contingency, we should be able to find an interpretation that satisfies the formula, and one that falsifies it. Here is an example:
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;
A formal proof of a formula by itself is just a string of characters. It has no intrinsic meaning. To give the proof meaning we must use the axioms in the environment to provide an interpretation for the predicates and constants in the proof. Arriving at suitable premises for an argument can be very difficult, because it requires one to thoroughly understand the problem at hand. But choosing your premises wisely is most important, for a correct proof means nothing if it is based on inappropriate premises.
Consider the following example:
environ
== We interpret the predicates Div and Mult as follows:
== Div[x,y,z] iff x / y = z
== Mult[x,y,z] iff x * y = z
reserve x,y,z,t,p for Real;
A1: for x,y,z holds Div[x, y, z] iff Mult[z, y, x];
A2: for x,y,z,t holds Div[z, t, x] & Div[z, t, y] implies x=y;
A3: ex p st for x holds Mult[x, p, p];
begin
absurd: for x, y holds x=y proof
let x, y be Real;
consider p such that
B1: for t holds Mult[t, p, p] by A3;
1: Mult[x, p, p] & Mult[y, p, p] by B1;
2: Div[p, p, x] & Div[p, p, y] by 1, A1;
3: x=y by 2, A2;
thus thesis by 3;
end;
Although the proof is perfectly correct, it has a conclusion that is blatantly silly
which says that there is only one real number!
The problem with this proof is that one of the premises is inappropriate, and does not accurately describe a property of the real numbers. Specifically, axiom A1 does not prohibit division by 0. As a result we do not have a faithful interpretation of the real numbers.
Let us consider another case where the above glitch has been fixed but another has been introduced.
environ
== We interpret the predicates Div and Mult as follows:
== Div[x,y,z] iff x / y = z
== Mult[x,y,z] iff x * y = z
reserve x,y,z,t,p for Real;
given 0 being Real;
A1: for x,y,z st y <> 0 holds Div[x, y, z] iff Mult[z, y, x];
A2: for x,y,z,t holds Div[z, t, x] & Div[z, t, y] iff x=y;
A3: ex p st for x holds Mult[x, p, p];
given 1 being Real;
A4: 1<>0;
A5: for x holds Mult[x, 1, x];
begin
absurd: for x holds Mult[0,1,x] proof
let x be Real;
a1: 0 = 0;
a2: Div[x,1,0] by a1, A2;
thus thesis by A1, a2, A4;
end;
Here is still another example with a similar problem. What is the problem?
environ
== We interpret the predicates Neg and Square as follows:
== Neg[x,y] iff y = -x
== Square[x,z] iff x * x = z
reserve x,y,z,t,p for Real;
A1: for x ex z st Neg[x,z];
A2: for x ex z st Square[x,z];
A3: for x, y, z st Neg[x,y] holds Square[x,z] iff Square[y,z];
A4: for x, y, z st Square[x,z] & Square[y,z] holds x = y;
begin
absurd: for x holds Neg[x,x] proof
let x be Real;
consider p such that
B1: Neg[x,p] by A1;
consider t such that
B2: Square[x,t] by A2;
1: Square[x,t] iff Square[p,t] by B1, A3;
2: Square[x,t] & Square[p,t] by B2, 1;
3: x=p by 2, A4;
thus thesis by B1, 3;
end;