We study OST and some of its most important extensions primarily from a proof-theoretic perspective, determine their consistency strengths by exhibiting equivalent systems in the realm of traditional set theory and introduce a new and interesting extension of OST which is conservative over ZFC.