ghost-state.tex 4.77 KB
 Ralf Jung committed Dec 10, 2017 1 \section{Extensions of the Base Logic}  Ralf Jung committed Oct 10, 2016 2   Ralf Jung committed Oct 22, 2016 3 In this section we discuss some additional constructions that we define within and on top of the base logic.  Ralf Jung committed Oct 10, 2016 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 committed Dec 10, 2017 6 \subsection{Derived Rules about Base Connectives}  Ralf Jung committed Oct 10, 2016 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 committed Nov 28, 2017 38 39 40  \infer{} {\TRUE \proves \plainly\TRUE}  Ralf Jung committed Oct 10, 2016 41 42 \end{mathparpagebreakable}  Ralf Jung committed Nov 28, 2017 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 committed Dec 10, 2017 45 \subsection{Persistent Assertions}  Ralf Jung committed Oct 10, 2016 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 committed Dec 10, 2017 55 \subsection{Timeless Assertions and Except-0}  Ralf Jung committed Oct 10, 2016 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:  Ralf Jung committed Dec 05, 2016 59 $\diamond \prop \eqdef \later\FALSE \lor \prop$  Ralf Jung committed Oct 10, 2016 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.  Ralf Jung committed Feb 02, 2017 65 The following rules can be derived about except-0:  Ralf Jung committed Oct 10, 2016 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  Ralf Jung committed Dec 05, 2016 130 {\text{$\term$ or $\term'$ is a discrete OFE element}}  Ralf Jung committed Oct 10, 2016 131 132 133 {\timeless{\term =_\type \term'}} \infer  Ralf Jung committed Dec 05, 2016 134 {\text{$\melt$ is a discrete OFE element}}  Ralf Jung committed Oct 10, 2016 135 136 137 {\timeless{\ownM\melt}} \infer  Robbert Krebbers committed Dec 10, 2017 138 {\text{$\melt$ is an element of a discrete camera}}  Ralf Jung committed Oct 10, 2016 139 140 141 {\timeless{\mval(\melt)}} \end{mathparpagebreakable}  Ralf Jung committed Oct 06, 2016 142 143 144 145 146 147  %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: