A finite axiomatisation of inductive-inductive definitions

Nordvall Forsberg, Fredrik and Setzer, Anton; Berger, Ulrich and Hannes, Diener and Schuster, Peter and Seisenberger, Monika, eds. (2012) A finite axiomatisation of inductive-inductive definitions. In: Logic, Construction, Computation. Ontos mathematical logic, 3 . De Gruyter, 259 - 287. ISBN 9783110324921 (https://doi.org/10.1515/9783110324921.259)

Full text not available in this repository.Request a copy

Abstract

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.