diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index 34a9dbfcce8ff62313a92ff8f9b7a0794982a526..5cf32a73a32880cd5af92c653d928513d06bf447 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -352,7 +352,9 @@ Second, a proof of a weakest precondition with any postcondition should imply th
 \end{enumerate}
 \end{defn}
 
-To express the adequacy statement for functional correctness, we assume that the signature $\Sig$ adds a predicate $\pred$ to the logic which reflects the set $V$ of legal return values into the logic:
+To express the adequacy statement for functional correctness, we assume that the signature $\Sig$ adds a predicate $\pred$ to the logic:
+\[ \pred : \Val \to \Prop \in \SigFn \]
+Furthermore, we assume that the \emph{interpretation} $\Sem\pred$ of $\pred$ reflects some set $V$ of legal return values into the logic (also see \Sref{sec:model}):
 \[\begin{array}{rMcMl}
   \Sem\pred &:& \Sem{\Val\,} \nfn \Sem\Prop \\
   \Sem\pred &\eqdef& \Lam \val. \Lam \any. \setComp{n}{v \in V}