Need Help With a Derivation Involving Universal Quantifiers

Hi!

I'm trying to teach myself logic, using Suppes' *Introduction to Logic*, which seems to be a great book, but it unfortunately comes without any solutions to the exercises (Worried) Well, and now I'm stuck with the following exercise:

"If one man is the father of a second, then the second is not father of the first. Therefore, no man is his own father." (or read it on google; I was able to solve most of them, except 3,4,9, and 10).

How do you solve that? Any help is greatly appreciated!

Mirko

Re: Need Help With a Derivation Involving Universal Quantifiers

Quote:

1) (x)(y)[Fxy -> ~Fyx].........assumpsion

2) (y)[Fxy -> ~Fyx]........from 1 and using Univ.Elimination,where we put x=x We could put x=a

3) [Fxx -> ~Fxx]........from 2 and using Univ.Elimin.,where we put y=x

This is a really old thread, but I was stuck on this problem as well. I don't understand how we can use Universal Specification (or Univeral Elimination) on the variables x and y, and have them both be x? Shouldn't they be different variables? When Univ. specification is used, when should the variables be the same, and when should they be different?

If someone could clarify this, that would be most appreciated!

Re: Need Help With a Derivation Involving Universal Quantifiers

Universal elimination can instantiate a variable with any term whatsoever (as long as the term's free variables do not become bound after the substitution). Nothing prevents instantiating both and in with .

I am not sure the derivation in post #9 is correct, though. First, existential elimination on should be done first, and it is with that that the universal variables should be instantiated. Second, step 7 uses universal introduction on the variable that is still free in the open assumption in step 5.