# 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

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$

• I see, but I need to know if those rules apply to either variables or constants in systems of natural deduction, like the one I'm using. I just have contradictory information in the textbooks I'm using, and they seem to be about the same system. Also, are you sure there's no way to get to ¬(a=b) with a direct derivation using the Id rules? – Iconoclasteretic Nov 3 '16 at 0:34
• 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
• Well, I've checked three different editions of the same textbook, and up to the 11th edition the author was defining the rules of identity saying that they only apply to constants, then on the 12th edition it was saying that they apply to both constants and variables. Perhaps it was a mistake that took him eleven editions to notice. – Iconoclasteretic Nov 3 '16 at 0:55
• Perhaps ... though maybe the author changed the system. What in general is highly unlikely though, is that the system would be incomplete, meaning that valid arguments can't be proven to be valid in the system. That would be quite embarrassing to the author, so logicians will take care that their system is complete before they put it in print. So do you think the system up to the 11th edition was incomplete? – Bram28 Nov 3 '16 at 1:03
• I think it was a mistake. The 11th edition has an exercise where you need to derive x = c, from x = a and a = c, thus the rule is applied to both variables and constants, but he still clearly states in the chapter that the rule applies only to constants. – Iconoclasteretic Nov 5 '16 at 6:50

This answer is to only part of the question. It is similar to what Bram28 suggested although it places the steps in a proof checker:

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?

Here is a proof:

I can use the assumed equality on line 3 to make the substitution in line 2 which allows me to derive line 4. That leads to a contradiction (line 5) allowing me to negate the assumed equality.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/