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

TL;DR

This paper presents two proofs of the wellfoundedness of recursive notation systems for a0_N-reflecting ordinals, using a0_{N-1}^0-inductive definitions and distinguished classes, advancing the understanding of ordinal notation systems.

Contribution

It introduces two novel proofs of wellfoundedness for recursive notation systems of a0_N-reflecting ordinals, employing different inductive and class-based methods.

Findings

Proof based on a0_{N-1}^0-inductive definitions

Proof based on distinguished classes

Establishment of wellfoundedness for a0_N-reflecting ordinal systems

Abstract

In this paper, we give two proofs of the wellfoundedness of recursive notation systems for $\Pi_N$-reflecting ordinals. One is based on $\Pi_{N-1}^0$-inductive definitions, and the other is based on distinguished classes.