Kripke-Platek set theory and the anti-foundation axiom (Q2765565)

KPA is the label the author attaches to the theory he considers, namely, the one obtained from Kripke-Platek set theory by replacing the foundation axiom by the anti-foundation axiom, AFA. He shows that (i) KPA and a second-order arithmetic \(\Delta^1_2\text{-CA}_0\) have the same proof-theoretic strength, and (ii) so do KPA+IND\(_\omega\) and \(\Delta^1_2\)-CA, by interpreting one theory into the other. AFA is stated in terms of graph theory. Given a directed graph, a decoration is, by definition, an assignment \(d\) of sets to nodes such that \(d(x)=\{d(y) \mid\exists\) edge from \(x\) to \(y\}\). AFA dictates that a graph has a unique decoration. The author considers graphs based on linear orders on \(\omega\), and shows their being well-ordered is \(\Delta_1\) in KPA.