base-logic.tex 14.2 KB
 Ralf Jung committed Oct 04, 2016 1 2 3 \section{Base Logic} \label{sec:base-logic}  Ralf Jung committed Oct 06, 2016 4 The base logic is parameterized by an arbitrary CMRA $\monoid$ having a unit $\munit$.  Ralf Jung committed Oct 06, 2016 5 By \lemref{lem:cmra-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 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$. \begin{align*} \type \bnfdef{}& \sigtype \mid 1 \mid \type \times \type \mid \type \to \type \\[0.4em] \term, \prop, \pred \bnfdef{}& \var \mid \sigfn(\term_1, \dots, \term_n) \mid () \mid (\term, \term) \mid \pi_i\; \term \mid \Lam \var:\type.\term \mid \term(\term) \mid \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 63 %\\&  Ralf Jung committed Oct 04, 2016 64  \ownM{\term} \mid \mval(\term) \mid  Ralf Jung committed Oct 04, 2016 65  \always\prop \mid  Ralf Jung committed Nov 27, 2017 66  \plainly\prop \mid  Ralf Jung committed Oct 04, 2016 67  {\later\prop} \mid  Ralf Jung committed Mar 31, 2017 68  \upd \prop  Ralf Jung committed Oct 04, 2016 69 70 71 \end{align*} Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.  Ralf Jung committed Nov 27, 2017 72 Note that the modalities $\upd$, $\always$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.  Ralf Jung committed Oct 04, 2016 73 74 75 76 77 78 79 80 81 82 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 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171  \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}} } %%% products \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}} %%% 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 \infer{}{\vctx \proves \wtt\munit{\textlog{M}}} \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 \text{$\var$ is guarded in $\term$} }{ \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 172  {\vctx \proves \wtt{\ownM{\melt}}{\Prop}}  Ralf Jung committed Oct 04, 2016 173 174 175 176 177 178 \and \infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a CMRA}} {\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 179 180 181 \and \infer{\vctx \proves \wtt{\prop}{\Prop}} {\vctx \proves \wtt{\plainly\prop}{\Prop}}  Ralf Jung committed Oct 04, 2016 182 183 184 185 186 187 188 189 190 191 192 193 194 195 \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} \subsection{Proof rules} \label{sec:proof-rules}  Ralf Jung committed Oct 06, 2016 196 197 198 199 200 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. %Furthermore, an arbitrary \emph{boxed} assertion context $\always\pfctx$ may be added to every constituent. 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 201   Ralf Jung committed Oct 06, 2016 202 \judgment{\vctx \mid \prop \proves \propB}  Ralf Jung committed Oct 04, 2016 203 204 205 206 \paragraph{Laws of intuitionistic higher-order logic with equality.} This is entirely standard. \begin{mathparpagebreakable} \infer[Asm]  Ralf Jung committed Oct 06, 2016 207 208 209  {} {\prop \proves \prop} \and  Ralf Jung committed Oct 22, 2016 210 \infer[Cut]  Ralf Jung committed Oct 06, 2016 211 212  {\prop \proves \propB \and \propB \proves \propC} {\prop \proves \propC}  Ralf Jung committed Oct 04, 2016 213 214 \and \infer[Eq]  Ralf Jung committed Oct 07, 2016 215 216  {\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 217 218 219 \and \infer[Refl] {}  Ralf Jung committed Oct 07, 2016 220  {\TRUE \proves \term =_\type \term}  Ralf Jung committed Oct 04, 2016 221 222 \and \infer[$\bot$E]  Ralf Jung committed Oct 06, 2016 223 224  {} {\FALSE \proves \prop}  Ralf Jung committed Oct 04, 2016 225 226 227 \and \infer[$\top$I] {}  Ralf Jung committed Oct 06, 2016 228  {\prop \proves \TRUE}  Ralf Jung committed Oct 04, 2016 229 230 \and \infer[$\wedge$I]  Ralf Jung committed Oct 06, 2016 231 232  {\prop \proves \propB \\ \prop \proves \propC} {\prop \proves \propB \land \propC}  Ralf Jung committed Oct 04, 2016 233 234 \and \infer[$\wedge$EL]  Ralf Jung committed Oct 06, 2016 235 236  {\prop \proves \propB \land \propC} {\prop \proves \propB}  Ralf Jung committed Oct 04, 2016 237 238 \and \infer[$\wedge$ER]  Ralf Jung committed Oct 06, 2016 239 240  {\prop \proves \propB \land \propC} {\prop \proves \propC}  Ralf Jung committed Oct 04, 2016 241 242 \and \infer[$\vee$IL]  Ralf Jung committed Oct 06, 2016 243 244  {\prop \proves \propB } {\prop \proves \propB \lor \propC}  Ralf Jung committed Oct 04, 2016 245 246 \and \infer[$\vee$IR]  Ralf Jung committed Oct 06, 2016 247 248  {\prop \proves \propC} {\prop \proves \propB \lor \propC}  Ralf Jung committed Oct 04, 2016 249 250 \and \infer[$\vee$E]  Ralf Jung committed Oct 06, 2016 251 252 253  {\prop \proves \propC \\ \propB \proves \propC} {\prop \lor \propB \proves \propC}  Ralf Jung committed Oct 04, 2016 254 255 \and \infer[$\Ra$I]  Ralf Jung committed Oct 06, 2016 256 257  {\prop \land \propB \proves \propC} {\prop \proves \propB \Ra \propC}  Ralf Jung committed Oct 04, 2016 258 259 \and \infer[$\Ra$E]  Ralf Jung committed Oct 06, 2016 260 261  {\prop \proves \propB \Ra \propC \\ \prop \proves \propB} {\prop \proves \propC}  Ralf Jung committed Oct 04, 2016 262 263 \and \infer[$\forall$I]  Ralf Jung committed Oct 06, 2016 264 265  { \vctx,\var : \type\mid\prop \proves \propB} {\vctx\mid\prop \proves \All \var: \type. \propB}  Ralf Jung committed Oct 04, 2016 266 267 \and \infer[$\forall$E]  Ralf Jung committed Oct 06, 2016 268  {\vctx\mid\prop \proves \All \var :\type. \propB \\  Ralf Jung committed Oct 04, 2016 269  \vctx \proves \wtt\term\type}  Ralf Jung committed Oct 06, 2016 270  {\vctx\mid\prop \proves \propB[\term/\var]}  Ralf Jung committed Oct 07, 2016 271 \\  Ralf Jung committed Oct 04, 2016 272 \infer[$\exists$I]  Ralf Jung committed Oct 06, 2016 273  {\vctx\mid\prop \proves \propB[\term/\var] \\  Ralf Jung committed Oct 04, 2016 274  \vctx \proves \wtt\term\type}  Ralf Jung committed Oct 06, 2016 275  {\vctx\mid\prop \proves \exists \var: \type. \propB}  Ralf Jung committed Oct 04, 2016 276 277 \and \infer[$\exists$E]  Ralf Jung committed Oct 06, 2016 278 279  {\vctx,\var : \type\mid\prop \proves \propB} {\vctx\mid\Exists \var: \type. \prop \proves \propB}  Ralf Jung committed Oct 04, 2016 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 % \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} Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda$ and $\mu$. \paragraph{Laws of (affine) bunched implications.} \begin{mathpar} \begin{array}{rMcMl} \TRUE * \prop &\provesIff& \prop \\  Robbert Krebbers committed Oct 14, 2016 296 297  \prop * \propB &\proves& \propB * \prop \\ (\prop * \propB) * \propC &\proves& \prop * (\propB * \propC)  Ralf Jung committed Oct 04, 2016 298 299 300 301 302 303 304 305 306 307 308 309 \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 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 \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.}  Ralf Jung committed Oct 04, 2016 334 \begin{mathpar}  Ralf Jung committed Oct 04, 2016 335 336 337 \infer[$\always$-mono] {\prop \proves \propB} {\always{\prop} \proves \always{\propB}}  Ralf Jung committed Oct 04, 2016 338 \and  Ralf Jung committed Oct 10, 2016 339 340 341 \infer[$\always$-E]{} {\always\prop \proves \prop} \and  Ralf Jung committed Oct 04, 2016 342 \begin{array}[c]{rMcMl}  Ralf Jung committed Nov 27, 2017 343 344  \always{\prop} \land \propB &\proves& \always{\prop} * \propB \\ (\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q)  Ralf Jung committed Oct 04, 2016 345 \end{array}  Ralf Jung committed Oct 04, 2016 346 \and  Ralf Jung committed Oct 04, 2016 347 348 349 350 \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 351 352 353 \end{array} \end{mathpar}  Ralf Jung committed Oct 04, 2016 354   Ralf Jung committed Oct 04, 2016 355 356 357 \paragraph{Laws for the later modality.} \begin{mathpar} \infer[$\later$-mono]  Ralf Jung committed Oct 04, 2016 358 359  {\prop \proves \propB} {\later\prop \proves \later{\propB}}  Ralf Jung committed Oct 04, 2016 360 361 362 363 364 365 \and \infer[L{\"o}b] {} {(\later\prop\Ra\prop) \proves \prop} \and \begin{array}[c]{rMcMl}  Ralf Jung committed Oct 04, 2016 366 367  \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 368  \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop)  Ralf Jung committed Oct 04, 2016 369 370 371 \end{array} \and \begin{array}[c]{rMcMl}  Ralf Jung committed Oct 04, 2016 372  \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\  Ralf Jung committed Nov 27, 2017 373 374  \always{\later\prop} &\provesIff& \later\always{\prop} \\ \plainly{\later\prop} &\provesIff& \later\plainly{\prop}  Ralf Jung committed Oct 04, 2016 375 376 377 \end{array} \end{mathpar}  Ralf Jung committed Oct 04, 2016 378   Ralf Jung committed Oct 13, 2016 379 \paragraph{Laws for resources and validity.}  Ralf Jung committed Oct 04, 2016 380 \begin{mathpar}  Ralf Jung committed Oct 04, 2016 381 \begin{array}{rMcMl}  Ralf Jung committed Oct 04, 2016 382 383 384 385 \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 386 \end{array}  Ralf Jung committed Oct 13, 2016 387 388 389 390 391 392 393 394 % \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 395 \and  Ralf Jung committed Oct 04, 2016 396 \begin{array}{rMcMl}  Ralf Jung committed Oct 04, 2016 397 \ownM{\melt} &\proves& \mval(\melt) \\  Ralf Jung committed Oct 04, 2016 398 399 400 \mval(\melt \mtimes \meltB) &\proves& \mval(\melt) \\ \mval(\melt) &\proves& \always\mval(\melt) \end{array}  Ralf Jung committed Oct 04, 2016 401 402 \end{mathpar}  Ralf Jung committed Oct 04, 2016 403   Ralf Jung committed Oct 21, 2016 404 \paragraph{Laws for the basic update modality.}  Ralf Jung committed Oct 04, 2016 405 \begin{mathpar}  Ralf Jung committed Oct 14, 2016 406 \inferH{upd-mono}  Ralf Jung committed Oct 04, 2016 407 408 409 {\prop \proves \propB} {\upd\prop \proves \upd\propB}  Ralf Jung committed Oct 14, 2016 410 \inferH{upd-intro}  Ralf Jung committed Oct 04, 2016 411 412 {}{\prop \proves \upd \prop}  Ralf Jung committed Oct 14, 2016 413 \inferH{upd-trans}  Ralf Jung committed Oct 04, 2016 414 415 416 {} {\upd \upd \prop \proves \upd \prop}  Ralf Jung committed Oct 14, 2016 417 \inferH{upd-frame}  Ralf Jung committed Oct 04, 2016 418 419 420 421 {}{\propB * \upd\prop \proves \upd (\propB * \prop)} \inferH{upd-update} {\melt \mupd \meltsB}  Ralf Jung committed Oct 04, 2016 422 {\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}  Ralf Jung committed Nov 27, 2017 423 424 425 426  \inferH{upd-plainly} {} {\upd\plainly\prop \proves \prop}  Ralf Jung committed Oct 04, 2016 427 \end{mathpar}  Ralf Jung committed Oct 13, 2016 428 The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.  Ralf Jung committed Oct 22, 2016 429 %\ralf{Trouble is, we don't actually have $\in$ inside the logic...}  Ralf Jung committed Oct 04, 2016 430   Ralf Jung committed Oct 07, 2016 431 \subsection{Consistency}  Ralf Jung committed Oct 04, 2016 432   Ralf Jung committed Oct 07, 2016 433 The consistency statement of the logic reads as follows: For any $n$, we have  Ralf Jung committed Oct 04, 2016 434 \begin{align*}  Ralf Jung committed Oct 07, 2016 435  \lnot(\TRUE \proves (\upd\later)^n\spac\FALSE)  Ralf Jung committed Oct 04, 2016 436 437 \end{align*} where $(\upd\later)^n$ is short for $\upd\later$ being nested $n$ times.  Ralf Jung committed Oct 04, 2016 438   Ralf Jung committed Oct 07, 2016 439 440 441 442 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.  Ralf Jung committed Oct 04, 2016 443 444 445 446 447  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: