🚀 go-pugleaf

In article <1992Nov17.164246.18220@uklirb.informatik.uni-kl.de> ayala@uklirb.informatik.uni-kl.de (Mauricio Ayala R.) writes:

>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.
>
>M. Ayala
>Universitaet Kaiserslautern
>FRG
>ayala@informatik.uni-kl.de
>

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].