base-logic.tex 15.4 KB
 Ralf Jung committed Dec 10, 2017 1 \section{Base Logic}  Ralf Jung committed Oct 04, 2016 2 3 \label{sec:base-logic}  Robbert Krebbers committed Dec 10, 2017 4 5 The base logic is parameterized by an arbitrary camera $\monoid$ having a unit $\munit$. By \lemref{lem:camera-unit-total-core}, this means that the core of $\monoid$ is a total function, so we will treat it as such in the following.  Ralf Jung committed Oct 04, 2016 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 This defines the structure of resources that can be owned. As usual for higher-order logics, you can furthermore pick a \emph{signature} $\Sig = (\SigType, \SigFn, \SigAx)$ to add more types, symbols and axioms to the language. You have to make sure that $\SigType$ includes the base types: $\SigType \supseteq \{ \textlog{M}, \Prop \}$ Elements of $\SigType$ are ranged over by $\sigtype$. Each function symbol in $\SigFn$ has an associated \emph{arity} comprising a natural number $n$ and an ordered list of $n+1$ types $\type$ (the grammar of $\type$ is defined below, and depends only on $\SigType$). We write $\sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn$ to express that $\sigfn$ is a function symbol with the indicated arity. Furthermore, $\SigAx$ is a set of \emph{axioms}, that is, terms $\term$ of type $\Prop$. Again, the grammar of terms and their typing rules are defined below, and depends only on $\SigType$ and $\SigFn$, not on $\SigAx$. Elements of $\SigAx$ are ranged over by $\sigax$. \subsection{Grammar}\label{sec:grammar} \paragraph{Syntax.}  Robbert Krebbers committed Oct 17, 2016 29 Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\Var$ of variables (ranged over by metavariables $\var$, $\varB$, $\varC$).  Ralf Jung committed Oct 04, 2016 30 31 32 33 34 Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$. \begin{align*} \type \bnfdef{}& \sigtype \mid  Ralf Jung committed Nov 28, 2017 35  0 \mid  Ralf Jung committed Oct 04, 2016 36  1 \mid  Ralf Jung committed Nov 28, 2017 37  \type + \type \mid  Ralf Jung committed Oct 04, 2016 38 39 40 41  \type \times \type \mid \type \to \type \\[0.4em] \term, \prop, \pred \bnfdef{}&  Ralf Jung committed Nov 28, 2017 42  \var \mid  Ralf Jung committed Oct 04, 2016 43  \sigfn(\term_1, \dots, \term_n) \mid  Ralf Jung committed Nov 28, 2017 44  \textlog{abort}\; \term \mid  Ralf Jung committed Oct 04, 2016 45 46 47 48 49  () \mid (\term, \term) \mid \pi_i\; \term \mid \Lam \var:\type.\term \mid \term(\term) \mid  Ralf Jung committed Nov 28, 2017 50 51 52 53 \\& \textlog{inj}_i\; \term \mid \textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var. \term \mid \Ret\textlog{inj}_2\; \var. \term \;\textlog{end} \mid %  Ralf Jung committed Oct 04, 2016 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69  \melt \mid \mcore\term \mid \term \mtimes \term \mid \\& \FALSE \mid \TRUE \mid \term =_\type \term \mid \prop \Ra \prop \mid \prop \land \prop \mid \prop \lor \prop \mid \prop * \prop \mid \prop \wand \prop \mid \\& \MU \var:\type. \term \mid \Exists \var:\type. \prop \mid \All \var:\type. \prop \mid  Ralf Jung committed Mar 31, 2017 70 %\\&  Ralf Jung committed Oct 04, 2016 71  \ownM{\term} \mid \mval(\term) \mid  Ralf Jung committed Oct 04, 2016 72  \always\prop \mid  Ralf Jung committed Nov 27, 2017 73  \plainly\prop \mid  Ralf Jung committed Oct 04, 2016 74  {\later\prop} \mid  Ralf Jung committed Mar 31, 2017 75  \upd \prop  Ralf Jung committed Oct 04, 2016 76 \end{align*}  Ralf Jung committed Nov 28, 2017 77 78 79 80 Well-typedness forces recursive definitions to be \emph{guarded}: In $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality. Furthermore, the type of the definition must be \emph{complete}. The type $\Prop$ is complete, and if $\type$ is complete, then so is $\type' \to \type$.  Ralf Jung committed Oct 04, 2016 81   Ralf Jung committed Nov 27, 2017 82 Note that the modalities $\upd$, $\always$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.  Ralf Jung committed Oct 04, 2016 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118  \paragraph{Variable conventions.} We assume that, if a term occurs multiple times in a rule, its free variables are exactly those binders which are available at every occurrence. \subsection{Types}\label{sec:types} Iris terms are simply-typed. The judgment $\vctx \proves \wtt{\term}{\type}$ expresses that, in variable context $\vctx$, the term $\term$ has type $\type$. A variable context, $\vctx = x_1:\type_1, \dots, x_n:\type_n$, declares a list of variables and their types. In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $\vctx$. \judgment[Well-typed terms]{\vctx \proves_\Sig \wtt{\term}{\type}} \begin{mathparpagebreakable} %%% variables and function symbols \axiom{x : \type \proves \wtt{x}{\type}} \and \infer{\vctx \proves \wtt{\term}{\type}} {\vctx, x:\type' \proves \wtt{\term}{\type}} \and \infer{\vctx, x:\type', y:\type' \proves \wtt{\term}{\type}} {\vctx, x:\type' \proves \wtt{\term[x/y]}{\type}} \and \infer{\vctx_1, x:\type', y:\type'', \vctx_2 \proves \wtt{\term}{\type}} {\vctx_1, x:\type'', y:\type', \vctx_2 \proves \wtt{\term[y/x,x/y]}{\type}} \and \infer{ \vctx \proves \wtt{\term_1}{\type_1} \and \cdots \and \vctx \proves \wtt{\term_n}{\type_n} \and \sigfn : \type_1, \dots, \type_n \to \type_{n+1} \in \SigFn }{ \vctx \proves \wtt {\sigfn(\term_1, \dots, \term_n)} {\type_{n+1}} }  Ralf Jung committed Nov 28, 2017 119 120 121 %%% empty, unit, products, sums \and \infer{\vctx \proves \wtt\term{0}}  Ralf Jung committed Nov 28, 2017 122  {\vctx \proves \wtt{\textlog{abort}\; \term}\type}  Ralf Jung committed Oct 04, 2016 123 124 125 126 127 128 129 130 \and \axiom{\vctx \proves \wtt{()}{1}} \and \infer{\vctx \proves \wtt{\term}{\type_1} \and \vctx \proves \wtt{\termB}{\type_2}} {\vctx \proves \wtt{(\term,\termB)}{\type_1 \times \type_2}} \and \infer{\vctx \proves \wtt{\term}{\type_1 \times \type_2} \and i \in \{1, 2\}} {\vctx \proves \wtt{\pi_i\,\term}{\type_i}}  Ralf Jung committed Nov 28, 2017 131 132 133 134 135 136 137 138 \and \infer{\vctx \proves \wtt\term{\type_i} \and i \in \{1, 2\}} {\vctx \proves \wtt{\textlog{inj}_i\;\term}{\type_1 + \type_2}} \and \infer{\vctx \proves \wtt\term{\type_1 + \type_2} \and \vctx, \var:\type_1 \proves \wtt{\term_1}\type \and \vctx, \varB:\type_2 \proves \wtt{\term_2}\type} {\vctx \proves \wtt{\textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var. \term_1 \mid \Ret\textlog{inj}_2\; \varB. \term_2 \;\textlog{end}}{\type}}  Ralf Jung committed Oct 04, 2016 139 140 141 142 143 144 145 146 147 148 %%% functions \and \infer{\vctx, x:\type \proves \wtt{\term}{\type'}} {\vctx \proves \wtt{\Lam x. \term}{\type \to \type'}} \and \infer {\vctx \proves \wtt{\term}{\type \to \type'} \and \wtt{\termB}{\type}} {\vctx \proves \wtt{\term(\termB)}{\type'}} %%% monoids \and  Ralf Jung committed Nov 28, 2017 149  \infer{}{\vctx \proves \wtt\melt{\textlog{M}}}  Ralf Jung committed Oct 04, 2016 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 \and \infer{\vctx \proves \wtt\melt{\textlog{M}}}{\vctx \proves \wtt{\mcore\melt}{\textlog{M}}} \and \infer{\vctx \proves \wtt{\melt}{\textlog{M}} \and \vctx \proves \wtt{\meltB}{\textlog{M}}} {\vctx \proves \wtt{\melt \mtimes \meltB}{\textlog{M}}} %%% props and predicates \\ \axiom{\vctx \proves \wtt{\FALSE}{\Prop}} \and \axiom{\vctx \proves \wtt{\TRUE}{\Prop}} \and \infer{\vctx \proves \wtt{\term}{\type} \and \vctx \proves \wtt{\termB}{\type}} {\vctx \proves \wtt{\term =_\type \termB}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}} {\vctx \proves \wtt{\prop \Ra \propB}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}} {\vctx \proves \wtt{\prop \land \propB}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}} {\vctx \proves \wtt{\prop \lor \propB}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}} {\vctx \proves \wtt{\prop * \propB}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop} \and \vctx \proves \wtt{\propB}{\Prop}} {\vctx \proves \wtt{\prop \wand \propB}{\Prop}} \and \infer{ \vctx, \var:\type \proves \wtt{\term}{\type} \and  Ralf Jung committed Nov 28, 2017 181  \text{$\var$ is guarded in $\term$} \and  Robbert Krebbers committed Jan 31, 2018 182  \text{$\type$ is complete and inhabited}  Ralf Jung committed Oct 04, 2016 183 184 185 186 187 188 189 190 191 192 193  }{ \vctx \proves \wtt{\MU \var:\type. \term}{\type} } \and \infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\Exists x:\type. \prop}{\Prop}} \and \infer{\vctx, x:\type \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\All x:\type. \prop}{\Prop}} \and \infer{\vctx \proves \wtt{\melt}{\textlog{M}}}  Ralf Jung committed Oct 04, 2016 194  {\vctx \proves \wtt{\ownM{\melt}}{\Prop}}  Ralf Jung committed Oct 04, 2016 195 \and  Robbert Krebbers committed Dec 10, 2017 196  \infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a camera}}  Ralf Jung committed Oct 04, 2016 197 198 199 200  {\vctx \proves \wtt{\mval(\melt)}{\Prop}} \and \infer{\vctx \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\always\prop}{\Prop}}  Ralf Jung committed Nov 27, 2017 201 202 203 \and \infer{\vctx \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\plainly\prop}{\Prop}}  Ralf Jung committed Oct 04, 2016 204 205 206 207 208 209 210 211 212 213 214 \and \infer{\vctx \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\later\prop}{\Prop}} \and \infer{ \vctx \proves \wtt{\prop}{\Prop} }{ \vctx \proves \wtt{\upd \prop}{\Prop} } \end{mathparpagebreakable}  Ralf Jung committed Dec 10, 2017 215 \subsection{Proof Rules}  Ralf Jung committed Oct 04, 2016 216 217 \label{sec:proof-rules}  Ralf Jung committed Oct 06, 2016 218 219 220 The judgment $\vctx \mid \prop \proves \propB$ says that with free variables $\vctx$, proposition $\propB$ holds whenever assumption $\prop$ holds. Most of the rules will entirely omit the variable contexts $\vctx$. In this case, we assume the same arbitrary context is used for every constituent of the rules.  Robbert Krebbers committed Dec 10, 2017 221 %Furthermore, an arbitrary \emph{boxed} proposition context $\always\pfctx$ may be added to every constituent.  Ralf Jung committed Oct 06, 2016 222 Axioms $\vctx \mid \prop \provesIff \propB$ indicate that both $\vctx \mid \prop \proves \propB$ and $\vctx \mid \propB \proves \prop$ are proof rules of the logic.  Ralf Jung committed Oct 04, 2016 223   Ralf Jung committed Oct 06, 2016 224 \judgment{\vctx \mid \prop \proves \propB}  Ralf Jung committed Oct 04, 2016 225 226 227 228 \paragraph{Laws of intuitionistic higher-order logic with equality.} This is entirely standard. \begin{mathparpagebreakable} \infer[Asm]  Ralf Jung committed Oct 06, 2016 229 230 231  {} {\prop \proves \prop} \and  Ralf Jung committed Oct 22, 2016 232 \infer[Cut]  Ralf Jung committed Oct 06, 2016 233 234  {\prop \proves \propB \and \propB \proves \propC} {\prop \proves \propC}  Ralf Jung committed Oct 04, 2016 235 236 \and \infer[Eq]  Ralf Jung committed Oct 07, 2016 237 238  {\vctx,\var:\type \proves \wtt\propB\Prop \\ \vctx\mid\prop \proves \propB[\term/\var] \\ \vctx\mid\prop \proves \term =_\type \term'} {\vctx\mid\prop \proves \propB[\term'/\var]}  Ralf Jung committed Oct 04, 2016 239 240 241 \and \infer[Refl] {}  Ralf Jung committed Oct 07, 2016 242  {\TRUE \proves \term =_\type \term}  Ralf Jung committed Oct 04, 2016 243 244 \and \infer[$\bot$E]  Ralf Jung committed Oct 06, 2016 245 246  {} {\FALSE \proves \prop}  Ralf Jung committed Oct 04, 2016 247 248 249 \and \infer[$\top$I] {}  Ralf Jung committed Oct 06, 2016 250  {\prop \proves \TRUE}  Ralf Jung committed Oct 04, 2016 251 252 \and \infer[$\wedge$I]  Ralf Jung committed Oct 06, 2016 253 254  {\prop \proves \propB \\ \prop \proves \propC} {\prop \proves \propB \land \propC}  Ralf Jung committed Oct 04, 2016 255 256 \and \infer[$\wedge$EL]  Ralf Jung committed Oct 06, 2016 257 258  {\prop \proves \propB \land \propC} {\prop \proves \propB}  Ralf Jung committed Oct 04, 2016 259 260 \and \infer[$\wedge$ER]  Ralf Jung committed Oct 06, 2016 261 262  {\prop \proves \propB \land \propC} {\prop \proves \propC}  Ralf Jung committed Oct 04, 2016 263 264 \and \infer[$\vee$IL]  Ralf Jung committed Oct 06, 2016 265 266  {\prop \proves \propB } {\prop \proves \propB \lor \propC}  Ralf Jung committed Oct 04, 2016 267 268 \and \infer[$\vee$IR]  Ralf Jung committed Oct 06, 2016 269 270  {\prop \proves \propC} {\prop \proves \propB \lor \propC}  Ralf Jung committed Oct 04, 2016 271 272 \and \infer[$\vee$E]  Ralf Jung committed Oct 06, 2016 273 274 275  {\prop \proves \propC \\ \propB \proves \propC} {\prop \lor \propB \proves \propC}  Ralf Jung committed Oct 04, 2016 276 277 \and \infer[$\Ra$I]  Ralf Jung committed Oct 06, 2016 278 279  {\prop \land \propB \proves \propC} {\prop \proves \propB \Ra \propC}  Ralf Jung committed Oct 04, 2016 280 281 \and \infer[$\Ra$E]  Ralf Jung committed Oct 06, 2016 282 283  {\prop \proves \propB \Ra \propC \\ \prop \proves \propB} {\prop \proves \propC}  Ralf Jung committed Oct 04, 2016 284 285 \and \infer[$\forall$I]  Ralf Jung committed Oct 06, 2016 286 287  { \vctx,\var : \type\mid\prop \proves \propB} {\vctx\mid\prop \proves \All \var: \type. \propB}  Ralf Jung committed Oct 04, 2016 288 289 \and \infer[$\forall$E]  Ralf Jung committed Oct 06, 2016 290  {\vctx\mid\prop \proves \All \var :\type. \propB \\  Ralf Jung committed Oct 04, 2016 291  \vctx \proves \wtt\term\type}  Ralf Jung committed Oct 06, 2016 292  {\vctx\mid\prop \proves \propB[\term/\var]}  Ralf Jung committed Oct 07, 2016 293 \\  Ralf Jung committed Oct 04, 2016 294 \infer[$\exists$I]  Ralf Jung committed Oct 06, 2016 295  {\vctx\mid\prop \proves \propB[\term/\var] \\  Ralf Jung committed Oct 04, 2016 296  \vctx \proves \wtt\term\type}  Ralf Jung committed Oct 06, 2016 297  {\vctx\mid\prop \proves \exists \var: \type. \propB}  Ralf Jung committed Oct 04, 2016 298 299 \and \infer[$\exists$E]  Ralf Jung committed Oct 06, 2016 300 301  {\vctx,\var : \type\mid\prop \proves \propB} {\vctx\mid\Exists \var: \type. \prop \proves \propB}  Ralf Jung committed Oct 04, 2016 302 303 304 305 306 307 308 309 310 % \and % \infer[$\lambda$] % {} % {\pfctx \proves (\Lam\var: \type. \prop)(\term) =_{\type\to\type'} \prop[\term/\var]} % \and % \infer[$\mu$] % {} % {\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]} \end{mathparpagebreakable}  Ralf Jung committed Nov 28, 2017 311 Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\textlog{abort}$, sum elimination, $\lambda$ and $\mu$.  Ralf Jung committed Oct 04, 2016 312 313 314 315 316 317  \paragraph{Laws of (affine) bunched implications.} \begin{mathpar} \begin{array}{rMcMl} \TRUE * \prop &\provesIff& \prop \\  Robbert Krebbers committed Oct 14, 2016 318 319  \prop * \propB &\proves& \propB * \prop \\ (\prop * \propB) * \propC &\proves& \prop * (\propB * \propC)  Ralf Jung committed Oct 04, 2016 320 321 322 323 324 325 326 327 328 329 330 331 \end{array} \and \infer[$*$-mono] {\prop_1 \proves \propB_1 \and \prop_2 \proves \propB_2} {\prop_1 * \prop_2 \proves \propB_1 * \propB_2} \and \inferB[$\wand$I-E] {\prop * \propB \proves \propC} {\prop \proves \propB \wand \propC} \end{mathpar}  Ralf Jung committed Nov 27, 2017 332 333 334 335 336 337 338 339 340 341 \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}  Ralf Jung committed Nov 28, 2017 342 343  (\plainly P \Ra \plainly Q) &\proves& \plainly (\plainly P \Ra Q) \\ \plainly ( ( P \Ra Q) \land (Q \Ra P ) ) &\proves& P =_{\Prop} Q  Ralf Jung committed Nov 27, 2017 344 345 346 347 348 349 350 \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}  Ralf Jung committed Nov 28, 2017 351 352 %\and %\infer[PropExt]{}{\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) \proves P =_{\Prop} Q}  Ralf Jung committed Nov 27, 2017 353 354 355 \end{mathpar} \paragraph{Laws for the persistence modality.}  Ralf Jung committed Oct 04, 2016 356 \begin{mathpar}  Ralf Jung committed Oct 04, 2016 357 358 359 \infer[$\always$-mono] {\prop \proves \propB} {\always{\prop} \proves \always{\propB}}  Ralf Jung committed Oct 04, 2016 360 \and  Ralf Jung committed Oct 10, 2016 361 362 363 \infer[$\always$-E]{} {\always\prop \proves \prop} \and  Ralf Jung committed Oct 04, 2016 364 \begin{array}[c]{rMcMl}  Ralf Jung committed Nov 28, 2017 365 366  (\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q) \\ \always{\prop} \land \propB &\proves& \always{\prop} * \propB  Ralf Jung committed Oct 04, 2016 367 \end{array}  Ralf Jung committed Oct 04, 2016 368 \and  Ralf Jung committed Oct 04, 2016 369 370 371 372 \begin{array}[c]{rMcMl} \always{\prop} &\proves& \always\always\prop \\ \All x. \always{\prop} &\proves& \always{\All x. \prop} \\ \always{\Exists x. \prop} &\proves& \Exists x. \always{\prop}  Ralf Jung committed Oct 04, 2016 373 374 375 \end{array} \end{mathpar}  Ralf Jung committed Oct 04, 2016 376   Ralf Jung committed Oct 04, 2016 377 378 379 \paragraph{Laws for the later modality.} \begin{mathpar} \infer[$\later$-mono]  Ralf Jung committed Oct 04, 2016 380 381  {\prop \proves \propB} {\later\prop \proves \later{\propB}}  Ralf Jung committed Oct 04, 2016 382 \and  Ralf Jung committed Jun 05, 2019 383 \infer[$\later$-I]  Ralf Jung committed Oct 04, 2016 384  {}  Ralf Jung committed Jun 05, 2019 385  {\prop \proves \later\prop}  Ralf Jung committed Oct 04, 2016 386 387 \and \begin{array}[c]{rMcMl}  Ralf Jung committed Oct 04, 2016 388 389  \All x. \later\prop &\proves& \later{\All x.\prop} \\ \later\Exists x. \prop &\proves& \later\FALSE \lor {\Exists x.\later\prop} \\  Ralf Jung committed Oct 14, 2016 390  \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop)  Ralf Jung committed Oct 04, 2016 391 392 393 \end{array} \and \begin{array}[c]{rMcMl}  Ralf Jung committed Oct 04, 2016 394  \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\  Ralf Jung committed Nov 27, 2017 395 396  \always{\later\prop} &\provesIff& \later\always{\prop} \\ \plainly{\later\prop} &\provesIff& \later\plainly{\prop}  Ralf Jung committed Oct 04, 2016 397 398 399 \end{array} \end{mathpar}  Ralf Jung committed Oct 04, 2016 400   Ralf Jung committed Oct 13, 2016 401 \paragraph{Laws for resources and validity.}  Ralf Jung committed Oct 04, 2016 402 \begin{mathpar}  Ralf Jung committed Oct 04, 2016 403 \begin{array}{rMcMl}  Ralf Jung committed Oct 04, 2016 404 405 406 407 \ownM{\melt} * \ownM{\meltB} &\provesIff& \ownM{\melt \mtimes \meltB} \\ \ownM\melt &\proves& \always{\ownM{\mcore\melt}} \\ \TRUE &\proves& \ownM{\munit} \\ \later\ownM\melt &\proves& \Exists\meltB. \ownM\meltB \land \later(\melt = \meltB)  Ralf Jung committed Oct 04, 2016 408 \end{array}  Ralf Jung committed Oct 13, 2016 409 410 411 412 413 414 415 416 % \and % \infer[valid-intro] % {\melt \in \mval} % {\TRUE \vdash \mval(\melt)} % \and % \infer[valid-elim] % {\melt \notin \mval_0} % {\mval(\melt) \proves \FALSE}  Ralf Jung committed Oct 04, 2016 417 \and  Ralf Jung committed Oct 04, 2016 418 \begin{array}{rMcMl}  Ralf Jung committed Oct 04, 2016 419 \ownM{\melt} &\proves& \mval(\melt) \\  Ralf Jung committed Oct 04, 2016 420 421 422 \mval(\melt \mtimes \meltB) &\proves& \mval(\melt) \\ \mval(\melt) &\proves& \always\mval(\melt) \end{array}  Ralf Jung committed Oct 04, 2016 423 424 \end{mathpar}  Ralf Jung committed Oct 04, 2016 425   Ralf Jung committed Oct 21, 2016 426 \paragraph{Laws for the basic update modality.}  Ralf Jung committed Oct 04, 2016 427 \begin{mathpar}  Ralf Jung committed Oct 14, 2016 428 \inferH{upd-mono}  Ralf Jung committed Oct 04, 2016 429 430 431 {\prop \proves \propB} {\upd\prop \proves \upd\propB}  Ralf Jung committed Oct 14, 2016 432 \inferH{upd-intro}  Ralf Jung committed Oct 04, 2016 433 434 {}{\prop \proves \upd \prop}  Ralf Jung committed Oct 14, 2016 435 \inferH{upd-trans}  Ralf Jung committed Oct 04, 2016 436 437 438 {} {\upd \upd \prop \proves \upd \prop}  Ralf Jung committed Oct 14, 2016 439 \inferH{upd-frame}  Ralf Jung committed Oct 04, 2016 440 441 442 443 {}{\propB * \upd\prop \proves \upd (\propB * \prop)} \inferH{upd-update} {\melt \mupd \meltsB}  Ralf Jung committed Oct 04, 2016 444 {\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}  Ralf Jung committed Nov 27, 2017 445 446 447 448  \inferH{upd-plainly} {} {\upd\plainly\prop \proves \prop}  Ralf Jung committed Oct 04, 2016 449 \end{mathpar}  Ralf Jung committed Oct 13, 2016 450 The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.  Robbert Krebbers committed Dec 10, 2017 451 %\ralf{Trouble is, we do not actually have $\in$ inside the logic...}  Ralf Jung committed Oct 04, 2016 452   Ralf Jung committed Oct 07, 2016 453 \subsection{Consistency}  Ralf Jung committed Oct 04, 2016 454   Ralf Jung committed Oct 07, 2016 455 The consistency statement of the logic reads as follows: For any $n$, we have  Ralf Jung committed Oct 04, 2016 456 \begin{align*}  Ralf Jung committed Nov 27, 2017 457  \lnot(\TRUE \proves (\later)^n\spac\FALSE)  Ralf Jung committed Oct 04, 2016 458 \end{align*}  Ralf Jung committed Nov 27, 2017 459 where $(\later)^n$ is short for $\later$ being nested $n$ times.  Ralf Jung committed Oct 04, 2016 460   Ralf Jung committed Oct 07, 2016 461 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.  Ralf Jung committed Nov 27, 2017 462 463 464 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.  Ralf Jung committed Oct 07, 2016 465   Ralf Jung committed Oct 04, 2016 466 467 468 469 470  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: