We have already mentioned that the names of bound variables do not matter. Everybody agrees that
is equivalent to
Sometimes we would like to rename some of the identifiers in a formula in order to make it easier to read. How do we ensure that our renaming does not change the meaning of the original formula?
Given a formula 
, we may change the name of a bound variable in and
obtain a formula 
equivalent to provided
no occurrence of an object identifier that was free in
becomes bound in , and every occurrence of a bound object
identifier in has the same binding in .
(Note, it is not enough that bound object identifiers remain bound, they
must remain bound to the same quantifier.)
Whenever we rename bound variables we refer to the rule of inference called Bound Variable Renaming. Bound variable renaming does not require any justification in MIZAR texts.
Let us look at some examples.
is equivalent to
and is not equivalent to
as a formerly free object identifier ( the y in P[z,y] ) has become bound.
is not equivalent to
as a free object identifier x in for x being T holds P[x,y,z] has become bound in for z being T holds P[z,y,z].
is not equivalent to
as a free object identifier y has become bound.
Inference rules for quantifiers involve renaming of object identifiers and a textual operation on formulas, called proper free substitution. This is its definition:
We say the formulacomes from formula
for object identifier
if
- the sort of
It is important to remember that proper free substitution is not an inference rule. It is a rule for editing formulas textually.
For example, the formula
becomes, under proper free substitution of Wilma for Fred, the formula
This in turn becomes, under proper free substitution of Hello for s, the formula
We use the notation 
to stand for the formula resulting
from the proper free substitution of for in formula .
Another way to think of this notation is of replacing every
free occurrence of by without introducing any
new bound occurrences of .
Note that there is no notation for proper free substitution that is
consistently used by all authors of logic texts,
so it is always important to determine the convention used for
each particular work.
This notation lets us define three more inference rules.
= ,   | provided is identical to
|
This requires some explanation. The intended meaning of this rule is that
we can exchange some or all free occurrences of and in a formula
provided =.
The condition attached to the formula says just that.
It might be easier to understand the formula if you look at it this way.
Knowing that = we may think that is just another name
of the same object named by . So, let us choose as the only name
that we use, is just an alias.
Examples.
environ
given a, b being THING;
1: a = b;
begin
b = a by 1; == =E
This example may look cryptic. The two premises needed by the inference rule
are formed by the same formula a=b. And indeed,
is identical to
as both of them are b=b.
environ
given a, b, c being THING;
1: a = b;
2: b = c;
begin
a = c by 1, 2; == =E
Here we see that
is identical to
.
environ
given a, b being THING;
1: P[a];
2: not P[b];
begin
R: now
assume step1: a = b;
step2: not P[a] by step1, 2; == =E
thus step3: contradiction by 1, step2; == ContrI
end;
a <> b by R; == PbyC
environ
given a, b, c being THING;
1: P[a];
2: not P[c];
3: a = b;
begin
b <> c by 1, 2, 3; == No single inference rule suffices.
== Mizar can figure out which basic rules are involved.
It is a worthwhile exercise to write the above using only single inference rules.
being 
holds where is any visible object identifier of sort .
This rule is sometimes called universal instantiation, or universal specialization, because it specializes a general statement about any object into a specific statement about a particular object. It represents our intuition that what holds for everything must hold for any specific thing. Look at these inferences.
environ
given Fred being PERSON;
given Hello being STATEMENT;
KnightSpeak: for y being PERSON holds
for s being STATEMENT holds
Knight[y] & Tells[y,s] implies True[s];
begin
== Specialize the y to Fred.
1: for s being STATEMENT holds
Knight[Fred] & Tells[Fred,s] implies True[s]
by KnightSpeak; == UE
== Further Specialize the s in 1 to Hello.
2: Knight[Fred] & Tells[Fred,Hello] implies True[Hello] by 1; == UE
== You must instantiate in the order that the quantifiers occur
== thus attempting to specify s to Hello will not work.
3: for y being PERSON holds
Knight[y] & Tells[y,Hello] implies True[Hello] by KnightSpeak;
== That is, when you have a list of universal quantifiers, only the
== leading ones can be eliminated.
== In order to achieve the inner universal quantifier elimination you
== have to use Universal Introduction, see below.
Suppose that you have the formula A[x] & B[x] in some context, where x is of sort THING. This means that there is a precise object, named x, which satisfies the formula. We can then certainly write:
ex y being THING st A[y] & B[y]
This formula is read as ``There exists some object y satisfying A[y] & B[y]''. We know that this is true at least in the case that y denotes the same object as x. There may also be objects other than the one denoted by x which also satisfy the formula.
But we also know that the following formula is true for exactly the same reasons:
ex y being THING st A[y] & B[x]
Note how only the argument to predicate A was changed.
In general we can do the following kind of inference.
being st where is a visible object identifier of sort .
This rule is sometimes called Existential Generalization. Note the particular form of this rule.
s. Note that the formula of the form
does not have free s.
to
and then existentially quantify the s.
(Note not necessarily all!).
For example, here are different existential statements that can be concluded from the same formula.
environ
given x,y being THING;
A: P[x,y,x];
begin
== Generalize with respect to y.
ex a being THING st P[x,a,x] by A; == ExI
== Generalize with respect to x.
ex b being THING st P[b,y,b] by A; == ExI
== Generalize with respect to the first x.
ex c being THING st P[c,y,x] by A; == ExI
== Generalize with respect to nothing.
ex d being THING st P[x,y,x] by A; == ExI
Here is an example of using universal elimination and existential introduction in an argument.
environ
given Fred being PERSON;
given Hello being STATEMENT;
A1: for x being PERSON holds
ex s being STATEMENT st
(Tells[x,s] & Tells[x,Hello] & s <> Hello & True[s]);
begin
== Here we universally instantiate, substituting Fred for x
== and eliminating the universal quantifier.
1: ex s being STATEMENT st
(Tells[Fred,s] & Tells[Fred,Hello] & s <> Hello & True[s]) by A1; == UE
== Existential generalization, replace all occurrences
== of Hello by t, and add the existential quantifier
2: ex t being STATEMENT st
ex s being STATEMENT st
(Tells[Fred,s] & Tells[Fred,t] & s <> t & True[s]) by 1; == ExI
== Existentially generalize, replace only the first
== of Fred occurrences by y, and add the existential quantifier.
3: ex y being PERSON st
ex t being STATEMENT st
ex s being STATEMENT st
(Tells[y,s] & Tells[Fred,t] & s <> t & True[s]) by 2; == ExI
environ
given Fred being PERSON;
given Hello being STATEMENT;
KnightSpeak: for y being PERSON for s being STATEMENT
holds Knight[y] & Tells[y,s] implies True[s];
A1: Knight[Fred];
A2: Tells[Fred, Hello];
begin
== Here is an example of Universal Instantiation.
1: for s being STATEMENT holds
Knight[Fred] & Tells[Fred,s] implies True[s] by KnightSpeak;
== And here is an example of Existential Generalization.
1a: ex s being STATEMENT st Tells[Fred,s] by A2;
1b: ex x being PERSON, s being STATEMENT st Tells[x,s] by A2;
1c: ex x being PERSON st Tells[x,Hello] by A2;
== This is also correct.
1d: ex x being KNIGHT, s being STATEMENT st Tells[Fred,Hello] by A2;
KnightSpeak1: for t being STATEMENT for x being PERSON
holds Knight[x] & Tells[x,t] implies True[t] proof
let t be STATEMENT;
== now we have to show the "for x ..." part
let x be PERSON;
thus Knight[x] & Tells[x,t] implies True[t] by KnightSpeak;
end;
2: for y being PERSON holds
Knight[y] & Tells[y,Hello] implies True[Hello] by KnightSpeak1;
2a: for y being PERSON holds
Knight[y] & Tells[y,Hello] implies True[Hello] proof
let y be PERSON;
1: for s being STATEMENT holds
Knight[y] & Tells[y,s] implies True[s] by KnightSpeak;
thus
Knight[y] & Tells[y,Hello] implies True[Hello] by 1;
end;
3: Knight[Fred] & Tells[Fred,Hello] implies True[Hello] by KnightSpeak;
4: True[Hello] by A1, A2, 3;
To introduce a universal quantifier we do another kind of hypothetical reasoning, called universal generalization or universal introduction. The intuition here is that to prove that some formula holds for all objects we show that it holds for any arbitrarily selected but fixed object.
 : now
