 If a system \(\mathbf{S}\) is complete for an interpretation, in the sense that every formula which is valid under the interpretation is provable in \(\mathbf{S},\) then an indirect way to show that a formula (or schema) is provable in \(\mathbf{S}\) is to establish its validity under the interpretation. Completeness does not always accompany soundness; for instance, Heyting arithmetic is sound but incomplete for the realizability interpretation described in Section 5.2 below. 