The inference rules that we have covered so far suffice to prove whatever is provable in a given environment. (The above claim requires a proof but we do not discuss it here. It falls into the area of metalogic---that is knowledge about logic. Our interest is here about practical aspects of proving.)

Any justification of a formula in MIZAR may take the form of a *proof*.
In essence, proofs are only a syntactic variation of recording
the application of inference rules, which offers some convenient short cuts
in conducting arguments.
The syntax of proofs is similar to the syntax of reasonings.

CompactStatement ::= | [ then ] Proposition SimpleJustification |Proposition Proof |

Proof ::= | proof Reasoning end |

Using examples, we show how the proof syntax is used for
recording the `II`, `NI`, `PbyC`, and `UI` rules.

impliesproof

assumeA:

.

.

.

thusJustification

end

Let us look at the proof form of the example from section 6.1. (Note the place where we announce the rule name.)

environ given x being PERSON; Ax1: P[x] implies Q[x]; Ax2: Q[x] implies R[x]; begin P[x] implies R[x] proof == Rule: II assume A: P[x]; 1a: Q[x] by A, Ax1; == Rule: IE thus R[x] by 1a, Ax2 == Rule: IE end

Whatever we can prove with a `proof`
we can also justify using the `now` reasoning.
There is a psychological difference though.
To use a proof we have to state first what we are proving, while in case of the
`now` reasoning we can do it later, if we wish, when we state
explicitly what has been proven.
(Certainly, in both cases the MIZAR checker will tell us whether our
statements are justified.)

For example, let us prove this theorem about a `PERSON` called `x`.

We do it both ways, presenting the proof first.

environ given x being PERSON; begin == The proof version ( (P[x] implies Q[x]) & (Q[x] implies R[x]) & P[x] ) implies R[x] proof == Rule: II assume A: (P[x] implies Q[x]) & (Q[x] implies R[x]) & P[x]; 1: P[x] by A; == CE 2: P[x] implies Q[x] by A; == CE 3: Q[x] by 1, 2; == IE 4: Q[x] implies R[x] by A; == CE thus R[x] by 3,4; == IE end; == The now version 1: now assume A: (P[x] implies Q[x]) & (Q[x] implies R[x]) & P[x]; 1: P[x] by A; == CE 2: P[x] implies Q[x] by A; == CE 3: Q[x] by 1, 2; == IE 4: Q[x] implies R[x] by A; == CE thus R[x] by 3,4; == IE end; ( (P[x] implies Q[x]) & (Q[x] implies R[x]) & P[x] ) implies R[x] by 1; == II

The justification of the main proposition is in both cases
via hypothetical reasoning (*Implication Introduction*).

notproof

assumeContra: ;

.

.

.

thuscontradictionJustification

end

Compare the `proof` and the `now` versions of the
example from section 6.2.2.

environ given glass being CONTAINER; given juice being DRINK; A1: Full[glass] implies Fresh[juice]; A2: not Fresh[juice]; begin == We show that: not Full[glass] == The proof version not Full[glass] proof == NI assume A: Full[glass]; 1: Fresh[juice] by A, A1; == IE thus contradiction by 1,A2; == ContrI end; == The now version S: now assume A: Full[glass]; 1: Fresh[juice] by A, A1; == IE thus contradiction by 1,A2; == ContrI end; not Full[glass] by S == NI

proof

assumeContra:;not

.

.

.

thuscontradictionJustification

end

The example from section 6.2.2 takes the following proof form.

environ given glass being CONTAINER; begin (not Full[glass] implies Full[glass]) implies Full[glass] proof == II assume a: not Full[glass] implies Full[glass]; S: now == NI assume b: not Full[glass]; 1: Full[glass] by a,b; == MP thus contradiction by 1,b; == ContrI end; T: not not Full[glass] by S; == NI thus Full[glass] by T == NE end;

: for being holds proof

let be ;

.

.

.

thus_{}Justification

end

And now, employing a proof, the example from section 7.7 looks as follows:

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 for y being PERSON holds Knight[y] & Tells[y,Hello] implies True[Hello] == UI proof 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

We have seen above how the hypothetical reasoning (`II`),
Negation Introduction `NI`, and Universal Introduction `UI` rules
take on the a shape of a proof.
Thus we know how to write a proof for a formula with an implication,
negation, or a universal quantifier as the main connective.
We also know how to prove an arbitrary formula by contradiction.
MIZAR allows us to write a proof for an arbitrary formula, even if its
structure is suitable to use a *SimpleJustification* on a basis
of some rule of inference.

& & . . . &proof

.

thusJustification;

.

thusJustification;

.

.

.

thusJustification

end

Usually, there is no point in employing this proof structure---applying
the `CI` rule results in a shorter text.

impliesproof

assumenot ;

.

.

.

thusnotJustification

end

From the *Modus Tollens* rule we can feel that such a structure is right.
And this is the case. Unfortunately, MIZAR **does not recognize it**
as a proper structure for proving a conditional.
Too bad!
But we can always find our way around the problem and do the indirect proof
with the `now` reasoning as follows:

A:now

assumenot ;

.

.

.

thusnotJustification

end;

B: notimpliesnotbyA;

impliesbyB== Reverse Implication

== MIZAR will accept the following as well:

impliesbyA== No single rule suffices

All proofs that are not by contradiction and are not indirect, are called direct proofs.

orproof

assumenot ;

.

.

.

thusJustification

end

Unfortunately, we cannot start with the negation of the second disjunct.
But always we can call on the `now` reasoning for help.

iffproof

. . .

thusimpliesJustification;

.

.

.

thusimpliesJustification;

end

Unfortunately for MIZAR, the order of these `thus`'es is important.

The correctness of a formula may be established by *SimpleJustification*
without writing an explicit `proof` for it.
Whenever we get the MIZAR processor to accept

then we can also justify using the following proof structure:

proof

.

.

.

thusbyReferences

end

Since the latter is longer we will prefer the former way of justification. Note how the above proof structure is similar to the one we discussed for conjunction in 8.2.1. Indeed, any formula can be seen as a conjunction with exactly one conjunct, no matter how strange it sounds.

A proof nested within another proof can be incorporated directly into the encompassing proof. We start with the example, which is a variation of one of the proofs from section 6.5.

environ given S being STUDENT; given M being Money; begin (Need[M] implies Work[S] & Save[M]) implies (Need[M] implies Work[S]) & (not Save[M] implies not Need[M]) proof == II assume A:( Need[M] implies Work[S] & Save[M] ); == At this point we have to prove the consequent of the original formula. == Since it is a conjunction, we do it in two separate thus'es. thus Need[M] implies Work[S] proof == II assume A1: Need[M]; 1a: Work[S] & Save[M] by A, A1; == IE thus Work[S] by 1a; == CE end; thus not Save[M] implies not Need[M] proof == II assume A1: not Save[M]; 2a: Need[M] implies Save[M] proof == II assume A2: Need[M]; 2b: Work[S] & Save[M] by A, A2; == IE thus Save[M] by 2b; == CE end; thus not Need[M] by A1, 2a; == MT end; end;

This proof can still be refined by incorporating the last part of the conclusion into the main proof.

environ given S being STUDENT; given M being Money; begin (Need[M] implies Work[S] & Save[M]) implies (Need[M] implies Work[S]) & (not Save[M] implies not Need[M]) proof == II assume A:( Need[M] implies Work[S] & Save[M] ); == At this point we have to prove the consequent of the original formula. == It is a conjunction. The first conjunct is concluded by a thus. thus Need[M] implies Work[S] proof == II assume A1: Need[M]; 1a: Work[S] & Save[M] by A, A1; == IE thus Work[S] by 1a; == CE end; == At this point the second conjunct has to be concluded. == Since it is an implication we incorporate the proof of the implication == into the main proof. == We are really doing the implication introduction from here on. assume A1: not Save[M]; == What remains to be proven at this point is: not Need[M] 2a: now == II assume A2: Need[M]; 2b: Work[S] & Save[M] by A, A2; == IE thus Save[M] by 2b; == CE end; thus not Need[M] by A1, 2a; == MT end;

