diff --git a/algebra/upred.v b/algebra/upred.v
index 392e5077907b8b600da4a1abb76c8d32ec3d6f26..096ca4dd2c33899bc0a52fd387b04ac22dfa8901 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1481,7 +1481,7 @@ Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
 Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ★ Q.
 Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
 
-(* Soundness results *)
+(** Consistency and adequancy statements *)
 Lemma adequacy φ n : (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) (■ φ)) → φ.
 Proof.
   cut (∀ x, ✓{n} x → Nat.iter n (λ P, |=r=> ▷ P)%I (■ φ)%I n x → φ).
@@ -1492,11 +1492,11 @@ Proof.
   eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
 Qed.
 
-Corollary soundnessN n : ¬ (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) False).
+Corollary consistencyModal n : ¬ (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) False).
 Proof. exact (adequacy False n). Qed.
 
-Corollary soundness : ¬ (True ⊢ False).
-Proof. exact (adequacy False 0). Qed.
+Corollary consistency : ¬ (True ⊢ False).
+Proof. exact (consistencyModal 0). Qed.
 End uPred_logic.
 
 (* Hint DB for the logic *)
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 9039a5af378487896baebb65a87d3a51d576efd7..f6fbcc5bd2a02ccd2ab07d980499b1a609dfc497 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -393,14 +393,18 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
 {\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}
 \end{mathpar}
 
-\subsection{Soundness}
+\subsection{Consistency}
 
-The soundness statement of the logic reads as follows: For any $n$, we have
+The consistency statement of the logic reads as follows: For any $n$, we have
 \begin{align*}
-  \lnot(\TRUE \vdash (\upd\later)^n \FALSE)
+  \lnot(\TRUE \proves (\upd\later)^n\spac\FALSE)
 \end{align*}
 where $(\upd\later)^n$ is short for $\upd\later$ being nested $n$ times.
 
+The reason we want a stronger consistency than the usual $\lnot(\TRUE \proves \FALSE)$ is our modalities: it should be impossible to derive a contradiction below the modalities.
+For $\always$, this follows from the elimination rule, but the other two modalities do not have an elimination rule.
+Hence we declare that it is impossible to derive a contradiction below any combination of these two modalities.
+
 
 %%% Local Variables:
 %%% mode: latex
diff --git a/docs/model.tex b/docs/model.tex
index 8767494c21c21c0b032dee6554538fe8890c1481..41b545ca2b4d060157c6b5238edd736e40620bd0 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -110,10 +110,11 @@ n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\rs)
 \end{aligned}
 \]
 
-The following theorem connects syntactic and semantic entailment:
+The following soundness theorem connects syntactic and semantic entailment.
+It is proven by showing that all the syntactic proof rules of \Sref{sec:base-logic} can be validated in the model.
 \[ \vctx \mid \prop \proves \propB \Ra \Sem{\vctx \mid \prop \proves \propB} \]
 
-It now becomes trivial to show soundness of the logic.
+It now becomes straight-forward to show consistency of the logic.
 
 %%% Local Variables:
 %%% mode: latex
diff --git a/program_logic/counter_examples.v b/program_logic/counter_examples.v
index aa3ceb25a82e44997fd4fe2f0c062da1d88e383f..fe673a206a1eb866a2301f5eeb0437abf7d715a2 100644
--- a/program_logic/counter_examples.v
+++ b/program_logic/counter_examples.v
@@ -93,7 +93,7 @@ Module inv. Section inv.
   Hypothesis finished_dup : ∀ γ, finished γ ⊢ finished γ ★ finished γ.
 
   (* We assume that we cannot view shift to false. *)
-  Hypothesis soundness : ¬ (True ⊢ pvs M1 False).
+  Hypothesis consistency : ¬ (True ⊢ pvs M1 False).
 
   (** Some general lemmas and proof mode compatibility. *)
   Lemma inv_open' i P R : inv i P ★ (P -★ pvs M0 (P ★ pvs M1 R)) ⊢ pvs M1 R.
@@ -186,7 +186,7 @@ Module inv. Section inv.
 
   Lemma contradiction : False.
   Proof.
-    apply soundness. iIntros "".
+    apply consistency. iIntros "".
     iVs A_alloc as (i) "#H".
     iPoseProof (saved_NA with "H") as "HN".
     iApply "HN". iApply saved_A. done.