home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / math / 14993 < prev    next >
Encoding:
Text File  |  1992-11-15  |  7.2 KB  |  172 lines

  1. Newsgroups: sci.math
  2. Path: sparky!uunet!convex!darwin.sura.net!paladin.american.edu!news.univie.ac.at!email!mips.complang.tuwien.ac.at!rz
  3. From: rz@mips.complang.tuwien.ac.at (Richard Zach)
  4. Subject: Re: Logic and Mathematicians (quite long)
  5. Message-ID: <1992Nov15.150408.18663@email.tuwien.ac.at>
  6. Sender: news@email.tuwien.ac.at
  7. Nntp-Posting-Host: mips.complang.tuwien.ac.at
  8. Reply-To: zach@csdec1.tuwien.ac.at
  9. Organization: Technische Universit"at Wien
  10. References:  <1992Nov13.090126.7142@jarvis.csri.toronto.edu>
  11. Distribution: sci.math
  12. Date: Sun, 15 Nov 1992 15:04:08 GMT
  13. Lines: 157
  14.  
  15. In article <1992Nov13.090126.7142@jarvis.csri.toronto.edu>, leemike@eecg.toronto.edu (Michael Lee) writes:
  16. |> re: zelany's reponse to zach@csdec1.tuwien.ac.at:
  17. |> note: `>' represents the statements of zach@csdec1.tuwien.ac.at
  18. |>       `|' represents some of zelany's statements
  19. |> 
  20. |> I'm working from zelany's posting (see above).  Hence, if I have 
  21. |> misinterpreted the originator of this thread, feel free to correct
  22. |> any errors.
  23.  
  24. |> >Examples: G"odel's Incompleteness Theorems:
  25. |> >He INVENTED the concepts of undecidability of
  26. |> >a sentence in a theory and of incompleteness.
  27. |> 
  28. |> In full, Godel's paper, `On Formally Undecidable Propositions
  29. |> of Principia Mathematica and Related Systens', dealt with the
  30. |> problem of consistency of a given set of axioms and the transformation
  31. |> rules of a given system, i.e., these axioms and the transformation
  32. |> rules do not lead to a theorem which is both true and false.
  33.  
  34. My point was that that was what G"odel did only marginally
  35. deal with. What it REALLY is about, imho, is the arithmetization
  36. of formal systems--G"odel numbering--and, complementary to what he
  37. did in his dissertation, about the relation between truth and
  38. provablity in arithmetic: while his completeness theorem
  39. says that whatever is logically true is provable in prdeicate
  40. logic, his (first) incompleteness theorem says that there are
  41. true sentences of arithmetic which are not provable in a
  42. formal system of arithmetic. The unprovability of consistency
  43. is a corollary to that.
  44.  
  45. [some background deleted]
  46.  
  47. |> >The interesting sentence (from the logical, and
  48. |> >also from G"odels standpoint) is the FIRST
  49. |> >incompleteness theorem (Why else did G"odel
  50. |> >entitle his paper "On undeciadable propositions"?
  51. |> >If he were interested more in consistency,
  52. |> >he would have titled it "The Unprovability of
  53. |> >Consistency" or something).
  54. |> 
  55. |> Your suggestion, i.e., the latter title would of implied something Godel
  56. |> did not prove.
  57.  
  58. Ok, ok: "The formal unprovability of consistence" or
  59. "Artithmetic does not prove itself consistent" or 
  60. "Hilbert's Program fails" or whatever
  61.  
  62. [description of consistency proofs deleted]
  63.  
  64. |> Also, it wouldn't really solve the
  65. |> question at hand, inference rules more powerful than simple arithmetical
  66. |> calculus may lead us to doubt the consistency in the reasoning itself 
  67. |> shifting our focus from the consistency of the axioms to the consistency of
  68. |> the reasoning.
  69.  
  70. After all, maybe propositional logic is inconsistent :-)
  71.  
  72. |> Whatever Godel's initial intent may be, his paper isn't
  73. |> trying to disprove axiomatic consistency but map-out the boundaries, its
  74. |> limits.
  75.  
  76. Hm. Did I say this? I dont think I did.
  77.  
  78. |> >From the mathematician's
  79. |> >viewpoint, the proof is trivial: A simple
  80. |> >diagonalization argument (in Kreisel's words).
  81. |> 
  82. |> I'm not certain of your term `simple diagonalization.'  From my perspective,
  83. |> I found the proof difficult to read and understand, I found nothing
  84. |> trivial about his proof.  He completely arithmetized a formal calculus
  85. |> and established a one-to-one correspondence between the expressions
  86. |> of a calculus and a particular subset of integers.
  87.  
  88. That was exactly my point: *G"odel numbering* is his big contribution
  89. there. As soon as you know how to do that (and I do not consider
  90. G"odel numbering a difficult concept per se), and you know
  91. what a diagonalization argument is, it is easy to obtain the
  92. result.
  93.  
  94. |> [deli service analogy deleted]
  95.  
  96. |> If the triviality of
  97. |> an idea is based on its most banal application then all of mathematics
  98. |> fall under the general heading of banality.     
  99.  
  100. Hm? All of mathematics is banal? or trivial?
  101. I dont get your point.
  102.   
  103. |> >Yet, Hilbert (and others) were very much taken by
  104. |> >surprise. In a sense, incompleteness says:
  105. |> >"The concept of consistency is not important"
  106. |> 
  107. |> Why wouldn't he be surprised?
  108. |> Godel demonstrated that his proposal
  109. |> on a finistic absolute proof for every deductive system is highly
  110. |> unlikey.  Godel, also, showed that inifinite bits of true arithmetical
  111. |> expression can not be formally be deduced from a given set axioms by a
  112. |> closed set of inference rules.  Yet still, the concept of consistency is
  113. |> possible along Hilbert's proposal; Godel proof doesn't logically conclude
  114. |> the impossibility of `consistency' nor does it directly address the 
  115. |> importance, or the lack thereof, of `consistency'.  Although, Godel
  116. |> didn't say Hilbert's proposal was impossible, he did flesh out its
  117. |> intractable characteristics.
  118.  
  119. What else does the 2nd theorem say, if not that Hilbert's Program is
  120. impossible? Could you please explain to me how an elementary proof
  121. of consistency of PA would work in spite of the 2nd Incompleteness Thm?
  122.  
  123. The importance of consistency was never questioned (sorry for being
  124. imprecise), but the importance of elementary proofs of consistency.
  125. And G"odel's results say that that is the wrong question to
  126. ask: after all, there is no answer.
  127.  
  128. |> Suffice to say, consistency for a mathematician or a logician is important; 
  129. |> what would be the point, if it was otherwise?
  130.  
  131. [stuff about V=L and CH deleted]
  132.  
  133. |> >The undecidability of predicate logic from
  134. |> >Turing's work: The really important part of his
  135. |> >paper were the "Computable Numbers", not 
  136. |> >the "Application to the Entscheidungsproblem".
  137. |> >And he MADE UP Turing machines etc. Again,
  138. |> >easy theorems, difficult concepts requiring
  139. |> >deep insight.
  140. |> 
  141. |> |You can add Church and Kleene to the same list.
  142.  
  143. |> I think you're talking of the first-order predicate logic, which was
  144. |> shown to be complete by Godel and then undecidable by Church and
  145. |> Turing by different methods.
  146.  
  147. |> >Gentzen's sequent calculus: his invention. Totally
  148. |> >disconnected from anything that had been done before.
  149. |> >Required deep insight into the nature of logic
  150. |> >to come up with. The "problems", eg, Herbrand's
  151. |> >Theorem, were easy corollaries of the Hauptsatz,
  152. |> >which, in itself, was easy to prove. But how do
  153. |> >you come up with the Hauptsatz in the first place?
  154. |> 
  155. |> How is Gentzen's work totaly disconnected from anything?
  156.  
  157. In the sense that he came up with something new which, at
  158. least at first sight, does not have anything to do with
  159. what had been done before. He didnt solve an open problem.
  160. He made up the sequent clculus, then proved some things
  161. about it. It was as if someone came up with an abstruse
  162. algebraic structure, proved some theorems about it,
  163. and the sole motivation for why anyone should consider
  164. it is because you can do certain things with it which
  165. you can also do with other means. 
  166.  
  167. [questions deleted]
  168.  
  169. -- 
  170. Richard Zach                         Technische Universitaet Wien
  171. [zach@csdec1.tuwien.ac.at]     Abteilung fuer Formale Logik 185.2
  172.