Meta-logic

From The Twelf Project
Jump to: navigation, search

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.