Notes on Definitional Equivalence

Back to the Main Page

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) = alpha
where
  1. the xi's are all distinct variables,
  2. alpha is a term not containing f, and
  3. 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!