ghost-state.tex

\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 Propositions 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. In fact, we can strip away later
from timeless propositions even when working under the later modality:
\begin{mathpar}
  \infer{\timeless{\prop} \and \prop \proves \later \propB}
  {\later\prop \proves \later\propB}
\end{mathpar}