How to Believe a Twelf Proof

Logical systems are represented in LF by giving a full and faithful (adequate) embedding of the deductive apparatus of the logic as canonical forms of certain types and kinds in LF in specified contexts. The collection of contexts over which the representation is adequate is called a world, because it provides generators for the canonical forms in question. Transferring adequacy from one world to another relies on the concept of subordination, which expresses the irrelevance of any “extra” variables in the target world.