The key point to understanding all this is the question:
What remains to be proven in a proof?
It is a formula.
Let us introduce a name for it.
That which still remains to be proven in a proof we call the current
*thesis*.
Initially, right after the `proof`, the current thesis is the original
formula that we are proving.
Each assumption (`assume`) and conclusion (`thus`)
that we make affects the thesis.
The precise explanation of *What is the current thesis?* is pretty
obscure.
Therefore, we will rely more on your intuition.
Assume we are at the beginning of a proof.
The current thesis is the original formula.
If we go through an assumption `assume` then it looks like we
are applying hypothetical reasoning and the current thesis better
be an implication.
After the assumption the current thesis is the consequent of the
previous thesis.
And now, if the current thesis is an implication we may expect
another assumption; if not we have to conclude (`thus`)
whatever remains to be proven.
At any point in a proof you can assume the negation of the current thesis,
which means that you are switching to a proof by contradiction.

MIZAR has been equipped with a special contraption to talk about the current thesis.

We know the fundamental proof structures for propositional formulas. We know also we can use a proof by contradiction. For a conditional formula we can present an indirect reasoning. We know how to structure a proof to get a universally quantified formula.

The previous example will be used to introduce the special formula named
`thesis`.
In a proof, `thesis` denotes the current thesis,
which is the formula that remains to be concluded in order to complete the
innermost proof.
The proof that can always be omitted (section 8.3)
can be then rewritten (although there is no need to write
it in the first place) as:

proof

.

.

.

thusthesisbyReferences

end

Outside of a proof `thesis` must not be used as it is meaningless.
It is quite natural to use `thesis` in hypothetical reasoning.

impliesproof

.==thesisis hereimplies

assume;

.==thesisis here

.

.

thusthesisJustification

.==thesisis herenot contradiction

.==which does not have to be concluded by athus

end

It is quite convenient to use `thesis` in a proof by contradiction,
it may shorten our proofs.

proof

.==thesisis here

assume not thesis;

.==thesisis herecontradiction

.

.

thusthesisJustification

.==thesisis herenot contradiction

.==which does not have to be concluded by athus

end

It is interesting to see the behaviour of `thesis` when
doing universal introduction. Let us look at an example.

environ 1: for p being Person holds Knight[p] implies Wise[p]; 2: for p being Person holds Wise[p] implies Rich[p]; begin for p being Person holds Knight[p] implies Rich[p] proof == UI let P be Person; == thesis <=> Knight[P] implies Rich[P] thus thesis proof == II == thesis <=> Knight[P] implies Rich[P] assume a: Knight[P]; == thesis <=> Rich[P] b: Wise[P] by 1, a; == UE, IE c: Rich[P] by 2, b; == UE, IE thus thesis by c == RE == thesis <=> not contradiction end; == thesis <=> not contradiction end; == The inner proof can be shortened. for p being Person holds Knight[p] implies Rich[p] proof == UI let P be Person; == thesis <=> Knight[P] implies Rich[P] thus thesis proof == II == thesis <=> Knight[P] implies Rich[P] assume a: Knight[P]; == thesis <=> Rich[P] b: Wise[P] by 1, a; == UE, IE thus thesis by 2, b; == UE, IE == thesis <=> not contradiction end; == thesis <=> not contradiction end; == The inner proof can be incorporated entirely. for p being Person holds Knight[p] implies Rich[p] proof == UI let P be Person; == thesis <=> Knight[P] implies Rich[P] == Since the thesis is a conditional we can use == hypothetical reasoning to get it. assume a: Knight[P]; == II == thesis <=> Rich[P] b: Wise[P] by 1, a; == UE, IE thus thesis by 2, b == thesis <=> not contradiction end;

environ given A, B being PERSON; Opp: for a being PERSON holds Knight[a] iff not Knave[a]; == These two statements are a translation of the sentence, said by A, == " I am a knave or B is a knight" A1: Knight[A] implies ( Knave[A] or Knight[B] ); A1': Knave[A] implies not ( Knave[A] or Knight[B] ); begin == The question is what are A and B? == First we argue that A must be a knight. C1: Knight[A] proof assume Contra: not Knight[A]; C1: Knave[A] by Contra, Opp; C2: not ( Knave[A] or Knight[B] ) by C1, A1'; C3: not Knave[A] by C2; C4: Knight[A] by C3, Opp; thus contradiction by C4, Contra; end; == Now we determine what B is. D1: Knight[B] proof S1: Knave[A] or Knight[B] by C1, A1; S2: not Knave[A] by C1, Opp; thus thesis by S1, S2; end;

environ given A, B, C being PERSON; Opp: for a being PERSON holds Knight[a] iff not Knave[a]; == These two are a translation of the sentence, said by A, == "All of us are knaves." A1: Knight[A] implies ( Knave[A] & Knave[B] & Knave[C] ); A1': Knave[A] implies not ( Knave[A] & Knave[B] & Knave[C] ); == These two are a translation of the sentence, said by B, == "Exactly one of us is a knight." B1: Knight[B] implies ( (Knight[A] & Knave[B] & Knave[C]) or (Knave[A] & Knight[B] & Knave[C]) or (Knave[A] & Knave[B] & Knight[C]) ); B1': Knave[B] implies not ( (Knight[A] & Knave[B] & Knave[C]) or (Knave[A] & Knight[B] & Knave[C]) or (Knave[A] & Knave[B] & Knight[C]) ); begin == The question is what are A, B and C? == First we argue that A must be a knave. A2: Knave[A] proof assume Contra: not Knave[A]; 1: Knight[A] by Contra, Opp; 2: Knave[A] by 1, A1; thus contradiction by 2, Contra; end; == A useful sentence: B2: ( (Knight[A] & Knave[B] & Knave[C]) or (Knave[A] & Knight[B] & Knave[C]) or (Knave[A] & Knave[B] & Knight[C]) ) implies not Knave[B] by B1'; == Then we argue that if C is a knight then B must be a knight. C2: Knight[C] implies Knight[B] proof assume S1: Knight[C]; S2: Knave[A] & Knight[C] by S1, A2; S3: not Knave[B] proof assume Contra: Knave[B]; 31: Knave[A] & Knave[B] & Knight[C] by S2, Contra; 32: not Knave[B] by B2, 31; thus contradiction by Contra, 32; end; thus Knight[B] by Opp, S3; end; == Then we argue that if C is a knave then B must still be a knight. C3: Knave[C] implies Knight[B] proof assume S1: Knave[C]; thus Knight[B] proof assume Contra: not Knight[B]; 1: Knave[B] by Opp, Contra; 2: Knave[A] & Knave[B] & Knave[C] by A2, S1, 1; 3: not Knave[A] by A1', 2; thus contradiction by A2, 3; end; end; == A tautology: C4: Knight[C] or not Knight[C]; C5: Knight[C] or Knave[C] by C4, Opp; == No matter what C is, B is a Knight. B3: Knight[B] by C2, C3, C5; C6: Knave[C] by A1, A1', B1, B1', B3, C5; Conclusion: Knave[A] & Knight[B] & Knave[C] by A2, B3, C6;

environ == Opp says that every person is either a Knight or a Knave, but == not both Opp: for a being PERSON holds Knight[a] iff not Knave[a]; == Veracity says that 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] ) begin == Theorem1 says that if some person, p, is a knave then there is at == least one statement s, uttered by p, that is not true == But it does not say that every statement of p is false. Can this == latter assertion be proven with the above environment? Theorem1: for p being PERSON holds Knave[p] implies ( ex s being STATEMENT st Tells[p,s] & not True[s] ) proof let p be PERSON; == We have to prove the implication. assume A1: Knave[p]; == Now we have to prove the consequent. C0: not Knight[p] by A1, Opp; C1: Knight[p] iff ( for s being STATEMENT holds Tells[p,s] implies True[s] ) by Veracity; C2: not ( for s being STATEMENT holds Tells[p,s] implies True[s] ) by C1, C0; C3: ex s being STATEMENT st not ( Tells[p,s] implies True[s] ) by C2; consider t being STATEMENT such that C4: not ( Tells[p,t] implies True[t] ) by C3; C5: Tells[p,t] & not True[t] by C4; thus thesis by C5; end;

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]; == Opp says that every person is either a Knight or a Knave, but == not both. Opp: for a being PERSON holds Knight[a] iff not Knave[a]; == Veracity says that 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] ); == Consistency says that if at least one of the things a person says is == false then everything they 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]) ); begin == Theorem2 says that Fred cannot say hello. Theorem2: not Tells[Fred,Hello] proof == Specialize Fact2 to the statement Hello. C0: Tells[Fred, Hello] implies not True[Hello] by Fact2; thus thesis by C0, Fact1; end; == Theorem3 says that if Fred says nothing at all, then he is a knight! Theorem3: (for s being STATEMENT holds not Tells[Fred,s]) implies Knight[Fred] proof assume A1: (for s being STATEMENT holds not Tells[Fred,s]); C0: for s being STATEMENT holds Tells[Fred,s] implies True[s] proof let s be STATEMENT; C1: not Tells[Fred,s] by A1; thus thesis by C1; end; C2: Knight[Fred] iff ( for s being STATEMENT holds Tells[Fred,s] implies True[s] ) by Veracity; thus thesis by C0, C2; end; == Theorem4 says that if some person, a, is a knave then every == statement s uttered by a is false. Theorem4: for p being PERSON holds Knave[p] implies ( for s being STATEMENT holds Tells[p,s] implies not True[s] ) proof let p be PERSON; == Now we have to prove the implication. assume A1: Knave[p]; == Now we have to prove the consequent. C0: not Knight[p] by A1, Opp; C1: Knight[p] iff ( for s being STATEMENT holds Tells[p,s] implies True[s] ) by Veracity; C2: not ( for s being STATEMENT holds Tells[p,s] implies True[s] ) by C1, C0; C3: ex s being STATEMENT st not ( Tells[p,s] implies True[s] ) by C2; consider t being STATEMENT such that C4: not ( Tells[p,t] implies True[t] ) by C3; C5: Tells[p,t] & not True[t] by C4; C6: ex s being STATEMENT st Tells[p,s] & not True[s] by C5; C7: (ex s being STATEMENT st Tells[p,s] & not True[s]) implies (for s being STATEMENT holds Tells[p,s] implies not True[s]) by Consistency; thus thesis by C6,C7; end;

== Here is the intended interpretation of the predicates Tells, Likes, and == Conspire. == Tells[Person, Statement] - Tells[a,s] means person a tells statement s. == Likes[Person, Person] - Likes[a,b] means person a likes person b. == Conspire[Person, Person, Person] - Conspire[x,y,z] means both x and y == do not like z. environ == These reserve statements save us the trouble of specifying == the sort of the variables being quantified. reserve x, y, z for Person; reserve r, s, t for Statement; given A, B, C, D, E, F, G being Person; given Lie, Promise, Blabla, Insult, Prayer being Statement; a1: for x holds Knave[x] or Knight[x] or Normal[x]; a1': for x holds Knave[x] implies not (Knight[x] or Normal[x]); a1'': for x holds Knight[x] implies not (Knave[x] or Normal[x]); a1''': for x holds Normal[x] implies not (Knight[x] or Knave[x]); a2: for x, y holds Likes[x, y] & Knight[x] implies Knave[y]; a2': for x, y holds Likes[x, y] & Knave[x] implies not Normal[y]; a2'': for x, y holds not Likes[x, y] & Normal[x] implies Knight[y]; a3: for x, y, z holds Conspire[x, y, z] implies not (Likes[x, z] or Likes[y, z]); a3': for x, y, z holds not Likes[x, z] & not Likes[y, z] & not (Likes[z, x] or Likes[z, y]) implies Conspire[x, y, z]; a4: for x, s holds Knight[x] & Tells[x, s] implies True[s] & s <> Insult; a4': for x, s holds Knave[x] & Tells[x, s] implies False[s] or s = Blabla; a4'': for x holds Normal[x] implies Tells[x, Promise]; a5: for x being Person holds Likes[x, D]; a5': not False[Prayer]; a5'': Prayer <> Blabla & Promise <> Blabla; a5''': for x holds Knave[x] implies not Likes[E, x]; a6: Likes[F, G] & Likes[G, F]; a6': Normal[F]; begin Exercise1: not Knave[G] proof 1: Normal[F] by a6'; 2: Likes[G, F] & Knave[G] implies not Normal[F] by a2'; 3: not ( Likes[G, F] & Knave[G] ) by 1, 2; 4: not Likes[G, F] or not Knave[G] by 3; thus not Knave[G] by a6, 4; end; Exercise2: not Conspire[F, F, G] proof 1: Likes[F, G] by a6; 2: Conspire[F, F, G] implies not (Likes[F, G] or Likes[F, G]) by a3; thus thesis by 1,2; end; Exercise3: not Conspire[A, E, D] proof 1: Likes[A, D] by a5; 2: Conspire[A, E, D] implies not (Likes[A, D] or Likes[E, D]) by a3; thus thesis by 1,2; end; Exercise4: not Normal[C] & Tells[C, Promise] implies True[Promise] or False[Promise] proof assume A: not Normal[C] & Tells[C, Promise]; 1: Knave[C] or Knight[C] by A, a1; 2: Knight[C] implies True[Promise] by A, a4; 3: Knave[C] implies False[Promise] by A, a4', a5''; thus thesis by 1,2,3; end; Exercise5: (Likes[E, A] iff Likes[E, B]) & Knave[B] & Normal[E] & Tells[A, Promise] implies True[Promise] proof assume A: (Likes[E, A] iff Likes[E, B]) & Knave[B] & Normal[E] & Tells[A, Promise]; 1: Knave[B] implies not Likes[E, B] by a5'''; 2: not Likes[E, B] by A, 1; 3: not Likes[E, A] by A, 2; 4: Knight[A] by 3, A, a2''; 5: Knight[A] implies True[Promise] by a4, A, a5''; thus thesis by 5, 4; end; Exercise6: Likes[B, A] & Knight[B] & Tells[A, Promise] implies False[Promise] proof 1: Likes[B, A] & Knight[B] implies Knave[A] by a2; 2: Knave[A] & Tells[A, Promise] implies False[Promise] by a4', a5''; thus thesis by 1,2; end; Exercise7: not Tells[D, Promise] implies Knight[D] proof assume A: not Tells[D, Promise]; 1: not Normal[D] by a4'', A; 2: Likes[E, D] by a5; 3: Knave[D] implies not Likes[E,D] by a5'''; 4: not Knave[D] by 2, 3; thus thesis by 1, 4, a1; end; Exercise8: Knave[B] & Knave[C] & Conspire[A, B, E] & Conspire[A, C, E] implies Conspire[B, C, E] proof assume A: Knave[B] & Knave[C] & Conspire[A, B, E] & Conspire[A, C, E]; 1: not Likes[E, B] & not Likes[E, C] by A, a5'''; 2: not Likes[B, E] by a3, A; 3: not Likes[C, E] by a3, A; thus thesis by 1, 2, 3, a3'; end; Exercise9: Conspire[D, A, E] & Tells[E, Insult] implies not (Normal[D] & Normal[A]) proof assume A: Conspire[D, A, E] & Tells[E, Insult]; 1: not Likes[D, E] & not Likes [A, E] by A, a3; 2: Knight[E] implies Insult <> Insult by A, a4; 3: not Knight[E] by 2; 4: not Normal[A] by a2'', 1, 3; 5: not Normal[D] by a2'', 1, 3; thus thesis by 4, 5; end; Exercise10: Tells[A, Prayer] & not Tells[A, Blabla] & not Tells[A, Promise] implies Knight[A] proof assume A: Tells[A, Prayer] & not Tells[A, Blabla] & not Tells[A, Promise]; 1: not False[Prayer] & not ( Prayer = Blabla ) implies not (Knave[A] & Tells[A,Prayer]) by a4'; 2: not Knave[A] or not Tells[A, Prayer] by 1, a5', a5''; 3: not Knave[A] by 2, A; 4: not Normal[A] by a4'', A; thus thesis by 3, 4, a1; end;