arXiv · 2101.05878
Solovay's Relative Consistency Proof for FIM and BI
Abstract
In 2002 Robert Solovay proved that a subsystem BI of classical second order arithmetic, with bar induction and arithmetical countable choice, can be negatively interpreted in the neutral subsystem BSK of Kleene's intuitionistic analysis FIM using Markov's Principle MP. Combining this result with Kleene's formalized recursive realizability, he established (in primitive recursive arithmetic PRA) that FIM + MP and BI have the same consistency strength. This historical note includes Solovay's original proof, with his permission, and the additional observation that Markov's Principle can be weakened to a double negation shift axiom consistent with Brouwer's creating subject counterexamples.
Explore related subjects
Keep this discovery
Joan Rand Moschovakis. 2021-01-14. Solovay's Relative Consistency Proof for FIM and BI. https://arxiv.org/abs/2101.05878
Cite the original work for its findings. Save a collection to share your selection of sources.