A finite axiomatisation of inductive-inductive definitions

Research output: Chapter in Book/Report/Conference proceedingOther chapter contribution


Induction-induction is a priciple for mutually defining data types A : Set and B : A Set. Both A and B are defined inductively, and the constructors for A can refer to B and vice versa.
Original languageEnglish
Title of host publicationLogic, Construction, Computation
EditorsUlrich Berger, Diener Hannes, Peter Schuster, Monika Seisenberger
Pages259 - 287
Publication statusPublished - 2012

Publication series

NameOntos mathematical logic
PublisherOntos Verlag


  • inductive-inductive definitions
  • programming
  • mathematical logic

Cite this

Nordvall Forsberg, F., & Setzer, A. (2012). A finite axiomatisation of inductive-inductive definitions. In U. Berger, D. Hannes, P. Schuster, & M. Seisenberger (Eds.), Logic, Construction, Computation (Vol. 3, pp. 259 - 287). (Ontos mathematical logic). https://doi.org/10.1515/9783110324921.259