An expression defined by cases is of the form **if** *P* **then** *T***else***U*, which takes the value *T* if the
proposition *P* is true and the value *U* if the proposition *P* is
false. This is the notation we will use in this section: the Watson
notation is `P || T , U`.

Any term may appear in the role of *P*; we adopt Frege's convention
that any object not equal to the truth value **true** is understood
to play the role of the truth value **false** where a proposition is
expected. We refer to *P* as the *hypothesis* of the
expression, and to *T* and *U* as its *branches* (positive and
negative, respectively).

We present the axioms of definition by cases supported by Watson. Notice that equality appears as a term-forming operation as well as in the role of a predicate here; it should be clear what is meant by each instance of the symbol once this is understood.

**hypotheses are propositions:**- (
**if***P***then***T***else***U*) = (**if***P*=**true****then***T***else***U*) **equations are propositions:**- (
*A*=*B*) =**if***A*=*B***then****true****else****false** **truth value roles:***T*=**if****true****then***T***else***U*;*U*=**if****false****then***T***else***U*.**special equations:**- (
*A*=*A*) =**true**;(

**true**=**false**) =**false**. **case distribution:***A*[(**if***P***then***T***else***U*)/*x*] = (**if***P***then***A*[*T*/*x*]**else***A*[*U*/*x*]).**application of hypothesis:**- (
**if***A*=*B***then***C*[*A*/*x*]**else***U*) = (**if***A*=*B***then***C*[*B*/*x*]**else***U*)

These axioms, together with the axioms of equational reasoning above, are sufficient to interpret the logic of propositional connectives and identity. This has been demonstrated using the prover; it is also explained in an unpublished paper [14] of Holmes available on the Web.

This logic of case expressions will probably not be familiar to the reader, but it should at least be clear that the axioms are true. To see that they are sufficient to support propositional logic and the logic of identity requires a little work.