I have a question about the proof system of Per Martin-Löf, developed in his paper "Hauptsatz for the intuitionionistic theory of iterated inductive definitions".
In this paper, Martin-Löf presents a rule-based inductive definition as a set of inference rules to be added to the sequent calculus. Part of the inference rules correspond directly to the rules of the inductive definitions: they serve to infer the heads of rules when the bodies can be be proven. But the remaining inferences rules strongly resemble an induction schema naturally associated with the inductive definition.
Our question is related to the equivalence of Martin-Löf's system, and the standard sequent calculus applied to the infinite predicate theory consisting of the material implications that correspond to the rules of the inductive definition, further extended with the first order induction schema discussed above. Does anybody know of work in which these two systems are equivalent?
It is easy to simulate any proof in Martin-Löf's system in the second system. However, it is less clear how to simulate proofs from the second system in Martin-Löfs system.