Meta-logic

A meta-logic is a logic for reasoning about another logic. When working with STELF, 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 STELF, 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 STELF’s facility used to state and verify totality assertions is the meta-logic used to reason about derivations in object logics.