/sci/ - Science & Math

>>9668023
In logic as a binary predicate with some minimal requirements (such as that for any terms x and y, we have that x=y has the same truth value as y=x) and then for each theory, you set up an axiom to derive equality statements.

In a set theory, usually you set up an axiom
∀X. ∀Y. [∀z. (z∈X ⇔ z∈Y) ⇒ X=Y]
saying you can prove, for any two sets X and Y, that when for each item (usually also set) z it's the case that z is in X if and only if it's also in Y (i.e. when they share elements), then X and Y are equal. The allquantors that are part of this definition range over any set in the domain. The domains of discourse is not necessarily part of the model (i.e. also a set).

Here's a list of a few theories - they will usually all come with their own rule to extent equality (beyind the logic rules, like symmetry or transitivity)
https://en.wikipedia.org/wiki/List_of_first-order_theories

One is Robinson arithmetic, in which the x's and y's are not sets but numbers. You must view this syntactically

∀x. ¬ Sx = 0
∀x. ¬ x = 0 → ∃y Sy = x
∀x.∀y. Sx = Sy → x = y
∀x. x + 0 = x
∀x.∀y. x + Sy = S(x + y)
∀x. x * 0 = 0
∀x.∀y. x * Sy = (x * y) + x.
(where, basically, Sx:=x+1)
So for example, using 0 for x and the first axiom, we can prove that "0+1 is not 0" is true.

But of course some theories are more expressive than others and so some may argue you really only need equality for sets and then do modeling.

In other logics, e.g. Matrin-Löf dependent type theory, equality comes with much more rules (computational ones). It's really up to you.