2

Are these the same in predicate logic with identity:

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

I'm not quite sure whether they can be used interchangeably in proofs.

Any help would be great!

Improve this question
2
  • 2
    Yes, they are interchangeable. The same applies to other crossed out predicates, like belongs to, etc. – Conifold May 8 '20 at 0:32
  • 1
    @Conifold That's not entirely true - in constructive mathematics, "≠" also seems to be used for apartness relations. – Noah Schweber May 8 '20 at 1:18
5

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.)

Improve this answer
4
  • I'm curious, why the downvote? – Noah Schweber May 8 '20 at 3:24
  • Upvoted! Maybe you could also give a concrete example where a constructive and classical mathematician might disagree about whether we can say that a≠b? – Sofie Selnes May 8 '20 at 6:58
  • 1
    This also happens when a and b represent the outcomes of computations that may or may not be well-founded or convergent. If an algorithmic result a (say a limit of a sequence) does not converge to a value b, so that you know 'not (a=b)', there is always the possibility that 'a' just may or may not have a value, in that case you cannot separate the two values, so it is not true that (a not-equals b). You avoid the latter because it might tempt you to use the difference between a and b to mean something. – hide_in_plain_sight May 8 '20 at 15:55
  • 1
    @SofieSelnes One may not be able to prove constructively that the distance between some two points in a metric space is positive, so that a≠b, but still be able to prove ¬(a=b) by constructive reductio (reducing a=b to a contradiction). – Conifold May 8 '20 at 18:50
4

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 #.

Improve this answer
1
  • +1 - I'm not sure I buy the distinction in the first three paragraphs, but I certainly prefer "#" as a symbol for apartness relations! – Noah Schweber May 10 '20 at 23:22
0

Noah Schweber already explained that constructive mathematics makes a difference between both formulas. But even in classical logic, we have a choice:

  1. 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).

  2. 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).

Improve this answer
11
  • But = has axioms; what are the axioms for ≠ ? – Mauro ALLEGRANZA May 8 '20 at 12:31
  • @MauroALLEGRANZA In the first case, there are no axioms for ≠. The symbol ≠ is not contained in the language; it's just used in examples since it's easier to wrirte and to read for a human. In the second case: x ≠ y ⇔ ¬ (x = y). – Uwe May 8 '20 at 13:05
  • 1
    Clear... but you have changed your text :-) "the language contains ≠ as an additional predicate symbol, whose semantics is defined in terms of =." If we add a new predicate symbol we have to specify axioms for it. – Mauro ALLEGRANZA May 8 '20 at 13:17
  • 1
    @SamuelMuldoon - as per modified answer (my comments regarded the first version of it) a new symbol can be added as (i) an abbreviation (in which case it is a "convention" in the meta-theory: e.g. every time you find a ≠ b read it as ¬ (a = b), or (ii) enlarging the theory with an axiom a ≠ b ↔ ¬ (a = b) – Mauro ALLEGRANZA May 21 '20 at 8:43
  • 1
    Carpenter's workshop ??? The OP posted a question about "logic"... – Mauro ALLEGRANZA May 21 '20 at 8:45

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.