home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #27 / NN_1992_27.iso / spool / sci / logic / 2113 < prev    next >
Encoding:
Internet Message Format  |  1992-11-19  |  2.4 KB
  1. Path: sparky!uunet!zaphod.mps.ohio-state.edu!wupost!waikato.ac.nz!canterbury.ac.nz!math!wft
  2. Newsgroups: sci.logic
  3. Subject: Re: Why invalid?
  4. Message-ID: <Bxzvpx.Bp7@cantua.canterbury.ac.nz>
  5. From: wft@math.canterbury.ac.nz (Bill Taylor)
  6. Date: Fri, 20 Nov 1992 03:15:32 GMT
  7. References: <1992Nov16.091653.1@woods.ulowell.edu> <lgfubaINN7v@peaches.cs.utexas.edu> 
  8.  <1992Nov17.164246.18220@uklirb.informatik.uni-kl.de> <1992Nov18.002216.15277@magnus.acs.ohio-state.edu>
  9. Organization: Department of Mathematics, University of Canterbury
  10. Nntp-Posting-Host: sss330.canterbury.ac.nz
  11. Lines: 44
  12.  
  13. |> >Can anyone give me a counterexample of the following:
  14. |> >
  15. |> >Let T a consistent first order theory with equality which
  16. |> >decidable set of quatifier-free logical consequences:
  17. |> >
  18. |> >  QF(T) = { B  |   t |= B, B quantifier-free }
  19. |> >
  20. |> >Let A be a T-consistent quantifier-free formula.
  21. |> >Then (T,A) is also a consistent first order logic with
  22. |> >equality and QF(T,A) is ALSO DECIDABLE.
  23.  
  24. |> Solution follows.
  25. |> 
  26. |> Take the theory over the language with one constant  0 , one function  f(x) ,
  27. |> one unary predicate  P(x), and a binary relation  R(x,y), as follows:
  28. |> 
  29. |> For all  x  R(0,f(x))
  30. |> R(0,0)
  31. |> and for each  n  in a non-recursive r.e. set, the axioms:
  32. |> 
  33. |> [ There exists an  x  such that  not R(0,x) ]  -->  [ P(n) ]
  34. |> 
  35. |> (where  n  is the abbreviation of  f(x)  applied  n  times to  0 )
  36. |> 
  37. |> Then one can check that the set of quantifier free sentences that are logical
  38. |> consequences of this axioms is recursive.
  39. |> 
  40. |> However if one expands the language with one more constant  c , and add the
  41. |> sentence   not R(0,c), then that set becomes non-recursive.  [if you dont allow
  42. |> an expansion of the language, then it can be shown that there is no counter-
  43. |> example].
  44.  
  45. I don't quite get this comment. If the constant c is in the original language,
  46. but with no extra axioms, isn't the original theory still decidable for
  47. quantifier-free formulas ? And thus isn't the example now a counterexample
  48. of the type originally required ?
  49.  
  50. Help sort me out please, somebody.
  51. ------------------------------------------------------------------------------
  52.               Bill Taylor              wft@math.canterbury.ac.nz
  53. ------------------------------------------------------------------------------
  54.                        Kleeneness is next to Godelness.
  55. ------------------------------------------------------------------------------
  56.  
  57.