**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

In (modal) logic, a proposition $p$ is **stable** under a modality $\diamond$ if $p \equiv \diamond{p}$. If $\diamond$ is monadic?, then $p$ is stable iff $p \equiv \diamond{q}$ for some $q$.

(In terms of modal type theory and propositions as types this means that $p$ is a *modal type*.)

In intuitionistic logic, the default is the double negation modality $\neg\neg$. Since $p \Rightarrow \neg\neg{p}$ regardless, $p$ is stable iff $\neg\neg{p} \Rightarrow p$. Being stable is weaker than being decidable; however, if every proposition is stable, then every proposition is decidable and the logic becomes classical. (This is because $p$ is decidable iff $p \vee \neg{p}$ is stable.) Double negation is monadic, so by the previous paragraph, $p$ is stable iff $p \equiv \neg\neg{q}$ for some $q$; in fact, $p$ is stable iff $p \equiv \neg{q}$ for some $q$. (I guess that this has to do with negation forming a monadic adjunction with itself, or something like that.) In the topological semantics? of intuitionistic logic (where propositions correspond to open sets), the stable propositions correspond to the regular open sets.

In the internal language of a category of sheaves $Sh(X)$, a proposition $p$ is $\neg\neg$-stable iff it is enough for $p$ to hold on a dense open subset of $X$ to be able to conclude that $p$ holds on the whole of $X$. For instance, the proposition $f = 0$ about a section $f$ of the sheaf of real functions on $X$ is $\neg\neg$-stable.

Last revised on January 27, 2014 at 09:37:49. See the history of this page for a list of all contributions to it.