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
182
		\text{$\var$ is guarded in $\term$} \and
		\text{$\type$ is complete}
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
\inferhref{L{\"o}b}{Loeb}
384
385
386
387
  {}
  {(\later\prop\Ra\prop) \proves \prop}
\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$.
Robbert Krebbers's avatar
Robbert Krebbers committed
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: