I will allow one more round of general discussion on this topic. After that I will only post messages that, in my opinion, are relevant to the kind of rigorous development that Tim Chow was seeking. Martin Martin Davis Professor Emeritus, Courant-NYU Visiting Scholar, UC Berkeley eipye + 1 = 0