ghost-state.tex 4.77 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$.

Ralf Jung's avatar
Ralf Jung committed
45
\subsection{Persistent Assertions}
46 47 48 49 50 51 52 53 54
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$.



Ralf Jung's avatar
Ralf Jung committed
55
\subsection{Timeless Assertions 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 62 63 64

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.

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 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
\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
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: