__"I have a proof that...."__

This is about an observation of a type that I don't particularly like to make, but once the observation has been made, it had better be recorded. In the following, `A` and `B` stand for propositions for which I may have a proof.

Consider statements `a`0 and `a`1:

(`a`0) I have a proof that __true__ (holds)

(`a`1) __true__ (holds) .

Then, `a`0 and `a`1 are equivalent. (Since —by definition— the proof that __true__ (holds) is empty, it is impossible not to have it.)

Consider statements `b`0 and `b`1:

(`b`0) I have a proof that __false__ (holds)

(`b`1) __false__ (holds) .

Then `b`0 and `b`1 are equivalent. (Since —by definition— the proof that __false__ (holds) does not exist, it is impossible to have it.)

From the above we conclude by case analysis the equivalence of `c`0 and `c`1:

(`c`0) I have a proof that I have a proof that `A` (holds)

(`c`1) I have a proof that `A` (holds) .

Consider statements `d`0 and `d`1:

(`d`0) I have a proof that `A`∧`B` (holds)

(`d`1) I have a proof that `A` (holds) and I have a proof that `B` (holds) .

Then `d`0 and `d`1 are equivalent. (Well, that is what "∧" (="and") means.)

This last law can be generalized to universal quantification. Consider statements `e`0 and `e`1 (in which the range for `n` is implicitly understood):

(`e`0) I have a proof that, for all `n`, `A`.`n` (holds)

(`e`1) For all `n`, I have a proof that `A`.`n` (holds) .

Then e0 and e1 are equivalent.

__Remark__: As a result it is semantically irrelevant that the sentence "I have a proof of `A`.`n` for all `n`" is syntactically ambiguous. (End of remark.)

Consider the statements `f`0 and `f`1:

(`f`0) If I have a proof that `A` (holds) then I have a proof that `B` (holds)

(`f`1) I have a proof that, if I have a proof that `A` holds, then `B` (holds)

Then `f`0 and `f`1 are equivalent. (If I don't have a proof that `A` (holds), `f`0 and `f`1 are both "vacuously" __true__; if I do have a proof that `A` (holds), both `f`0 and `f`1 reduce to "I have a proof that `B` (holds)".)

__Remark__: As a result it is semantically irrelevant that the sentence "I have a proof that `B` holds if I have a proof of `A`." is syntactically ambiguous. (End of remark.)

But consider now statements `g`0 and `g`1:

(`g`0) I have a proof that `A` ∨ `B` (holds)

(`g`1) I have a proof that `A` (holds) or I have a proof that `B` (holds) or I have both proofs.

In this case, the two statements are not equivalent: `g`1 implies `g`0, but it is in general not the other way round.

`* *
*`

Let us now do away with all the above verbosity and abbreviate "I have a proof that `A` (holds)" to "[`A`]". Our laws about having proofs can then be summa rized as follows:

(a) [__true__] ≡ __true__

(b) [__false__] ≡ __false__

(c) [[`A`]] ≡ [`A`]

(d) [`A` ∧ `B`] ≡ [`A`] ∧ [`B`]

(e) [〈∀n :: `A`.`n`〉] ≡ 〈∀`n` :: [`A`.`n`]〉

(f) [`A`] ⇒ [`B`] ≡ [[`A`] ⇒ `B`]

(g) [`A` ∨ `B`] ⇐ [`A`] ∨ [`B`]

The moral of the story is that "I have a proof that..." has all the algebraic properties of the "everywhere" operator, i.e. of universal quantification over a non-empty domain (see [DS90]).

[DS90] Dijkstra, Edsger W. and Scholten, Carel S., *Predicate Calculus and Program Semantics*, Springer-Verlag, New York, 1990.

Austin, 15 October 1995

Prof. Dr. Edsger W. Dijkstra

Department of Computer Sciences

The University of Texas at Austin,

Austin, TX 78712-1188

USA

Transcription by Mikhail Esteves.

Last revised on