base-logic.tex 15.4 KB
Newer Older
1
\section{Base Logic}
2 3
\label{sec:base-logic}

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.
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.}
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$).
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's avatar
Ralf Jung committed
35
      0 \mid
36
      1 \mid
Ralf Jung's avatar
Ralf Jung committed
37
      \type + \type \mid
38 39 40 41
      \type \times \type \mid
      \type \to \type
\\[0.4em]
  \term, \prop, \pred \bnfdef{}&
Ralf Jung's avatar
Ralf Jung committed
42
      \var \mid
43
      \sigfn(\term_1, \dots, \term_n) \mid
Ralf Jung's avatar
Ralf Jung committed
44
      \textlog{abort}\; \term \mid
45 46 47 48 49
      () \mid
      (\term, \term) \mid
      \pi_i\; \term \mid
      \Lam \var:\type.\term \mid
      \term(\term)  \mid
Ralf Jung's avatar
Ralf Jung committed
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
%
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's avatar
Ralf Jung committed
70
%\\&
Ralf Jung's avatar
Ralf Jung committed
71
    \ownM{\term} \mid \mval(\term) \mid
72
    \always\prop \mid
Ralf Jung's avatar
Ralf Jung committed
73
    \plainly\prop \mid
74
    {\later\prop} \mid
Ralf Jung's avatar
Ralf Jung committed
75
    \upd \prop
76
\end{align*}
Ralf Jung's avatar
Ralf Jung committed
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$.
81

Ralf Jung's avatar
Ralf Jung committed
82
Note that the modalities $\upd$, $\always$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
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's avatar
Ralf Jung committed
119 120 121
%%% empty, unit, products, sums
\and
	\infer{\vctx \proves \wtt\term{0}}
Ralf Jung's avatar
Ralf Jung committed
122
        {\vctx \proves \wtt{\textlog{abort}\; \term}\type}
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's avatar
Ralf Jung committed
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}}
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's avatar
Ralf Jung committed
149
        \infer{}{\vctx \proves \wtt\melt{\textlog{M}}}
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's avatar
Ralf Jung committed
181
		\text{$\var$ is guarded in $\term$} \and
182
		\text{$\type$ is complete and inhabited}
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's avatar
Ralf Jung committed
194
		{\vctx \proves \wtt{\ownM{\melt}}{\Prop}}
195
\and
196
	\infer{\vctx \proves \wtt{\melt}{\type} \and \text{$\type$ is a camera}}
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's avatar
Ralf Jung committed
201 202 203
\and
	\infer{\vctx \proves \wtt{\prop}{\Prop}}
		{\vctx \proves \wtt{\plainly\prop}{\Prop}}
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's avatar
Ralf Jung committed
215
\subsection{Proof Rules}
216 217
\label{sec:proof-rules}

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.
221
%Furthermore, an arbitrary \emph{boxed} proposition context $\always\pfctx$ may be added to every constituent.
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.
223

224
\judgment{\vctx \mid \prop \proves \propB}
225 226 227 228
\paragraph{Laws of intuitionistic higher-order logic with equality.}
This is entirely standard.
\begin{mathparpagebreakable}
\infer[Asm]
229 230 231
  {}
  {\prop \proves \prop}
\and
232
\infer[Cut]
233 234
  {\prop \proves \propB \and \propB \proves \propC}
  {\prop \proves \propC}
235 236
\and
\infer[Eq]
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]}
239 240 241
\and
\infer[Refl]
  {}
242
  {\TRUE \proves \term =_\type \term}
243 244
\and
\infer[$\bot$E]
245 246
  {}
  {\FALSE \proves \prop}
247 248 249
\and
\infer[$\top$I]
  {}
250
  {\prop \proves \TRUE}
251 252
\and
\infer[$\wedge$I]
253 254
  {\prop \proves \propB \\ \prop \proves \propC}
  {\prop \proves \propB \land \propC}
255 256
\and
\infer[$\wedge$EL]
257 258
  {\prop \proves \propB \land \propC}
  {\prop \proves \propB}
259 260
\and
\infer[$\wedge$ER]
261 262
  {\prop \proves \propB \land \propC}
  {\prop \proves \propC}
263 264
\and
\infer[$\vee$IL]
265 266
  {\prop \proves \propB }
  {\prop \proves \propB \lor \propC}
267 268
\and
\infer[$\vee$IR]
269 270
  {\prop \proves \propC}
  {\prop \proves \propB \lor \propC}
271 272
\and
\infer[$\vee$E]
273 274 275
  {\prop \proves \propC \\
   \propB \proves \propC}
  {\prop \lor \propB \proves \propC}
276 277
\and
\infer[$\Ra$I]
278 279
  {\prop \land \propB \proves \propC}
  {\prop \proves \propB \Ra \propC}
280 281
\and
\infer[$\Ra$E]
282 283
  {\prop \proves \propB \Ra \propC \\ \prop \proves \propB}
  {\prop \proves \propC}
284 285
\and
\infer[$\forall$I]
286 287
  { \vctx,\var : \type\mid\prop \proves \propB}
  {\vctx\mid\prop \proves \All \var: \type. \propB}
288 289
\and
\infer[$\forall$E]
290
  {\vctx\mid\prop \proves \All \var :\type. \propB \\
291
   \vctx \proves \wtt\term\type}
292
  {\vctx\mid\prop \proves \propB[\term/\var]}
293
\\
294
\infer[$\exists$I]
295
  {\vctx\mid\prop \proves \propB[\term/\var] \\
296
   \vctx \proves \wtt\term\type}
297
  {\vctx\mid\prop \proves \exists \var: \type. \propB}
298 299
\and
\infer[$\exists$E]
300 301
  {\vctx,\var : \type\mid\prop \proves \propB}
  {\vctx\mid\Exists \var: \type. \prop \proves \propB}
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's avatar
Ralf Jung committed
311
Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\textlog{abort}$, sum elimination, $\lambda$ and $\mu$.
312 313 314 315 316 317


\paragraph{Laws of (affine) bunched implications.}
\begin{mathpar}
\begin{array}{rMcMl}
  \TRUE * \prop &\provesIff& \prop \\
318 319
  \prop * \propB &\proves& \propB * \prop \\
  (\prop * \propB) * \propC &\proves& \prop * (\propB * \propC)
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's avatar
Ralf Jung committed
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's avatar
Ralf Jung committed
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's avatar
Ralf Jung committed
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's avatar
Ralf Jung committed
351 352
%\and
%\infer[PropExt]{}{\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) \proves P =_{\Prop} Q}
Ralf Jung's avatar
Ralf Jung committed
353 354 355
\end{mathpar}

\paragraph{Laws for the persistence modality.}
356
\begin{mathpar}
357 358 359
\infer[$\always$-mono]
  {\prop \proves \propB}
  {\always{\prop} \proves \always{\propB}}
360
\and
361 362 363
\infer[$\always$-E]{}
{\always\prop \proves \prop}
\and
364
\begin{array}[c]{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
365 366
  (\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q) \\
  \always{\prop} \land \propB &\proves& \always{\prop} * \propB
367
\end{array}
368
\and
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}
373 374 375
\end{array}
\end{mathpar}

376

377 378 379
\paragraph{Laws for the later modality.}
\begin{mathpar}
\infer[$\later$-mono]
380 381
  {\prop \proves \propB}
  {\later\prop \proves \later{\propB}}
382
\and
Ralf Jung's avatar
Ralf Jung committed
383
\infer[$\later$-I]
384
  {}
Ralf Jung's avatar
Ralf Jung committed
385
  {\prop \proves \later\prop}
386 387
\and
\begin{array}[c]{rMcMl}
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's avatar
Ralf Jung committed
390
  \later\prop &\proves& \later\FALSE \lor (\later\FALSE \Ra \prop)
391 392 393
\end{array}
\and
\begin{array}[c]{rMcMl}
394
  \later{(\prop * \propB)} &\provesIff& \later\prop * \later\propB \\
Ralf Jung's avatar
Ralf Jung committed
395 396
  \always{\later\prop} &\provesIff& \later\always{\prop} \\
  \plainly{\later\prop} &\provesIff& \later\plainly{\prop}
397 398 399
\end{array}
\end{mathpar}

400

Ralf Jung's avatar
Ralf Jung committed
401
\paragraph{Laws for resources and validity.}
402
\begin{mathpar}
403
\begin{array}{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
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)
408
\end{array}
Ralf Jung's avatar
Ralf Jung committed
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}
417
\and
418
\begin{array}{rMcMl}
Ralf Jung's avatar
Ralf Jung committed
419
\ownM{\melt} &\proves& \mval(\melt) \\
420 421 422
\mval(\melt \mtimes \meltB) &\proves& \mval(\melt) \\
\mval(\melt) &\proves& \always\mval(\melt)
\end{array}
423 424
\end{mathpar}

425

Ralf Jung's avatar
Ralf Jung committed
426
\paragraph{Laws for the basic update modality.}
427
\begin{mathpar}
Ralf Jung's avatar
Ralf Jung committed
428
\inferH{upd-mono}
429 430 431
{\prop \proves \propB}
{\upd\prop \proves \upd\propB}

Ralf Jung's avatar
Ralf Jung committed
432
\inferH{upd-intro}
433 434
{}{\prop \proves \upd \prop}

Ralf Jung's avatar
Ralf Jung committed
435
\inferH{upd-trans}
436 437 438
{}
{\upd \upd \prop \proves \upd \prop}

Ralf Jung's avatar
Ralf Jung committed
439
\inferH{upd-frame}
440 441 442 443
{}{\propB * \upd\prop \proves \upd (\propB * \prop)}

\inferH{upd-update}
{\melt \mupd \meltsB}
Ralf Jung's avatar
Ralf Jung committed
444
{\ownM\melt \proves \upd \Exists\meltB\in\meltsB. \ownM\meltB}
Ralf Jung's avatar
Ralf Jung committed
445 446 447 448

\inferH{upd-plainly}
{}
{\upd\plainly\prop \proves \prop}
449
\end{mathpar}
Ralf Jung's avatar
Ralf Jung committed
450
The premise in \ruleref{upd-update} is a \emph{meta-level} side-condition that has to be proven about $a$ and $B$.
451
%\ralf{Trouble is, we do not actually have $\in$ inside the logic...}
452

Ralf Jung's avatar
Ralf Jung committed
453
\subsection{Consistency}
454

Ralf Jung's avatar
Ralf Jung committed
455
The consistency statement of the logic reads as follows: For any $n$, we have
456
\begin{align*}
Ralf Jung's avatar
Ralf Jung committed
457
  \lnot(\TRUE \proves (\later)^n\spac\FALSE)
458
\end{align*}
Ralf Jung's avatar
Ralf Jung committed
459
where $(\later)^n$ is short for $\later$ being nested $n$ times.
460

Ralf Jung's avatar
Ralf Jung committed
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's avatar
Ralf Jung committed
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's avatar
Ralf Jung committed
465

466 467 468 469 470

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "iris"
%%% End: