\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. 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} \infer{} {\TRUE \proves \plainly\TRUE} \end{mathparpagebreakable} 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$. \subsection{Persistent Propositions} We call a proposition $\prop$ \emph{persistent} if $\prop \proves \always\prop$. These are propositions that do not own anything'', so we can (and will) treat them like normal'' intuitionistic propositions. 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 Proposition 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$ This modality is useful because there is a class of propositions which we call \emph{timeless} propositions, 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 propositions. The following rules 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 propositions: \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}} {\timeless{\term =_\type \term'}} \infer {\text{$\melt$ is a discrete OFE element}} {\timeless{\ownM\melt}} \infer {\text{$\melt$ is an element of a discrete camera}} {\timeless{\mval(\melt)}} \end{mathparpagebreakable} %%% Local Variables: %%% mode: latex %%% TeX-master: "iris" %%% End: