Meta-logic
From The Twelf Project
A meta-logic is a logic for reasoning about another logic. When working with Twelf, there are two common usages for the term "meta-logic."
The first meaning of this term is "a logic used to encode a object logic." When using Twelf, LF is the meta-logic used to create an adequate encoding of an object logic. When used this way, a meta-logic may also be called a meta-language.
The second meaning of the term is that a meta-logic is a logic in which we state and prove metatheorems. In this case Twelf's facility used to state and verify totality assertions is the meta-logic used to reason about derivations in object logics.
This page is incomplete. We should expand it.
