Vladimir_Nesov comments on Open Thread June 2010, Part 4

[Vladimir_Nesov]

Yes, using a formal world simplifies this a lot.