Solovay’s Relative Consistency Proof for FIM and BI
Joan Rand Moschovakis · Notre Dame Journal of Formal Logic · 2021
In his own words, this historical note documents Robert Solovay’s argument in 2002 that a classical system BI with arithmetic comprehension and bar induction is equiconsistent, over primitive recursive arithmetic PRA, with Kleene’s formal system FIM for intuitionistic analysis plus Markov’s Principle.