Solovay's Relative Consistency Proof for FIM and BI

TL;DR

This paper discusses Solovay's proof that certain subsystems of second-order arithmetic are equally consistent, using interpretability and Markov's Principle, with historical context and potential weakening of assumptions.

Contribution

It presents Solovay's original proof linking BI and FIM with Markov's Principle, and explores weakening Markov's Principle to a double negation shift.

Findings

FIM + MP and BI share the same consistency strength.

Solovay's proof uses interpretability and Markov's Principle.

Markov's Principle can be weakened to a double negation shift.

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.