From: fateman@gmail.com   
      
   Regarding Waldek's note -- about the undecidability of central problems in   
   mathematics that require determining whether an expression is zero or not...   
   (Results due to Daniel Richardson, 1968 or so).   
   I don't consider this a design flaw in the systems that people build.  It is a   
   fundamental limitation in the mechanization of mathematics. One that cannot be   
   remedied by a better design.  Unless you design a system that is so   
   constrained (say, to integer    
   arithmetic) that Richardson's results don't hold.   
      
   This issue about mechanization goes back to Russell and Whitehead, and   
   actually a good deal before that.     
   Analogously, Godel's theorem, while in some sense devastating, hardly stopped   
   mathematicians from doing mathematics.   
      
   RJF   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)