Concerning my posting on consistency proofs, in response to Steel: Grigori Mints has informed me that Cohen's proof at Berkeley was not his old reconstruction of the substitution method, but a version of Gentzen's (second) consistency proof. Bill Tait