An object logic is a logic encoded as an LF signature, with the intent of studying it with Twelf. The term "logic" is used very broadly here, as it can refer to any deductive system with an abstract syntax and a set of relations that can be encoded in LF. We use the term object language as a synonym. Examples of object logics include arithmetic over natural numbers, a theory of lists, propositional logic, linear logic, or programming languages like the simply-typed lambda calculus.
In general, anything defined using an LF signature is an object logic of some form. The term object logic is used to contrast the logic from the meta-logic used to encode it.
This page is incomplete. We should expand it.