Re: [CL] Re: Decidability
Norbert,
A Skolem function is actually an unspecified
function. If you have a statement such as
For every prime number x, there exists
a prime number y greater than x,
that implies that there exists one or more
possible functions from x to y. In this case,
there is an uncountably infinite number of
such functions. If you replace the variable
y with a Skolem function f(x), the symbol f
is merely a representative for any of those
possible functions, some of which are primitive
recursive and some of which are not.
But in any case, if a statement is decidable
before you replace any variables with Skolem
functions, it will still be decidable afterwards.
John