home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #16 / NN_1992_16.iso / spool / sci / logic / 1245 < prev    next >
Encoding:
Text File  |  1992-07-27  |  2.6 KB  |  78 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!munnari.oz.au!bunyip.cc.uq.oz.au!cltr.uq.OZ.AU!gar
  3. From: gar@cltr.uq.oz.au (Greg Restall)
  4. Subject: Re: Equivalence of Strong completeness and categoricity
  5. Message-ID: <1992Jul28.060932.29412@cltr.uq.OZ.AU>
  6. Sender: news@cltr.uq.OZ.AU (Mr. Time Waster)
  7. Nntp-Posting-Host: lingua.cltr.uq.oz.au
  8. Organization: Centre for Language Teaching and Research, Uni of Queensland, AUSTRALIA.
  9. References: <1992Jul22.205827.16651@cenatls.cena.dgac.fr> 
  10.     <1992Jul28.025048.6503@thunder.mcrcim.mcgill.edu>
  11. Date: Tue, 28 Jul 1992 06:09:32 GMT
  12. Lines: 64
  13.  
  14. boshuck@triples.math.mcgill.ca (William Boshuck) writes:
  15.  
  16. * The proof which answers question 1) depends on something
  17. * called the deduction theorem which, in turn gives an answer to
  18. * the second question. The deduction theorem says that for a
  19. * theory T and formulas F,G, that the following inferences (both
  20. * top to bottom and bottom to top) are valid
  21. *
  22. *                T,F |- G
  23. *              ------------
  24. *              T |- F ==> G   .    
  25. *
  26. * (I am using |- to denote provability in whatever logic is
  27. * under consideration) In some treatments of logic, this is
  28. * virtually the definition of implication (perhaps rightly so).
  29. * In particular, this rule is valid in intuitionistic, and modal
  30. * logics (at least in the more common ones like S4).
  31.  
  32. Pretty good so far...
  33.  
  34. * If T is a theory in a logic which admits the above rule for
  35. * implication then we can say the following. First, categoricity
  36. * implies strong completeness: Suppose T is categorical. If T |-
  37. * F then that's it. Otherwise, T |- ~F in which case T,F |- F &
  38. * ~F so T adjoin F is an inconsistent theory. 
  39.  
  40. But not here.  
  41.  
  42. It's not that it's in *error*, but just that it's not
  43. so general.  There are plenty of good logics (like R,
  44. R-W, Linear Logic, and so on), that satisfy modus ponens
  45. and the deduction theorem (in the way you describe), 
  46. but that don't validate the move:
  47.  
  48.      A |- C
  49.     --------  (Weakening; or K)
  50.     A,B |- C
  51.  
  52. which you need (in some form) to get from T |- ~F to 
  53. T,F |- F & ~F.
  54.  
  55. The reason you might want to get rid of the offending
  56. principle is to invalidate the offensive
  57.  
  58.      |- C
  59.     -------
  60.     |- B->C
  61.  
  62. which is invalid in all of the systems mentioned above,
  63. and frankly, which *ought* to be invalid, on many sensible
  64. readings of `->'.
  65.  
  66. Relevantly yours,
  67.  
  68. Greg Restall
  69.  
  70.  
  71. --
  72. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
  73. Greg Restall        Philosophy Department, University of Queensland.   
  74. gar@cltr.uq.oz.au   Queensland, 4072.  Australia.                 
  75. - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
  76. The day logic stops being fun is the day it ceases to be my profession.
  77.                                -- Bob Meyer
  78.