🚀 go-pugleaf

In article <Bxzvpx.Bp7@cantua.canterbury.ac.nz> wft@math.canterbury.ac.nz (Bill Taylor) 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.
>
>|> 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 ?
>

Bill, what happens is that with that extra constant in the language, some 
quantified sentences of the original language can have quantifier free logical
consequences:

(*)     [ There exists an  x  such that  not  R(0,x) ]  -->  [ P(n) ]

will imply the quantifier free sentence     

(**)    not R(0,c) -->  P(n)
[ only for the n's that satisfy  (*) ].

So if the set of quantifier free sentences of the theory in the new language 
(with no extra axioms, other than logical ones) were recursive, by looking at 
the sentences of the form (**) one could decide membership in the non-recursive
r.e. set we started with.  [ actually the reason to include the axiom R(0,0)
was to avoid this kind of situation for the constant  0 ]. [ By the way, a 
fellow student pointed out that in fact there are no counterexamples if we only
allow new relation symbols in the new language ].