Both answers are correct. Soundness in general means “nothing bad happens”. In the context of equational theories, the following would be *sound* phenomena: 1. A theory is sound (with respect to a given semantics) if derivable equalities are true. 2. An equality-checking algorithm is sound if it accepts only derivable equalities. To see why these are soundness phenomena, think about what happens in the opposite case: a theory derives a false equality, or an algorithm accepts an underivable equality. Soundness on its own is easy to achieve, consider an empty theory, or an algorithm that rejects all equalities. Completeness in general means "as good as it gets". In the context of equational theories, the following would be complete phenomena: 1. A theory is complete (with respect to a given semantics) if it derives all true equations. 2. An equality-checking algorithm is complete if it accepts all derivable equalities. Completeness on its own is easy to achieve, consider a theory that derives all equalities, or an algorithm that accepts all equalities. Soundness and completeness balance each other out. With regards to the question, we can think in terms of theories or in terms of an equality-checking algorithm. In terms of theories and semantics based on normal forms, we think of the normal form `nf(t)` as the meaning of `t`. (For example, in a nice enough theory, the normal form of a closed term of type `nat` will be a numeral, i.e., a canonically represented natural number.) Under this view: * the theory is *sound* (with respect to normal-form-semantics) if derivability of `t ≡ u` implies `nf(t) = nf(u)`, * the theory is *complete* if `nf(t) = nf(u)` implies `t ≡ u`. On the other hand, an equality-checking algorithm based on normal forms accepts `t ≡ u` if the normal forms `nf(t)` and `nf(u)` are syntactically equal. Under this view: * the algorithm is *sound* if `nf(t) = nf(u)` implies that `t ≡ u` is derivable, * the algorithm is *complete* if derivability of `t ≡ u` implies `nf(t) = nf(u)`.