Newer
Older
Ralf Jung
committed
\section{Extensions of the Base Logic}
In this section we discuss some additional constructions that we define within and on top of the base logic.
Ralf Jung
committed
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
These are not ``extensions'' in the sense that they change the proof power of the logic, they just form useful derived principles.
\subsection{Derived rules about base connectives}
We collect here some important and frequently used derived proof rules.
\begin{mathparpagebreakable}
\infer{}
{\prop \Ra \propB \proves \prop \wand \propB}
\infer{}
{\prop * \Exists\var.\propB \provesIff \Exists\var. \prop * \propB}
\infer{}
{\prop * \All\var.\propB \proves \All\var. \prop * \propB}
\infer{}
{\always(\prop*\propB) \provesIff \always\prop * \always\propB}
\infer{}
{\always(\prop \Ra \propB) \proves \always\prop \Ra \always\propB}
\infer{}
{\always(\prop \wand \propB) \proves \always\prop \wand \always\propB}
\infer{}
{\always(\prop \wand \propB) \provesIff \always(\prop \Ra \propB)}
\infer{}
{\later(\prop \Ra \propB) \proves \later\prop \Ra \later\propB}
\infer{}
{\later(\prop \wand \propB) \proves \later\prop \wand \later\propB}
\infer{}
{\prop \proves \later\prop}
\end{mathparpagebreakable}
\subsection{Persistent assertions}
We call an assertion $\prop$ \emph{persistent} if $\prop \proves \always\prop$.
These are assertions that ``don't own anything'', so we can (and will) treat them like ``normal'' intuitionistic assertions.
Of course, $\always\prop$ is persistent for any $\prop$.
Furthermore, by the proof rules given in \Sref{sec:proof-rules}, $\TRUE$, $\FALSE$, $t = t'$ as well as $\ownGhost\gname{\mcore\melt}$ and $\mval(\melt)$ are persistent.
Persistence is preserved by conjunction, disjunction, separating conjunction as well as universal and existential quantification and $\later$.
\subsection{Timeless assertions and except-0}
One of the troubles of working in a step-indexed logic is the ``later'' modality $\later$.
It turns out that we can somewhat mitigate this trouble by working below the following \emph{except-0} modality:
\[ \diamond \prop \eqdef \later\FALSE \lor \prop \]
Ralf Jung
committed
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
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
This modality is useful because there is a class of assertions which we call \emph{timeless} assertions, for which we have
\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop \]
In other words, when working below the except-0 modality, we can \emph{strip away} the later from timeless assertions.
The following ruels can be derived about except-0:
\begin{mathpar}
\inferH{ex0-mono}
{\prop \proves \propB}
{\diamond\prop \proves \diamond\propB}
\axiomH{ex0-intro}
{\prop \proves \diamond\prop}
\axiomH{ex0-idem}
{\diamond\diamond\prop \proves \diamond\prop}
\begin{array}[c]{rMcMl}
\diamond{(\prop * \propB)} &\provesIff& \diamond\prop * \diamond\propB \\
\diamond{(\prop \land \propB)} &\provesIff& \diamond\prop \land \diamond\propB \\
\diamond{(\prop \lor \propB)} &\provesIff& \diamond\prop \lor \diamond\propB
\end{array}
\begin{array}[c]{rMcMl}
\diamond{\All x. \prop} &\provesIff& \All x. \diamond{\prop} \\
\diamond{\Exists x. \prop} &\provesIff& \Exists x. \diamond{\prop} \\
\diamond\always{\prop} &\provesIff& \always\diamond{\prop} \\
\diamond\later\prop &\proves& \later{\prop}
\end{array}
\end{mathpar}
The following rules identify the class of timeless assertions:
\begin{mathparpagebreakable}
\infer
{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \land \propB}}
\infer
{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \lor \propB}}
\infer
{\vctx \proves \timeless{\prop} \and \vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop * \propB}}
\infer
{\vctx \proves \timeless{\prop}}
{\vctx \proves \timeless{\always\prop}}
\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \Ra \propB}}
\infer
{\vctx \proves \timeless{\propB}}
{\vctx \proves \timeless{\prop \wand \propB}}
\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\All\var:\type.\prop}}
\infer
{\vctx,\var:\type \proves \timeless{\prop}}
{\vctx \proves \timeless{\Exists\var:\type.\prop}}
\axiom{\timeless{\TRUE}}
\axiom{\timeless{\FALSE}}
\infer
{\text{$\term$ or $\term'$ is a discrete OFE element}}
Ralf Jung
committed
{\timeless{\term =_\type \term'}}
\infer
{\text{$\melt$ is a discrete OFE element}}
Ralf Jung
committed
{\timeless{\ownM\melt}}
\infer
{\text{$\melt$ is an element of a discrete CMRA}}
{\timeless{\mval(\melt)}}
\end{mathparpagebreakable}