home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #26 / NN_1992_26.iso / spool / comp / lang / c / 16273 < prev    next >
Encoding:
Internet Message Format  |  1992-11-10  |  2.7 KB
  1. Xref: sparky comp.lang.c:16273 comp.lang.c++:16030 comp.lang.pascal:6461 comp.lang.misc:3569
  2. Path: sparky!uunet!ogicse!decwrl!concert!sas!mozart.unx.sas.com!sasghm
  3. From: sasghm@theseus.unx.sas.com (Gary Merrill)
  4. Newsgroups: comp.lang.c,comp.lang.c++,comp.lang.pascal,comp.lang.misc
  5. Subject: Re: Godel's Proof (was Re: Software design =/= Programming)
  6. Message-ID: <BxIBDz.481@unx.sas.com>
  7. Date: 10 Nov 92 15:37:11 GMT
  8. Article-I.D.: unx.BxIBDz.481
  9. References: <josef.720690811@uranium>     <1992Nov04.073218.11970@cadlab.sublink.org>     <1dcuutINNi8t@agate.berkeley.edu> <1992Nov8.031423.16207@ucc.su.OZ.AU>     <1992Nov9.144550.28811@us-es.sel.de> <LOEGEL.92Nov9134531@fegatello.ssc.gov> <BxHz2v.EK4@sci.kun.nl>
  10. Sender: news@unx.sas.com (Noter of Newsworthy Events)
  11. Organization: SAS Institute Inc.
  12. Lines: 49
  13. Originator: sasghm@theseus.unx.sas.com
  14. Nntp-Posting-Host: theseus.unx.sas.com
  15.  
  16.  
  17. In article <BxHz2v.EK4@sci.kun.nl>, hansm@cs.kun.nl (Hans Mulder) writes:
  18. |> In <LOEGEL.92Nov9134531@fegatello.ssc.gov> loegel@fegatello.ssc.gov (George J. Loegel) writes:
  19. |> >From the McGraw-Hill Dictionary of Science and Technology:
  20. |> >Godel's Proof: Any formal arithmetical system is incomplete in the
  21. |> >sense that, given any consistent set of arithmetical axioms, there are
  22. |> >true statements in the resulting arithmetical system that cannot be
  23. |> >derived from these axioms.
  24. |> >--- end of def ---
  25. |> 
  26. |> This is inaccurate.  Counterexample:
  27. |> 
  28. |> Axioms: all closed first-order arithmetical formulae that are true when
  29. |>         interpreted w.r.t. the natural numbers.
  30. |> Rules of inference: none needed.
  31. |> 
  32. |> This formal system is consistent, since there no formulae F s.t. both F
  33. |> and ~F are true.  It is complete, since there are no _closed_ formulae F
  34. |> s.t. neither F nor ~F is true.
  35. |> 
  36. |> It doesn't fall for G\:odel's Theorem because it is not semi-decidable,
  37. |> i.e. for a given formula F one cannot (in general) decide whether it is
  38. |> an axiom in this system.
  39. |> 
  40. |> --
  41. |> Hope this helps,
  42. |> 
  43. |> Hans Mulder                hansm@cs.kun.nl
  44.  
  45. I don't think it will help this thread.  But you should be commended
  46. for the effort.  Here is an algorithm whose application *will* help:
  47.  
  48.     1. Acquire a copy of _Computability and Logic_ by Boolos
  49.        and Jeffrey.
  50.  
  51.     2. Read it.
  52.  
  53.     3. Do the proofs (i.e., expand the proof sketches into
  54.        full proofs).
  55.  
  56. If you apply this algorithm to its completion you will understand
  57. the relations of completeness, decidability, finite axiomatizability,
  58. truth (in models and the standard model), and related concepts.
  59. It's a lot of fun too.  (Don't cheat now!  Do all the steps.)
  60.  
  61. -- 
  62. Gary H. Merrill  [Principal Systems Developer, C Compiler Development]
  63. SAS Institute Inc. / SAS Campus Dr. / Cary, NC  27513 / (919) 677-8000
  64. sasghm@theseus.unx.sas.com ... !mcnc!sas!sasghm
  65.