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?


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 :


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.