On finite models for the equivalence (with C.S.Scholten)

On finite models for the equivalence

The equivalence, denoted by $\equiv$ , is postulated to be reflexive, symmetric, and associative, i.e. we have for all $X, Y$ , and $Z$

(0) $[X \equiv X]$

(reflexive)

(1) $\left[(X \equiv Y) \equiv (Y \equiv X)\right]$

(symmetric)

(2) $\left[(X \equiv Y) \equiv Z\right] \equiv (X \equiv (Y \equiv Z))$ .

(associative).

On account of the associativity, we feel free to omit the semantically irrelevant parenthesis pairs.

With $\left\lbrack {A \equiv B}\right\rbrack$ denoting the equality of the expressions

(3) $[X \equiv X \equiv Y \equiv Y]$

parsing (3) as $\left\lbrack {X \equiv \left( {X \equiv \left( {Y \equiv Y}\right) }\right) }\right\rbrack$ we see

that $\left( {Y \equiv Y}\right)$ is a right identity element of $\exists$ ;

parsing (3) as $\left\lbrack {\left( {\left( {X \equiv X}\right) \equiv Y}\right) \equiv Y}\right\rbrack$ we see

that $\left( {X \equiv X}\right)$ is a left identity element of $\equiv j$

parsing (3) as $\left\lbrack {\left( {X \equiv X}\right) \equiv \left( {Y \equiv Y}\right) }\right\rbrack$ we see

that these identity elements are the same. (Not

surprisingly so.) In the sequel we shall denote the identily element of the equivalence by 0.

Theorem The number of distinct values in a finite model for the equivalence is a power of 2.

(The theorem is well-known; this note is written because we like the following argument.)

Since the Theorem holds for the trivial model consisting of only one value - viz. 0 - we concentrate our attention on the nontrivial models, i.e. those with more values. The Theorem now follows from the following Lemma. The values of a nontrivial finite model for the equivalence can be partitioned into two disjoint sets E and O such that

(i) $E$ and $O$ are of equal size, and (ii) the elements of $E$ provide a model for the equivalence.

Proof of Lemma 0. We shall prove Lemma 0 by showing how for a given nontrivial finite model the partitions E and O can be constructed. To begin with, we select an arbitrary element different from 0 and call it 1 . With this choice we introduce a pairing by

$$ (X \mathrm {a n d} Y \mathrm {a r e p a i r e d}) \equiv [ X \equiv 1 \equiv Y ] $$

Note that

(i) 0 and 1 are paired (ii) each element $z$ is paired to $z \equiv 1$ (iii) no element is paired to itself $\left\lbrack {2 \equiv 1 \equiv 2}\right\rbrack$ would lead to $\left\lbrack {0 \equiv 1}\right\rbrack$ ,contradicting that 1 has been chosen different from 1

From the pairing we conclude that the given model

consists of an even number of values.

The idea of the construction is to initialize both E and O to the empty set:

$$ E, O := \phi , \phi $$

and to deal with the pairs in turn, adding one of its elements to E and the other to O, the choice (possibly) being constrained by the invariant. In order to formulate the invariant we introduce the predicate comp , given by

$$ c o m p. V. Z \equiv e l e m e n t Z e q u i v a l e s t h e (c o n t i n u e d) $$

$$ e q u i v a l e n c e o f s o m e e l e m e n t s f r o m V ^ {\prime \prime} $$

from which

(4) $\operatorname{comp.}V. \land \operatorname{comp.}V. \Rightarrow \operatorname{comp.}V.\left( {X \equiv Y}\right)$

p follows. From (4) follows -with ${X}{1}{Y}{1}V\;\left( {{2,2} \equiv 1,E}\right)$

(5) $\neg \operatorname{comp}.E.1 \Rightarrow \neg \operatorname{comp}.E.2 \vee \neg \operatorname{comp}.E.\left( {Z \equiv 1}\right) ,$

and the construction main wins

P : 7 comp. E. 1

initially true since $E = \phi \Rightarrow P$

Consider now the next pair to be dealt with: calling one element $Z$ ,the other element is $Z = 1$ . Under validity of $P$ we have an account of (5)

$$ \lnot c o m p. E. Z \lor \lnot c o m p. E. (Z \equiv 1) $$

CSS 118 /EWD967-3

and hence it is possible to make the choice which of the elements of the pair to call 2 in such a way as to ensure

(6) $\neg \operatorname{comp}.E.\left( {Z \equiv 1}\right)$

Since

$$ \lnot c o m p. E. 1 \land \lnot c o m p. E. (2 \equiv 1) \Rightarrow \lnot c o m p. (E \cup {2 }). 1, $$

with 2 satisfying (6)

$$ E, O := E \cup {2 }, O \cup {2 \leq 1 } $$

mainains

Upon completion, we have

(7) $\left( {A{X}{1}{Y}{1} : X \in E \land {Y}_{1} \in E : \left( {X \equiv Y}\right) \in E}\right)$

because we have for any $X$ and $Y$

$$ X \in E \land Y \in E $$

$$ \begin{array}{l} \Rightarrow {\mathrm {d e f i n i t i o n o f c o m p . i n p a r t i c u l a r} Z \in V \Rightarrow \mathrm {c o m p . V . Z} } \ c o m p. E. X \wedge c o m p. E. Y \ \Rightarrow {(4) \mathrm {w i t h} V := E } \ c o m p. E. (X \equiv Y) \ \Rightarrow {P a n d (5), w i t h Z := X \equiv Y } \ \mathrm {t} \mathrm {c o m p . E .} (X \equiv Y \equiv 1) \ \Rightarrow {\mathrm {d e f i n i t i o n o f c o m p} } \ \lnot ((X \equiv Y \equiv 1) \in E) \ = {X \equiv Y \equiv 1) \in E \cup O } \ (X \equiv Y \equiv 1) \in O \ = {\mathrm {c o n s t r u c t i o n o f} E \mathrm {a n d} O } \ \end{array} $$

$$ (X \equiv Y) \in E $$

And (7) says that the elements of $E$ provide a model for the equivalence.

(End of Proof of Lemma 0.)

Undoubtedly, the above presentation leaves room for editorial improvements (for which we currently lack the opportunity), but we do like the argument.

An alternative argument shows

(i) the existence of a model of size ${2}^{0}$ (ii) from the existence of a model of size ${2}^{n}$ that the next finite model is of size ${2}^{n + 1}$ .

Lemma 0 , however, enables us to carry out the induction step without any reference to powers of 2 .

Furthermore, the argument provides a nice example of how nondeterministic algorithms can be used to avoid case analysis: requirement (6) may or may not prescribe the choice of $Z$ ,but this distinction no longer surfaces in our argument.

Nuenen, 19 July 1986

cIrs. C. S. Scholten

Klein Paradips 4

7361 TD BEEKBERGEN

The Netherlands

prof. dr. Edsger W. Dgksta

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712- 1188

United States of America