| |
|
let be ;
| |
| . | |
| . | |
| . | |
|
thus Justification
| |
| end; | |
being holds by
where and are permitted to be identical object identifiers.
The formula must not contain any
free occurrences of any object identifier introduced inside the now
other than .
Remember that any formula visible at line which has
free will not be properly
visible inside the reasoning. The `value' of the object identifier defined outside of the reasoning
is not arbitrary (many things could have already been stated about it),
and so any formula with a free from outside the proof
is actually referring to a different object than the
inside the proof.
(Go back now and reread the definition of visibility).
So for example, the following inference is correct
environ
given Fred being PERSON;
A: Knight[Fred];
begin
== We prove that for all persons, Fred is a knight.
== (Do not worry that it does not make much sense.)
1: now
let p be PERSON;
thus Knight[Fred] by A; == RE
end;
for p being PERSON holds Knight[Fred] by 1 == UI
while this one is not:
environ
given Fred being PERSON;
A: Knight[Fred];
begin
== This says the same as in the previous example.
== But it tries to prove that all persons are knights!
1: now
let Fred be PERSON; == You can do it.
== The following does not work as Fred mentioned in axiom A
== is not the same Fred as inside this reasoning.
thus Knight[Fred] by A;
****************************99
**
** 99 Your inference is not accepted by the checker.
**
end;
for p being PERSON holds Knight[Fred] by 1; == UI
********************************************99
**
** 99 Your inference is not accepted by the checker.
**
== Note. The reasoning at 1 was incorrect, still we can make
== a reference to it.
== The above does not work, but the step below does.
for Fred being PERSON holds Knight[Fred] by 1; == UI
We can now complete the example where we wanted to instantiate an inner quantifier. Note how we do renaming of the quantified object from y in the now, to yy in the concluded formula 2.
environ
given Fred being PERSON;
given Hello being STATEMENT;
KnightSpeak: for y being PERSON holds
for s being STATEMENT holds
Knight[y] & Tells[y,s] implies True[s];
begin
== We want to substitute Hello for s.
1: now
let y be PERSON;
1: for s being STATEMENT holds
Knight[y] & Tells[y,s] implies True[s] by KnightSpeak; == UE
thus Knight[y] & Tells[y,Hello] implies True[Hello] by 1; == UE
end;
2: for yy being PERSON holds
Knight[yy] & Tells[yy,Hello] implies True[Hello] by 1 == UI
Our last inference rule is used to convert an existential statement about some object, into a statement about a specific object. The idea is that if we have
being st then will hold for some specific object
of sort .
But since we do not know what that object actually is, the name
that we give it should be different from any other visible name.
Otherwise, unexpectedly, we can give a new meaning to a name
that we have been using.
The inference rule looks like
being st being such that : Where the formula must not contain any free .
The consider statement introduces a new object with identifier
and sort .
This will hide all prior instances of and any prior
formulas with a free cannot be used in the current scope as they
contain the now hidden previous .
Here is a complicated example illustrating this inference rule.
environ
given Hello being STATEMENT;
given Fred being PERSON;
== Hello is a true statement.
Fact1: True[Hello];
== Fred always lies.
Fact2: for s being STATEMENT holds Tells[Fred,s] implies not True[s];
== Every person is either a Knight or a Knave, but not both.
Opp: for a being PERSON holds Knight[a] iff not Knave[a];
== A person is a knight if and only if every statement
== they say is true.
Veracity: for a being PERSON holds
Knight[a] iff
(for s being STATEMENT holds Tells[a,s] implies True[s]);
== If at least one of the things you say is false
== then everything you say is false.
Consistency: for a being PERSON holds
(ex s being STATEMENT st Tells[a,s] & not True[s]) implies
(for s being STATEMENT holds Tells[a,s] implies not True[s]);
== Every person says at least one thing.
Verbosity: for p being PERSON holds ex s being STATEMENT st Tells[p,s];
== Some person says everything.
BlabberMouth: ex p being PERSON st for s being STATEMENT holds Tells[p,s];
begin
== We demonstrate that there is some person who says Hello.
== Use the fact that blabber mouth exists.
consider blabber being PERSON such that
1: for s being STATEMENT holds Tells[blabber,s]
by BlabberMouth; == ExE
== Combine this with the fact that Hello is a statement.
2: Tells[blabber, Hello] by 1; == UE
== Now existentially generalize
ex p being PERSON st Tells[p,Hello] by 2; == ExI
== We prove that there exists some person p such that if they
== are a knight then all statements are true.
== This example should demonstrate to you that the scope of
== an existential quantifier better not be a conditional,
== if it is possible for the antecedent to be false for some
== object.
consider blabber being PERSON such that
1: for s being STATEMENT holds Tells[blabber,s]
by BlabberMouth; == ExE
2': now
assume A: Knight[blabber];
3: for s being STATEMENT holds
Tells[blabber,s] implies True[s]
by Veracity, A; == UE, EqE
4: now
let s be STATEMENT;
5: Tells[blabber,s] by 1; == UE
thus True[s] by 3, 5; == UE, IE
end;
thus for s being STATEMENT holds True[s] by 4; == UI
end;
2: Knight[blabber] implies
(for s being STATEMENT holds True[s]) by 2'; == II
ex p being PERSON st
(Knight[p] implies (for s being STATEMENT holds True[s]))
by 2; == ExI
== Note that we can reference 2' directly.
ex p being PERSON st
(Knight[p] implies (for s being STATEMENT holds True[s]))
by 2'; == ExI
In the example above we have indicated the lines where two basic rules of inference have been used, in the indicated order. Although, we need not doing it to satisfy the MIZAR checker, sometimes it helps to clarify things for ourselves.
As with derived inference rules for propositional calculus, there are derived inference rules for quantifiers. Here we mention only the so called De Morgan's Laws (See 6.3.11 for the De Morgan's laws in their quantifier-free version.) and attach the corresponding argument using only the basic rules of inference.
being holds ) being st not environ
A1: not (for a being T holds PHI[a]);
begin
1: now
assume
step1: not (ex a being T st not PHI[a]);
step2: now
let x be T;
step3': now assume
step3: not PHI[x];
step4: ex a being T st not PHI[a] by step3; == ExI
thus contradiction by step1, step4; == ContrI
end;
thus PHI[x] by step3'; == PbyC
end; == We have just shown: for a being T holds PHI[a].
thus contradiction by A1, step2; == ContrI
end;
ex a being T st not PHI[a] by 1 == PbyC
being st ) being holds not environ
A1: not (ex a being T st PHI[a]);
begin
1: now
let x be T;
step0: now
assume step1: PHI[x];
step2: ex a being T st PHI[a] by step1; == ExI
thus contradiction by A1, step2; == ContrI
end;
thus not PHI[x] by step0 == NI
end;
for a being T holds not PHI[a] by 1; == UI
being holds not being st ) environ
A1: for a being T holds not PHI[a];
begin
1: now
assume step1: ex a being T st PHI[a];
consider x being T such that
step2: PHI[x] by step1; == ExE
step3: not PHI[x] by A1; == UE
thus contradiction by step2, step3; == ContrI
end;
not (ex a being T st PHI[a]) by 1 == PbyC
being st not being holds ) environ
A1: ex a being T st not PHI[a];
begin
1: now
assume step1: for a being T holds PHI[a];
consider x being T such that
step2: not PHI[x] by A1; == ExE
step3: PHI[x] by step1; == UE
thus contradiction by step2, step3; == ContrI
end;
not (for a being T holds PHI[a]) by 1 == PbyC