home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #16 / NN_1992_16.iso / spool / sci / logic / 1243 < prev    next >
Encoding:
Text File  |  1992-07-27  |  2.6 KB  |  69 lines
  1. Newsgroups: sci.logic
  2. Path: sparky!uunet!usc!snorkelwacker.mit.edu!thunder.mcrcim.mcgill.edu!triples.math.mcgill.ca!boshuck
  3. From: boshuck@triples.math.mcgill.ca (William Boshuck)
  4. Subject: Re: Equivalence of Strong completeness and categoricity
  5. Message-ID: <1992Jul28.025048.6503@thunder.mcrcim.mcgill.edu>
  6. Sender: news@thunder.mcrcim.mcgill.edu
  7. Nntp-Posting-Host: triples.math.mcgill.ca
  8. Organization: Dept Of Mathematics and Statistics
  9. References: <1992Jul22.205827.16651@cenatls.cena.dgac.fr>
  10. Date: Tue, 28 Jul 92 02:50:48 GMT
  11. Lines: 57
  12.  
  13. In article <1992Jul22.205827.16651@cenatls.cena.dgac.fr> alliot@cenatls.cena.dgac.fr (Jean-Marc Alliot) writes:
  14. >
  15. >Consistency: A system is consistent if, for any wff F, we
  16. >can not have at the same time (F is a theorem) and (not F is a
  17. >theorem). 
  18. >
  19. >Categoricity: a system is categoric if, for any wff F, we have either
  20. >(F is theorem) or (not F is a theorem).
  21. >
  22. >Strong completeness: a system based on a set S of axioms is strongly
  23. >complete if for any wff F, we have either (F is a theorem) or (F added
  24. >to S is an inconsistent system).
  25. >
  26. >
  27. >Now the questions:
  28. >
  29. >1) It seems quite clear that in any system which is a superset of
  30. >propositional calculus Categoricity and Strong completeness are
  31. >equivalent. However a short and clear demonstration would be very much
  32. >welcome.
  33. >
  34. >2) Does the property hold in the general case (I especially think of
  35. >intuitionist logic) ?
  36. >
  37.  
  38. The proof which answers question 1) depends on something
  39. called the deduction theorem which, in turn gives an answer to
  40. the second question. The deduction theorem says that for a
  41. theory T and formulas F,G, that the following inferences (both
  42. top to bottom and bottom to top) are valid
  43.  
  44.                 T,F |- G
  45.               ------------
  46.               T |- F ==> G   .    
  47.  
  48. (I am using |- to denote provability in whatever logic is
  49. under consideration) In some treatments of logic, this is
  50. virtually the definition of implication (perhaps rightly so).
  51. In particular, this rule is valid in intuitionistic, and modal
  52. logics (at least in the more common ones like S4).
  53.  
  54. If T is a theory in a logic which admits the above rule for
  55. implication then we can say the following. First, categoricity
  56. implies strong completeness: Suppose T is categorical. If T |-
  57. F then that's it. Otherwise, T |- ~F in which case T,F |- F &
  58. ~F so T adjoin F is an inconsistent theory. Now, strong
  59. completeness implies categoricity: Again, if F is a theorem
  60. then you're done.  Otherwise, T adjoin F is an inconsistent
  61. theory; that is, T,F |- (false). By the above rule we get
  62. T |- F ==> (false), that is, T |- ~F. 
  63.  
  64. I hope this has been helpful.
  65.  
  66. WHB
  67.  
  68.  
  69.