Σ11 Choice in a Theory of Sets and Classes
Gerhard Jäger, Jürg Krähenbühl · 2010
Dedicated to Wolfram Pohlers on his retirement Several decades ago Friedman showed that the subsystem Σ1 1-AC of second order arithmetic is proof-theoretically equivalent – and thus equiconsistent – to (Π1 0-CA)<ε0. In this article we prove the analogous result for Σ1 1 choice in the context of the von Neumann-Bernays-Gödel theory NBG of sets and classes.