Restrictable Primitives?

Hi all,

In a previous discussion, I came to know that if one add a primitive
one place function symbole F to FOL with identity , then the following
becomes a theorem:

Ax Ey ( y=F(x) )

Three questions:-

First: What is the prove of that?

Second: can we adopt a methodology to restrict that? I mean to
restrict F from ranging over all variables of the language, in such a
manner that for a specific formula Phi :

Ax (Ey(y=F(x)) iff Phi(x))?

I mean can we have another kind of primive concepts , like a
'restrictable primitive function symbole', such that when we say that
F is a restrictable primitive function symbole by Phi , then this
leads to:

Ax (Ey(y=F(x)) iff Phi(x))

Of course if Phi(x) <-> x=x , it is clear that F becomes unrestricted.

Is that possible?

Third: to generalize matters, if such restrictions are possible, then
can this be generalized over other kinds of primitives?

Zuhair



.

Loading