 As Sundholm (1983: 159) points out, in the terms “BHK-Interpretation” and “Proof Interpretation” it would be appropriate to replace “Interpretation” by “Explanation”. For in a logical-mathematical context, “interpretation” has come to refer to the interpretation of one formal theory in  another.[1]  An interpretation of a formal system \(U\) in a formal system \(V\) is given by a translation \('\) of formulas of \(U\) to formulas of \(V\) that preserves  provability:[2]