But, as I had anticipated earlier, higher order abstract syntax gives rise to difficulties when it is combined with inductive definitions. For instance, if you take the standard encoding of l-calculus, which is this with the encoding that we have seen before for terms, then if you take this to be an inductive set because L occurs negatively, this breaks the so called adequacy. So, are we going to loose higher order abstract syntax or induction principles. This would be very bad in a logical framework.

---