# Help with Rules of Identity of First Order Logic with Equality

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

1. Raa
2. ¬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?

• If you have the rule : "from $Fx$ and $\lnot Fy$ derive : $\lnot (x=y)$", you can apply it with $Rax$ as $Fx$. Thus $Raa$ is $Fa$ and $\lnot Rab$ is $\lnot Fb$ and you can conclude with : $\lnot (a=b)$. – Mauro ALLEGRANZA Nov 3 '16 at 13:53
• But there is no need to have this rule, because it is a simple consequence of the preceeding one (by tautological equivalence between : $(p \land q) \to r$ and $(p \land \lnot r) \to \lnot q$). – Mauro ALLEGRANZA Nov 3 '16 at 15:32
• I see, does this mean relational predicates are no different than monadic predicates when we apply the identity rules? Even if it is an intransitive relation? And about the equivalences you mention how do they relate to the identity rules? – Iconoclasteretic Nov 5 '16 at 6:44

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$
• Your textbooks are not contradictory; they just define the rules differently. And so what you can or cannot do all depends on how the rules are defined for the particular system you decide to use. So yes, maybe there is a system out there that can get the $\neg a = b$ in one step ... but none that I am familiar with. – Bram28 Nov 3 '16 at 0:40