Wellfoundedness proofs by means of non-monotonic inductive definitions II: First order operators

In this paper, we give two proofs of the wellfoundedness of a recursive notation system for ΠN-reflecting ordinals. One is based on distinguished classes, and the other is based on -inductive definitions.