ghost-state.tex 4.79 KB
Newer Older
1
\section{Extensions of the Base Logic}
2

Ralf Jung's avatar
Ralf Jung committed
3
In this section we discuss some additional constructions that we define within and on top of the base logic.
4
5
These are not ``extensions'' in the sense that they change the proof power of the logic, they just form useful derived principles.

Ralf Jung's avatar
Ralf Jung committed
6
\subsection{Derived Rules about Base Connectives}
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
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}
Ralf Jung's avatar
Ralf Jung committed
38
39
40

  \infer{}
  {\TRUE \proves \plainly\TRUE}
41
42
\end{mathparpagebreakable}

Ralf Jung's avatar
Ralf Jung committed
43
44
Noteworthy here is the fact that $\prop \proves \later\prop$ can be derived from Löb induction, and $\TRUE \proves \plainly\TRUE$ can be derived via $\plainly$ commuting with universal quantification ranging over the empty type $0$.

45
46
\subsection{Persistent Propositions}
We call a proposition $\prop$ \emph{persistent} if $\prop \proves \always\prop$.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
These are propositions that ``do not own anything'', so we can (and will) treat them like ``normal'' intuitionistic propositions.
48
49
50
51
52
53
54

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$.



55
\subsection{Timeless Proposition and Except-0}
56
57
58

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:
59
\[ \diamond \prop \eqdef \later\FALSE \lor \prop \]
60

61
This modality is useful because there is a class of propositions which we call \emph{timeless} propositions, for which we have
62
\[ \timeless{\prop} \eqdef \later\prop \proves \diamond\prop  \]
63
In other words, when working below the except-0 modality, we can \emph{strip away} the later from timeless propositions.
64

65
The following rules can be derived about except-0:
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
\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}

91
The following rules identify the class of timeless propositions:
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
\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
130
{\text{$\term$ or $\term'$ is a discrete OFE element}}
131
132
133
{\timeless{\term =_\type \term'}}

\infer
134
{\text{$\melt$ is a discrete OFE element}}
135
136
137
{\timeless{\ownM\melt}}

\infer
138
{\text{$\melt$ is an element of a discrete camera}}
139
140
141
{\timeless{\mval(\melt)}}
\end{mathparpagebreakable}

142
143
144
145
146
147


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