Are these the same in predicate logic with identity:
- ¬ (a = b)
- a ≠ b
I'm not quite sure whether they can be used interchangeably in proofs.
Any help would be great!
Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.
Sign up to join this communityAre these the same in predicate logic with identity:
I'm not quite sure whether they can be used interchangeably in proofs.
Any help would be great!
In classical mathematics these are the same, and indeed more generally the "strike-through" notation is just shorthand for logical negation.
In constructive mathematics, however, my understanding is that in at least some situations the symbol is reserved for an apartness relation. Basically, once we go constructive a mere negated equality isn't very useful; we want some sort of positive distinctness relation. In this situation the symbol "≠" is sometimes used to denote such a relation, and so "a≠b" is different from "¬(a=b)." The former implies the latter, but not conversely in general.
(FWIW I find this use of the symbol "≠" to be confusing, but it does seem standard-ish.)
Although x ≠ y stands for ¬(x = y) to be more reader-friendly in the standard presentations of predicate logic, there is a syntactic distinction between them.
¬(x = y) is the negation of an atomic formula, whereas x ≠ y is the complement (negation) of a binary relation (or, dyadic predicate), which is, when taken positively, called diversity relation. Tarski cites it, together with the universal relation, the empty relation and the identity relation, as a logical notion among binary relations (see Tarski, A.: 1986, ‘What Are Logical Notions?’, edited (with an introduction) by J.Corcoran, History and Philosophy of Logic 7, pp. 143–154).
This fine distinction opens up possibilities for interesting threads of thought that, for example, restrict the semantic reciprocity between {(x, y) | x = y} and {(x, y) | x ≠ y}.
In this connection, it should be remarked that the diversity relation is not an apartness relation in general, and it is a good practice to denote apartness relation by the symbol #.
Noah Schweber already explained that constructive mathematics makes a difference between both formulas. But even in classical logic, we have a choice:
a ≠ b can be the same formula as ¬ (a = b). Then ≠ is just syntactic sugar: We write a ≠ b as an abbreviation for ¬ (a = b) in the same way we write x + y instead of +(x,y) or x < y instead of <(x,y).
Alternatvely, a ≠ b can be a formula that is syntactically different from ¬ (a = b) but semantically equivalent to it. Then the language contains ≠ as an additional predicate symbol, whose semantics is defined in terms of =, using the axiom x ≠ y ⇔ ¬ (x = y).
In standard mathematics, this distinction is irrelevant. But it matters if one takes formulas as syntactic objects: In case 1, a ≠ b is a negated atom with the predicate symbol =, in case 2, it is a non-negated atom with the predicate symbol ≠. Note that both conventions are used (by different authors).