🚀 go-pugleaf

|> >Can anyone give me a counterexample of the following:
|> >
|> >Let T a consistent first order theory with equality which
|> >decidable set of quatifier-free logical consequences:
|> >
|> >  QF(T) = { B  |   t |= B, B quantifier-free }
|> >
|> >Let A be a T-consistent quantifier-free formula.
|> >Then (T,A) is also a consistent first order logic with
|> >equality and QF(T,A) is ALSO DECIDABLE.

|> Solution follows.
|> 
|> Take the theory over the language with one constant  0 , one function  f(x) ,
|> one unary predicate  P(x), and a binary relation  R(x,y), as follows:
|> 
|> For all  x  R(0,f(x))
|> R(0,0)
|> and for each  n  in a non-recursive r.e. set, the axioms:
|> 
|> [ There exists an  x  such that  not R(0,x) ]  -->  [ P(n) ]
|> 
|> (where  n  is the abbreviation of  f(x)  applied  n  times to  0 )
|> 
|> Then one can check that the set of quantifier free sentences that are logical
|> consequences of this axioms is recursive.
|> 
|> However if one expands the language with one more constant  c , and add the
|> sentence   not R(0,c), then that set becomes non-recursive.  [if you dont allow
|> an expansion of the language, then it can be shown that there is no counter-
|> example].

I don't quite get this comment. If the constant c is in the original language,
but with no extra axioms, isn't the original theory still decidable for
quantifier-free formulas ? And thus isn't the example now a counterexample
of the type originally required ?

Help sort me out please, somebody.
------------------------------------------------------------------------------
              Bill Taylor              wft@math.canterbury.ac.nz
------------------------------------------------------------------------------
                       Kleeneness is next to Godelness.
------------------------------------------------------------------------------