# Negation of equality in FOL

I am unsure if there is a rule in FOL that allows me to make this derivation

1. ¬(a = b) Assumption
2. a ≠ b ???

Is this derivation allowed, and if so what notation should I use to justify it?

• I think that 2. is just a notational variant of 1. Identity is a 2-place predicate that is always interpreted in the same way. – Adam Sharpe May 22 '19 at 16:14
• @Adam hmm okay, the reason I ask is because in a derivation I assumed a=b and then derived a contradiction, so by ¬ Introduction I thought it should be ¬(a=b), can I just write a ¬= b instead? – Anon May 22 '19 at 16:27
• Unfortunately, I wouldn't feel comfortable saying for sure without knowing your text, since different texts might be different. But, for example, if you look at the Wikipedia article on first-order logic (en.wikipedia.org/wiki/First-order_logic), a≠b wouldn't even be a well-formed formula. What text are you using? – Adam Sharpe May 22 '19 at 16:51
• It was just in a past paper for my course, the question was determine whether the conclusion can be derived from the premises and if so, derive it. Perhaps the answer was just it cannot be derived because a ¬= b is not a wff. Thanks for your help. – Anon May 22 '19 at 17:00
• a ≠ b is a shorthand for ¬(a = b). a ¬= b instead, is simply wrong: we negate a statement and not a predicate. – Mauro ALLEGRANZA May 22 '19 at 17:45

## 1 Answer

The question is whether the following is a derivation in first-order logic:

1. ¬(a = b) Assumption
2. a ≠ b ???

Rather than being a derivation they are two different ways of formatting the same thing, that a is not equal to b.

One needs to ask whether either way of writing this is a well formed formula (wff) for the logic text that one is using. In the logic textbook forallx, linked below, neither are wff. The authors discuss the issue of equality in section 24.1:

The symbol ‘=’ is a two-place predicate. Since it is to have a special meaning, we will write it a bit differently: we put it between two terms, rather than out front.

This means that they would write a = b, rather than =ab as one might expect from the way predicates are used in the text.

When it comes to negating that equality they write neither ¬(a = b) nor a ≠ b, but rather ¬a = b. Here they explain this syntax using x and p:

This last sentence contains the formula ‘¬x = p’. That might look a bit strange, because the symbol that comes immediately after the ‘¬’ is a variable, rather than a predicate, but this is not a problem. We are simply negating the entire formula, ‘x = p’.

One has to follow whatever syntax one's logic textbook has defined for these wffs.

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/