XPost: alt.philosophy, comp.theory   
   From: janburse@fastmail.fm   
      
   Hi,   
      
   Well then get an education. Every Gödel   
   sentence G, has a size, doesn't it?   
   The formal analogue of the Liar Paradox,   
      
   except it’s expressed arithmetically:   
      
   G ≡ ∀y¬Proof(y,┌G┐).   
      
   Gödel did explicitly construct a Gödel   
   sentence G in his 1931 paper. He did not   
   claim it was astronomically large,   
      
   nor impossible to write. Now you can do   
   the encoded Liar also with Turing Machines TM:   
      
   1. Fix a formal proof system S (e.g. PA) and   
   an effective enumeration of all proofs.   
   2. Build a TM M(x) that, given a code x, searches   
   for an S-proof of the formula with code a; if it finds   
   M(x) halts <=> exists y Proof(y,x) (i.e. Prov(x)).   
      
   Etc.. etc..   
      
   Bye   
      
   dart200 schrieb:   
   > this shit makes me feel like i'm   
   > stuck in a mad house planet   
   >   
   > undecidability has nothing to do with   
   > computational complexity and the   
   > fact we think the limit to decidability   
   > is bounded by how well we can   
   > bit pack a self-referential turing   
   > machine into a proof is just literal   
   > nonsense   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)