# 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