Так вот, логики-математики, которые не являются кем-то ещё, интересуются только такими аспектами логики, которые "в духе" теории групп, теории колец, теории чисел, (всё остальное, чем типично профессионально занимаются математики).

Как люди придумывали формальные определения для ∈, или оператора принадлежности в теории множеств.

Map theory.

Klaus Grue — Map Theory '1990, §3.6.

Определение принадлежности:

a ∈˙ b = (if b F ∃˙v : a =˙ (b v))

Рекурсивное определение равенства множеств:

x =˙ y = (if x (if y T F) (if y F (∀˙u∃˙v : (x u) =˙ (y v)) ∧˙ (∀˙v∃˙u : (x u) =˙ (y v))))
,

где ∀˙u∃˙v : (x u) =˙ (y v)) ∧˙ (∀˙v∃˙u : (x u) =˙ (y v)) ≡ A = B,

где A = {s(a u) | u ∈ Ф} и B = {s(b v) | v ∈ Ф}

— множества, репрезентируемые строгими хорошо основанными картами a и b,

где s(a u) рассматривается в контексте рекурсивного определения свойства бытия множеством:

s(T) = ∅ и s(f) = {s(f x) | x ∈ Ф}, если f — строгая карта, где Ф — множество хорошо основанных карт

и где f x понимается как f, применённый на x; строгость f значит то, что она является чёрным ящиком; хорошая основанность f значит ∀x1...xn ∈ G ∃n : (f x1...xn) = T, где G — множество карт.

Понятие карты ассоциируется с понятием функции, подробнее и вокруг — в источнике.

В общем, x…