Abstract: | This paper presents an extension of a proof system for encoding generic judgments, the logic FOλΔ of Miller and Tiu, with an induction principle. The logic FOλΔ is itself an extension of intuitionistic logic with fixed points and a “generic quantifier”, , which is used to reason about the dynamics of bindings in object systems encoded in the logic. A previous attempt to extend FOλΔ with an induction principle has been unsuccessful in modeling some behaviours of bindings in inductive specifications. It turns out that this problem can be solved by relaxing some restrictions on , in particular by adding the axiom B≡ x.B, where x is not free in B. We show that by adopting the equivariance principle, the presentation of the extended logic can be much simplified. Cut-elimination for the extended logic is stated, and some applications in reasoning about an object logic and a simply typed λ-calculus are illustrated. |