Consider Ortholattices (OL). (The same remarks hold for OML, MOL, and BA.) We started with an equational basis B1 in terms of join, meet, and complement. To show that a set of equations B2 in terms of the Sheffer stroke is a basis for OL, we showed that B1 is definitionally equivalent to B2, using the standard definitions.

This section is a summary of our view of definitional equivalence.

An *equational definition* has the form

f(x1,x2,...,xn) = alphawhere

- the
`x`i's are all distinct variables, -
`alpha`is a term not containing`f`, and - all of
`alpha`'s variables are among`{x1,x2,...,xn}`.

If we have a theory T, and if we add a definition of a new operation, say `f`,
we get a definitional extension of T, say T'. The important property
of T' is that if we have a statement S not involving `f`,
we can prove S in T iff we can prove S in T'; that is, T' is a conservative extension
of T.

Two theories T1 and T2 are *definitionally equivalent* if each has
a definitional extension, say T1' and T2', such that T1' and T2' are equivalent.

For example, consider the two theories

T1 | T2 ----------------------------------------|---------------------------- c(c(x) v y) v x = x. | f(x,y) = f(y,x). c(c(x) v y) v (z v y) = y v (z v x). | f(f(x,y),f(x,f(y,z))) = x. ----------------------------------------|----------------------------Extend each theory by defining the operations in the other theory.

T1' | T2' ----------------------------------------|---------------------------- c(c(x) v y) v x = x. | f(x,y) = f(y,x). c(c(x) v y) v (z v y) = y v (z v x). | f(f(x,y),f(x,f(y,z))) = x. | f(x,y) = c(x) v c(y). | x v y = f(f(x,x),f(y,y)). | c(x) = f(x,x). ----------------------------------------|----------------------------If we can show the extended theories to be equivalent, then we have shown T1 and T2 to be definitionally equivalent.

Note that it is not sufficient to prove (T1' => T2) and (T2' => T1). We must prove the definitions in the other theory as well the axioms.

In this example, T1 and T2 are definitionally equivalent:
T1 is Boolean algebra in terms of join and complement, and
T2 is Boolean algebra in terms of the Sheffer stroke.
*The proofs are difficult!*