docs: add empty type and sum

docs/base-logic.tex

@@ -32,18 +32,25 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
 \begin{align*}
   \type \bnfdef{}&
       \sigtype \mid
+      0 \mid
       1 \mid
+      \type + \type \mid
       \type \times \type \mid
       \type \to \type
 \\[0.4em]
   \term, \prop, \pred \bnfdef{}&
-      \var \mid
+      \var \bm\mid
       \sigfn(\term_1, \dots, \term_n) \mid
+      \textlog{abort}(\term) \mid
       () \mid
       (\term, \term) \mid
       \pi_i\; \term \mid
       \Lam \var:\type.\term \mid
       \term(\term)  \mid
+\\&
+      \textlog{inj}_i\; \term \mid
+      \textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var. \term \mid \Ret\textlog{inj}_2\; \var. \term \;\textlog{end} \mid
+%
       \melt \mid
       \mcore\term \mid
       \term \mtimes \term \mid
@@ -67,7 +74,10 @@ Below, $\melt$ ranges over $\monoid$ and $i$ ranges over $\set{1,2}$.
     {\later\prop} \mid
     \upd \prop
 \end{align*}
-Recursive predicates must be \emph{guarded}: in $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.
+Well-typedness forces recursive definitions to be \emph{guarded}:
+In $\MU \var. \term$, the variable $\var$ can only appear under the later $\later$ modality.
+Furthermore, the type of the definition must be \emph{complete}.
+The type $\Prop$ is complete, and if $\type$ is complete, then so is $\type' \to \type$.
 
 Note that the modalities $\upd$, $\always$, $\plainly$ and $\later$ bind more tightly than $*$, $\wand$, $\land$, $\lor$, and $\Ra$.
 
@@ -106,7 +116,10 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
 	}{
 		\vctx \proves \wtt {\sigfn(\term_1, \dots, \term_n)} {\type_{n+1}}
 	}
-%%% products
+%%% empty, unit, products, sums
+\and
+	\infer{\vctx \proves \wtt\term{0}}
+        {\vctx \proves \wtt{\textlog{abort}(\term)}\type}
 \and
 	\axiom{\vctx \proves \wtt{()}{1}}
 \and
@@ -115,6 +128,14 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
 \and
 	\infer{\vctx \proves \wtt{\term}{\type_1 \times \type_2} \and i \in \{1, 2\}}
 		{\vctx \proves \wtt{\pi_i\,\term}{\type_i}}
+\and
+        \infer{\vctx \proves \wtt\term{\type_i} \and i \in \{1, 2\}}
+        {\vctx \proves \wtt{\textlog{inj}_i\;\term}{\type_1 + \type_2}}
+\and
+        \infer{\vctx \proves \wtt\term{\type_1 + \type_2} \and
+        \vctx, \var:\type_1 \proves \wtt{\term_1}\type \and
+        \vctx, \varB:\type_2 \proves \wtt{\term_2}\type}
+        {\vctx \proves \wtt{\textlog{match}\; \term \;\textlog{with}\; \Ret\textlog{inj}_1\; \var. \term_1 \mid \Ret\textlog{inj}_2\; \varB. \term_2 \;\textlog{end}}{\type}}
 %%% functions
 \and
 	\infer{\vctx, x:\type \proves \wtt{\term}{\type'}}
@@ -125,7 +146,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
 	{\vctx \proves \wtt{\term(\termB)}{\type'}}
 %%% monoids
 \and
-        \infer{}{\vctx \proves \wtt\munit{\textlog{M}}}
+        \infer{}{\vctx \proves \wtt\melt{\textlog{M}}}
 \and
 	\infer{\vctx \proves \wtt\melt{\textlog{M}}}{\vctx \proves \wtt{\mcore\melt}{\textlog{M}}}
 \and
@@ -157,7 +178,8 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
 \and
 	\infer{
 		\vctx, \var:\type \proves \wtt{\term}{\type} \and
-		\text{$\var$ is guarded in $\term$}
+		\text{$\var$ is guarded in $\term$} \and
+		\text{$\type$ is complete}
 	}{
 		\vctx \proves \wtt{\MU \var:\type. \term}{\type}
 	}
@@ -286,7 +308,7 @@ This is entirely standard.
 %   {}
 %   {\pfctx \proves \mu\var: \type. \prop =_{\type} \prop[\mu\var: \type. \prop/\var]}
 \end{mathparpagebreakable}
-Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda$ and $\mu$.
+Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\textlog{abort}$, sum elimination, $\lambda$ and $\mu$.
 
 
 \paragraph{Laws of (affine) bunched implications.}
@@ -317,8 +339,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
 {\plainly\prop \proves \always\prop}
 \and
 \begin{array}[c]{rMcMl}
-  \TRUE &\proves& \plainly{\TRUE} \\
-  (\plainly P \Ra \plainly Q) &\proves& \plainly (\plainly P \Ra Q)
+  (\plainly P \Ra \plainly Q) &\proves& \plainly (\plainly P \Ra Q) \\
+\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) &\proves& P =_{\Prop} Q
 \end{array}
 \and
 \begin{array}[c]{rMcMl}
@@ -326,8 +348,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
   \All x. \plainly{\prop} &\proves& \plainly{\All x. \prop} \\
   \plainly{\Exists x. \prop} &\proves& \Exists x. \plainly{\prop}
 \end{array}
-\and
-\infer[PropExt]{}{\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) \proves P =_{\Prop} Q}
+%\and
+%\infer[PropExt]{}{\plainly ( ( P \Ra Q) \land (Q \Ra P ) ) \proves P =_{\Prop} Q}
 \end{mathpar}
 
 \paragraph{Laws for the persistence modality.}
@@ -340,8 +362,8 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
 {\always\prop \proves \prop}
 \and
 \begin{array}[c]{rMcMl}
-  \always{\prop} \land \propB &\proves& \always{\prop} * \propB \\
-  (\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q)
+  (\plainly P \Ra \always Q) &\proves& \always (\plainly P \Ra Q) \\
+  \always{\prop} \land \propB &\proves& \always{\prop} * \propB
 \end{array}
 \and
 \begin{array}[c]{rMcMl}
@@ -358,7 +380,7 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
   {\prop \proves \propB}
   {\later\prop \proves \later{\propB}}
 \and
-\infer[L{\"o}b]
+\inferhref{L{\"o}b}{Loeb}
   {}
   {(\later\prop\Ra\prop) \proves \prop}
 \and

docs/ghost-state.tex

@@ -35,8 +35,13 @@ We collect here some important and frequently used derived proof rules.
 
   \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 assertions}
 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.