It would be helpful for the FOM readership to see a discussion of the various proofs of S2S decidability, how they compare, and the best most readable sources. Harvey Friedman http://www.cs.nyu.edu/pipermail/fom/2015-October/019245.html