Thread: Prove it's well-defined

Hi,

How can you prove that an operation is well-defined, for instance: the sum of two congruence classes?

Thanks in advance.

The need to prove that an operation is well-defined arises when not all steps or elements of the operation are uniquely identified and precisely described. For example, when the definition says, "take the minimum of this set," we must know that the minimum exists. Moreover, in a partially ordered set (such as a collection of subsets ordered by inclusion) there can be several minimums, so taking "the" minimum raises a problem.

Let [a] denote the equivalence class of a modulo some n. The sum of two classes [a1] + [a2] is usually defined as [a1 + a2]. However, addition has to be defined on classes, not on classes with chosen representatives. Therefore, given a class, one has to choose a representative first, and it is not clear a priori that the result of the sum does not depend on the representatives.

One of the potential problems with nondeterministic choice is the violation of the equality axiom:

For any property A and any x, y, x = y and A(x) imply A(y).

Fix some numbers a1, a1' and a2 such that a1 ≡ a1' (mod n), i.e., [a1] = [a1']. Then by definition, [a1] + [a2] = [a1 + a2], so the equality axioms says that [a1'] + [a2] = [a1 + a2]. However, the definition says that [a1'] + [a2] = [a1' + a2]. For the equality axiom to be true, one must show a1 + a2 ≡ a1' + a2 (mod n).