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)
x=y ⇔ y=x (symmetry);
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.
If I have
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?