Need help with Rules of Identity for First Order Logic with Equality

Question

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?

Answer 1

The quantifiers rules can be more generally specified with terms.

Terms are : variables, contants or "complex" ones (like e.g. x+0 in arithmetic).

The reason why is that every first-order theory has an ulimited supply of variables, while constants are usually few : one or none.

If we consider first-order arithmetic, we have only one constant : 0.

Thus, if we restrict the rules for quantifiers to constants, we are in trouble with e.g. the "instantiation" of the true sentence : ∃x (x ≠ 0).

---

Also the equality rules can be specified with terms :

(=I) : we may derive (t = t) with no assumptions

(=E) : if φ is a formula, s and t are terms substitutable for x in φ, and we have derivations D of (s = t) and D' of φ[s/x], we may derive φ[t/x]. The undischarged assumptions are those of D together with those of D'.

---

With the rule :

from Fx and ¬Fy, derive : ¬(x=y),

you can apply it with Rax as Fx.

Thus, Raa is Fa and ¬Rab is ¬Fb and you can conclude with :

¬(a=b).