Calculating with Partitions

In the book of Chandy & Misra [CM88], I found an interesting consequence of three variables of which exactly one is true. To begin with, such a relation can be formalized as follows:

(0)	[ x ∨ y ∨ z ]
(1)	[ ¬(x ∧ y) ]
(2)	[ ¬(x ∧ z) ]
(3)	[ ¬(y ∧ z) ]

Note

Before proceeding with the interesting fact, let's have a closer look at the square brackets. They come from the book of Dijkstra & Scholten and they constitute a form of implicit universal quantification. If x, y and z are normal boolean variables, it can be omitted. However if they are predicates ([DS90] introduces them as boolean structures), you can leave out their arguments and it is considered that they are universally quantified over. In such a case,

	[ x ∨ y ∨ z ]

would be equivalent to

	〈∀ i:: (x ∨ y ∨ z).i〉 

and predicate application is considered to distribute over the logical connectives so it is, in turn equivalent to

	〈∀ i:: x.i ∨ y.i ∨ z.i〉 

Since i doesn't play a role in our manipulations, it simplifies the formula and our work to leave it out.

This means that, if x, y and z are the characteristic predicate of sets X, Y, Z, our set of constraint states that they partition the type over which they range.

(end of note)

Now the interesting consequence is this one:

(4)	[ ¬x  ≡  y ∨ z ]

Its proof is nice and simple. The usual heuristics to design a proof of such a theorem is either to manipulate the whole formula or to transform one side into the other. Since we don't have rules to relate either of y or z to ¬x, we choose to manipulate the whole formula. Also, we need to join ¬x and y ∨ z with either a disjunction or a conjunction because of the shape of the rules that we have. The golden rule, stated below, is a good candidate to achieve just that.

(5)	[ x ∨ y ≡ x ≡ y ≡ x ∧ y ]	("Golden rule")

For those unfamiliar with the rule, they can convince themselves of the validity or the rule by seeing that x ⇒ y can be equivalently formulated as follows:

	x  ≡  x ∧ y
	x ∨ y  ≡  y

By transitivity, they are equivalent. Hence, the golden rule. Now for the proof of (4):

	  ¬x  ≡  y ∨ z
	=   { ¬ over ≡ to get ¬ out of the way }
	  ¬(x  ≡  y ∨ z)
	=   { Golden rule }
	  ¬(x ∧ (y ∨ z)  ≡  x ∨ y ∨ z)
	=   { (0) }
	  ¬(x ∧ (y ∨ z))
	=   { ∧ over ∨.  It acheives the
	      grouping of (1) to (3) }
	  ¬( (x ∧ y) ∨ (x ∧ z) )
	=   { ¬ over ∨ }
	  ¬(x ∧ y) ∧ ¬(x ∧ z)
	=   { (1) and (2) }
	  true

This simple proof is six step and it carries an inactive negation around needlessly. We could remove one step and the noise of the negation if we simply realize that

	¬(x  ≡  y)  ≡  x  ≢  y

Also, we can use the golden rule over ≢ if we realize that replacing an even number of ≡ by ≢ in a sequence of equivalences leaves the truth value unchanged.

	  x  ≢  y ∨ z
	=   { Golden rule }
	  x ∧ (y ∨ z)  ≢  x ∨ y ∨ z
	=   { (0) }
	  ¬(x ∧ (y ∨ z))
	=   { ∧ over ∨ }
	  ¬((x ∧ y) ∨ (x ∧ z))
	=   { ¬ over ∨ }
	  ¬(x ∧ y) ∧ ¬(x ∧ z)
	=   { (1) and (2) }
	  true

It is nicer this way: the proof is shorter and ¬ is inactive only for one step. We can suppose that it can be generalized to more variables. Indeed, (0) to (3) can be generalized by (6) and (7) and we can replace x, y, z by x.i for any appropriate i.

(6) [〈∃ i:: x.i〉 ]
(7) [〈∀ i,j: i ≠ j: ¬(x.i ∧ x.j)〉 ]

A first attempt at generalizing (4) might yield

(4')	[ x.j  ≢ 〈∃ i: i ≠ j: x.i〉 ]

but we can do better. We don't need to only have on variable on the left hand side of ≢, we could have many, like on the right hand side. The important thing is that variables appear on exactly one side. To formalize this, we can use an arbitrary separating predicate P. The x.i such that P.i holds will be on the left and the others will be on the right.

(4'')	[〈∃ i: P.i: x.i〉 ≢〈∃ i: ¬P.i: x.i〉 ]

Notice how nicely symmetric (4'') is. The same technique can be used to prove it as what we used for (4).

	 〈∃ i: P.i: x.i〉 ≢〈∃ i: ¬P.i: x.i〉 
	=   { Golden rule }
	   〈∃ i: P.i: x.i〉 ∧〈∃ i: ¬P.i: x.i〉 
	  ≢〈∃ i: P.i: x.i〉 ∨〈∃ i: ¬P.i: x.i〉 
	=   { ∧ over ∃ and nesting; merge ranges }
	 〈∃ i,j: P.i ∧ ¬P.j: x.i ∧ x.j〉 ≢〈∃ i:: x.i〉 
	=   { (6) }
	  ¬〈∃ i,j: P.i ∧ ¬P.j: x.i ∧ x.j〉 
	=   { ¬ over ∃ }
	 〈∀ i,j: P.i ∧ ¬P.j: ¬(x.i ∧ x.j)〉 
	⇐  { P.i ∧ ¬P.j ⇒ P.i ≠ P.j and the 
	      contrapositive of Leibniz's
	      principle applies }
	 〈∀ i,j: i ≠ j: ¬(x.i ∧ x.j)〉 
	=   { (7) }
	  true

Our next investigation is whether or not (4'') is sufficient to characterize the kind of partition defined by (6) and (7). To do so, we prove that (4'') ≡ (6) ∧ (7). Mutual implication is an intesting choice of strategy since half of the work is already done and we only have a weaker proof obligation to take care of. We can prove (6) and (7) separately under the assumption of (4'')

Proof of (6)

	 〈∃ i:: x.i〉 
	≠   { (4'') with P.i ≡ true }
	 〈∃ i: false: x.i〉 
	=   { Empty range }
	  false

For the proof of (7), we have to notice the formal differences between (7) and one of the sides of (4''). First of all, (7) has more dummies and has a universal quantification instead of an existential one. Second, the term of the quantification has two (negated) occurrences of x rather than just one positive one. What we must do is split the dummies between two quantifications --nesting should do nicely--, then move the second x term out of the inner quantification and use one of the negations to change the ∀ into ∃. The formula should then be amenable to an application of (4'').

Proof of (7)

	 〈∀ i,j: i ≠ j: ¬(x.i ∧ x.j)〉 
	=   { Nesting to separate the dummies }
	 〈∀ i::〈∀ j: i ≠ j: ¬(x.i ∧ x.j)〉 〉 
	=   { ¬ over ∧ then ∨ over ∀ to keep only one
	      x term inside the inner quantification }
	 〈∀ i::〈∀ j: i ≠ j: ¬x.j〉  ∨ ¬x.i〉  
	=   { ¬ over ∃ }
	 〈∀ i:: ¬〈∃ j: i ≠ j: x.j〉  ∨ ¬x.i〉  
	=   { Now we have the shape we were looking for
	      we can use (4'') with P.i  ≡  i = j }
	 〈∀ i::〈∃ j: i = j: x.j〉  ∨ ¬x.i〉  
	=   { One point rule }
	 〈∀ i:: x.i ∨ ¬x.i〉  
	=   { Excluded middle and identity of ∀ }
	  true

Luckily enough, after the application of (4''), the steps are of the kind "there is only one thing to do". Without context, the rest of the proof could look like a giant rabbit but, since (4'') is the main part of the rules that we can apply, it is reasonable to expect that we should create an opportunity to apply it and each step before its application bridges the formal difference between the two.

The above proof has been presented as a nice example that an elegant proof can be designed using only the properties of the formulae rather than their interpretation and to present some more advanced heuristics to do so.

The investigation has been prompted by my delight at seeing how nicely the first parts of the problem were solved using the golden rule but the decision to show the proof was taken because of my surprise at how easily the last proof came to me with a simple analysis of the formal differences between the two main formulae although I had expected it to keep me busy for a long time.

Simon Hudon
March 8th, 2011
Meilen

References

[CM88] K. Mani Chandy and Jayadev Misra, Parallel Program Design:
       A Foundation, Addison-Wesley, 1988

[DS90] Edsger W. Dijkstra and Carel S. Scholten, Predicate Calculus
       and Program Semantics, Texts and Monograph in Computer
       Science, Springer Verlag New York Inc., 1990