Structuring metatheory on inductive definitions

We examine a problem for machine supported metatheory. There are true state ments about a theory that are true of some (but only some) extensions; howe ver, standard theory-structuring facilities do not support selective inheri tance. We use the example of the deduction theorem for modal logic and show how a statement about a theory can explicitly formalize the closure condit ions extensions should satisfy for it to remain true. We show how metatheor ies based on inductive definitions allow theories and general metatheorems to be organized this way and report on a case study using the theory FSo. ( C) 2000 Academic Press.