I'm a beginner in logic and I'm studying with textbooks. Right now I've just got to predicate logic with identity and I need to ask a few questions, so I can free my mind of doubts and sleep well at night.
Do the identity rules (Id)
p//x=x (reflexivity);
x=y ⇔ y=x (symmetry);
x=y/y=z//x=z (transitivity);
Fx/x=y//Fy, Fx/¬Fy//¬(x=y) (substitution);
apply to both variables and constants?
I'm almost certain that they do, but there's this textbook that says they only apply to constants, and then a more recent edition of the same book says it apply to both variables and constants. So I just need to be sure.
Another question:
If I have
- Raa
- ¬Rab
can I infer from both premises the line ¬(a=b) with the Id rules, or do I need some intermediate step? Or is it just wrong?
One last question: when doing Existential Instantiation (EI), I know I can replace the variable with a new constant, one that did not appear in the proof in any preceding line and in the conclusion line, and then drop the quantifier; but there's a textbook that says I could instantiate with a variable, providing it's a new one that has not been used, so this mean I can do EI with both variables and constants? I was sure that I could only instantiate with a constant, and that the constant was supposed to be a "temporary name". Can anyone clear this to me?
I'll treat your first and last question at the same time: there are different formal systems of logic, and yes, some will use variables when eliminating quantifiers, where others use constants. For the former kinds of systems, the identity rules apply to those variables as well as constants, but for the latter types of systems, the identity rules only apply to constants.
Then, to infer $\neg a = b$ you probably need to do a proof by contradiction: assume $a=b$, infer $Rab$ by substituting $b$ for the second $a$ in $Raa$, and that contradicts with $\neg Rab$