The notions of soundness and completeness both express relationships between the formal theory (or proof system) itself and the models of that theory. Informally, soundness means that if we can show by equational logic that t = t' is a theorem then the the realisations of t and t' within the algebra will be identified. We showed in section 5.1 that the terms add(succ(zero),succ(succ(zero))) and succ(succ(succ(zero))) were equal by successive application of the equations
Within the algebra |Num|, each of these terms is mapped onto 3. If it is generally true that terms in the same equivalence class have the same denotation in the algebra, then the proof system is sound with respect to that algebra. This is what we would expect and is usually not hard to achieve.
Completeness, on the other hand, is more elusive. If a proof system is complete with respect to an algebra, then every pair of terms which have the same denotation in the algebra must form a theorem in the logic. The incompleteness of our theory can be illustrated by considering the following true statement about natural numbers:
Within the equations E there is no substitution or sequence of
substitutions we can make which will eventually arrive at this
statement; or, in other words, the statement is not a theorem of the
logic. We can prove it if we are allowed to use inductive
methods or case analysis. The reasoning might be something like this:
consider the case where the LHS is true; then by recursive application
of the equations it must reduce to
greaterthan(succ(X), zero) for some X. If we now consider
lessthan(zero,succ(X)), the RHS, we find that this also is true.
The same argument can be applied to the case when the LHS is false.
But the result cannot be proved in equational logic without resort to
these means; the theory is incomplete.
Another example of an unprovable truth is the statement
the commutative law of addition. The only way that this can be a theorem of the logic is if it is added it to the set E of equations, in which case it is axiomatically true. But it is not provable from the theory as it stands. Gödel's Theorem states formally that it is not possible to construct a finitely axiomatized theory of numbers which is complete (though we could do a lot better than this).