**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**

A modal logic is **uniform** if it is closed under the rule of uniform substitution of $\mathcal{L}_\omega(n)$-formulae for propositional variables and is **normal** if it also contains the axiom schemata:

(K) $\Diamond_i(\psi \vee \chi) \to \Diamond_i(\psi)\vee \Diamond_i(\chi)$

(N) $\neg \Diamond_i(\bot)$

and monotonicity (for each $i$):

if $\psi \to \chi \in \Lambda$ then $\Diamond_i \psi \to \Diamond_i \chi \in \Lambda$.

The smallest normal modal logic with $m$ ‘agents’ is K(m). (The diamonds correspond to the $M_i$ of that entry.)

Last revised on October 24, 2012 at 12:20:52. See the history of this page for a list of all contributions to it.