A /\ B == A == B == A \/ BAnd 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 == Rwe 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)
First we rewrite (2) in a form that is sometimes easier to use:
(3) !P \/ !Q \/ !RThere are three ways to rewrite this as an implication:
(4) P => !Q \/ !Rand 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 /\ Rand (5) follows by contradiction.
Of course we can rephrase (5) as
(6) !Q \/ !RFinally 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 /\ !RWith the above properties it is very easy to do calculational proofs on trilemmas.
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