I noticed the following in the Simpson posting referred to: "....in the present historical era, the orthodox and almost universally accepted explication of mathematical rigor is formal provability in ZFC, Zermelo-Frankel set theory with the axiom of choice." Sandy