Finitary partial inductive definitions as a general logic

Abstract

We describe how the calculus of partial inductive definitions is used to represent logics. This calculus includes the powerful principle of definitional reflection. We describe two conceptually different approaches to representing a logic, both making essential use of definitional reflection. In the deductive approach, the logic is defined by its inference rules. Only the succedent rules (in a sequent calculus setting - introduction rules in a natural deduction setting) need be given. The other rules are obtained implicitly using definitional reflection. In the semantic approach, the logic is defined using its valuation function. The latter approach often provides a more straightforward representation of logics with simple semantics but complicated proof systems.