[FOM] Bounded Arithmetic sufficient for mutual interpretability result?

[Rupert McCallum]

In my PhD thesis I state that the mutual interpretability of ZFC+IC and ZF+DC+"every set of reals is Lebesgue measurable" is provable in Bounded Arithmetic.

Is this correct? It seems as though the interpretation functions from each theory to the other change the lengths of proofs by a linear function, so that my remark should be correct. But maybe I am wrong and Predicative Arithmetic is necessary.

I have asked Edward Nelson and he says he does not know the answer. This may mean that no-one knows the answer.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140325/ed7cce32/attachment-0001.html>