Definition by cases

An expression defined by cases is of the form if P then TelseU, 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 Telse 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.