Trilemmas

While working on [The Mysterious Lock of Monte Carlo] it was necessary to express a trilemma, i.e., a statement that 'exactly one of P, Q, and R is true'. Here is a rather elegant formalization of that statement.

Definition

We know from the properties of the == operator that it is associative, so that we can unambiguously write statements like

 A /\ B == A == B == A \/ B

And since == is also symmetric, we can even reorder the expressions in any order we like.

Such a 'chain' of equivalences is true iff an even number of the expressions is false: it is true if all expressions are true, and every two false expressions can be replaced by a true one.

So by stating that

 (1)  P == Q == R

we are saying that either two or none of P, Q, and R are false. Or conversely that one or three of P, Q, and R are true. For our trilemma we do not want P, Q, and R to be all true, so we need to add one other condition:

 (2)  !(P /\ Q /\ R)

This gives us a nice symmetric definition of a trilemma:

 exactly one of P, Q, and R is true == (P == Q == R) /\ !(P /\ Q /\ R)

Properties

By the above definition (1) and (2) hold for any trilemma. But we can prove more properties.

First we rewrite (2) in a form that is sometimes easier to use:

 (3)  !P \/ !Q \/ !R

There are three ways to rewrite this as an implication:

 (4)  P => !Q \/ !R

and the two symmetric variants.

Next we prove that any two of the parts of the trilemma (say Q and R) are never simultaneously true:

 (5)  !(Q /\ R)

and the two symmetric variants. Proof:

   !(Q /\ R)
==   "logic: distribution, preparing for (4)"
   !Q \/ !R
<=   "(4)"
   P
==   "(1)"
   Q == R
<=   "logic: weakening, to establish contradiction"
   Q /\ R

and (5) follows by contradiction.

Of course we can rephrase (5) as

 (6)  !Q \/ !R

Finally we will show a weaker way to express one of the parts of the trilemma in the others:

   P
==   "(1)"
   Q == R
==   "logic: golden rule, preparing for (5)"
   Q \/ R == Q /\ R
==   "Q /\ R == false, by (5)"
   !(Q \/ R)

So we conclude that

 (7)  P == !(Q \/ R)

or the slightly rewritten

 (8)  P == !Q /\ !R

With the above properties it is very easy to do calculational proofs on trilemmas.

This page is brought to you by Marnix Klooster, and is part of his home page. Feel free to e-mail me with comments on the form and content of this page.

Changes to calc/calc-tri.html:

Sat Oct 30 12:38:39 MEST 2004  Marnix Klooster
  * Move from CVS to darcs: do not show the CVS date anymore.

Thu Feb  7 19:43:35 MET 2002  marnix
  * Updated all files to use the m4 template

Wed Sep  5 21:20:00 MEST 2001  marnix
  * Made explicit that last changed date is in GMT

Wed Sep  5 21:08:51 MEST 2001  marnix
  * Now 'last changed' is on its own line

Wed Sep  5 10:10:47 MEST 2001  marnix
  * Added date last changed

Wed Sep  5 08:50:24 MEST 2001  marnix
  * Initial revision