docs: plainly rules

docs/base-logic.tex

@@ -307,7 +307,30 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
   {\prop \proves \propB \wand \propC}
 \end{mathpar}
 
-\paragraph{Laws for the always modality.}
+\paragraph{Laws for the plainness modality.}
+\begin{mathpar}
+\infer[$\plainly$-mono]
+  {\prop \proves \propB}
+  {\plainly{\prop} \proves \plainly{\propB}}
+\and
+\infer[$\plainly$-E]{}
+{\plainly\prop \proves \always\prop}
+\and
+\begin{array}[c]{rMcMl}
+  \TRUE &\proves& \plainly{\TRUE} \\
+  (\plainly P \Ra \plainly Q) &\proves& \plainly (\plainly P \Ra Q)
+\end{array}
+\and
+\begin{array}[c]{rMcMl}
+  \plainly{\prop} &\proves& \plainly\plainly\prop \\
+  \All x. \plainly{\prop} &\proves& \plainly{\All x. \prop} \\
+  \plainly{\Exists x. \prop} &\proves& \Exists x. \plainly{\prop}
+\end{array}
+\and
+\infer[PropExt]{}{\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) \proves P =_{\Prop} Q}
+\end{mathpar}
+
+\paragraph{Laws for the persistence modality.}
 \begin{mathpar}
 \infer[$\always$-mono]
   {\prop \proves \propB}
@@ -317,9 +340,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
 {\always\prop \proves \prop}
 \and
 \begin{array}[c]{rMcMl}
-  \TRUE &\proves& \always{\TRUE} \\
-  \always{(\prop \land \propB)} &\proves& \always{(\prop * \propB)} \\
-  \always{\prop} \land \propB &\proves& \always{\prop} * \propB
+  \always{\prop} \land \propB &\proves& \always{\prop} * \propB \\
+  (\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q)
 \end{array}
 \and
 \begin{array}[c]{rMcMl}
@@ -348,7 +370,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
 \and
 \begin{array}[c]{rMcMl}
   \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\
-  \always{\later\prop} &\provesIff& \later\always{\prop}
+  \always{\later\prop} &\provesIff& \later\always{\prop} \\
+  \plainly{\later\prop} &\provesIff& \later\plainly{\prop}
 \end{array}
 \end{mathpar}
 
@@ -397,6 +420,10 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
 \inferH{upd-update}
 {\melt \mupd \meltsB}
 {\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}
+
+\inferH{upd-plainly}
+{}
+{\upd\plainly\prop \proves \prop}
 \end{mathpar}
 The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.
 %\ralf{Trouble is, we don't actually have $\in$ inside the logic...}