# A clarification regarding the Existential Introduction rule

I require clarification on the Existential rule E4 in Eliot Mendelson's Introduction to Mathematical Logic, page 61:

Let $t$ be a term that is free for $x$ in a wf $A(x,t)$, and let $A(t,t)$ arise from $A(x,t)$ by replacing all free occurrences of $x$ by $t$. Then $(\exists x)A(x,t)$ is provable from $A(t,t)$.

I think it might be more commonly known as existential introduction?

When you use the existential rule, for example, if you have a $2$-place predicate $A(x,x)$, do you have to change the variables to terms? Or can they stay variables? And more specifically, if you have a $2$-place predicate $A(x,x)$ can you do this: $(\exists y)A(x,y)$?

-
The «rule E4» is, I guess, some rule in some book you are reading... At the very least, tell us what book that is---ideally, explain the rule and give as much context as is reasonable! –  Mariano Suárez-Alvarez Oct 17 '11 at 7:01
$\rm A(x,x)\implies \exists y: A(x,y)$, yes. Not sure what rule(s) this falls under or whatever you're looking at. –  anon Oct 17 '11 at 7:06
Ahh yes, good point! thanks - It's in Eliot Mendelson's introduction to mathematical logic... to quote him "let 't' be a term that is free for 'x' in a wf 'A(x,t)', and let 'A(t,t)' arise from 'A(x,t) by replacing all free occurances of 'x' by 't'. Then, (Ex)A(x,t) is provable from A(t,t). –  Katie Henebery Oct 17 '11 at 7:12
Thanks for your answers!! –  Katie Henebery Oct 17 '11 at 7:13
Katie, please add all the information to the question itself. –  Mariano Suárez-Alvarez Oct 17 '11 at 7:14