Logical frameworks such as the Edinburgh LF or Isabelle have concentrated on the traditional logics of mathematical practice, i.e. classical or intuitionistic, propositional, or first- or higher-order logics, which can be given effective encodings in terms of some notion of `truth' consequence. Other logics, however, such as modal logics, introduce intensional elements that can really only be understood in terms of validity.
We discuss how one might extend a traditional logical framework of implies/forall with a new intensional logical connective for validity, which we can use to encode these logics directly.