ghost-state.tex 4.79 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$.  Robbert Krebbers committed Dec 10, 2017 45 46 \subsection{Persistent Propositions} We call a proposition $\prop$ \emph{persistent} if $\prop \proves \always\prop$.  Robbert Krebbers committed Dec 10, 2017 47 These are propositions that do not own anything'', so we can (and will) treat them like normal'' intuitionistic propositions.  Ralf Jung committed Oct 10, 2016 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$.  Robbert Krebbers committed Dec 10, 2017 55 \subsection{Timeless Proposition 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   Robbert Krebbers committed Dec 10, 2017 61 This modality is useful because there is a class of propositions which we call \emph{timeless} propositions, for which we have  Ralf Jung committed Oct 10, 2016 62 $\timeless{\prop} \eqdef \later\prop \proves \diamond\prop$  Robbert Krebbers committed Dec 10, 2017 63 In other words, when working below the except-0 modality, we can \emph{strip away} the later from timeless propositions.  Ralf Jung committed Oct 10, 2016 64   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 \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}  Robbert Krebbers committed Dec 10, 2017 91 The following rules identify the class of timeless propositions:  Ralf Jung committed Oct 10, 2016 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  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: