PREDICATE LOGIC EXAMPLEI cant embed images but I've tried to link it if you can see it but if not then ill type part of the proof here:
- p(x) ^ r(x,y)
- r(x,y)
- Ǝy.r(x,y)
so from line 1 to 2, we used the OR elimination right rule and then from line 2 to 3 we use the "exists introduction" rule - IMAGE OF EXISTS INTRODUCTION RULE However the condition of that rule is that "the free variable (t) must not clash with the bound variable of P". so my question is doesn't the introducing Ǝy make the y in r(x,y) clash?