From 4b81074ef82b4bac8698150e69aef3629c7a2f76 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 27 Nov 2017 13:56:17 +0100
Subject: [PATCH] docs: plainly consistency
---
docs/base-logic.tex | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 6c8782d14..f0b97ad9c 100644
--- a/docs/base-logic.tex
+++ b/docs/base-logic.tex
@@ -432,13 +432,14 @@ The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that h
The consistency statement of the logic reads as follows: For any $n$, we have
\begin{align*}
- \lnot(\TRUE \proves (\upd\later)^n\spac\FALSE)
+ \lnot(\TRUE \proves (\later)^n\spac\FALSE)
\end{align*}
-where $(\upd\later)^n$ is short for $\upd\later$ being nested $n$ times.
+where $(\later)^n$ is short for $\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.
+For $\always$ and $\plainly$, this follows from the elimination rules.
+For updates, we use the fact that $\upd\FALSE \proves \upd\plainly\FALSE \proves \FALSE$.
+However, there is no elimination rule for $\later$, so we declare that it is impossible to derive a contradiction below any number of laters.
%%% Local Variables:
--
GitLab