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 -formulae for propositional variables and is normal if it also contains the axiom schemata:
(K)
(N)
and monotonicity (for each ):
if then .
The smallest normal modal logic with ‘agents’ is K(m). (The diamonds correspond to the 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.