English
Let A ⊆ M. A subset s of M × M is said to be definable in two dimensions over A if there exists a first-order formula φ in the language L with parameters from A such that for all a,b ∈ M, (a,b) ∈ s if and only if M ⊨ φ(a,b).
Русский
Пусть A ⊆ M. Подмножество s ⊆ M × M называется двумерно определимым над A, если существует формула первого порядка φ в языке L с параметрами из A такая, что для всех a,b ∈ M выполняется: (a,b) ∈ s тогда и только тогда, когда M ⊨ φ(a,b).
LaTeX
$$$\\\\operatorname{Definable}_2(s) \\iff \\exists \\varphi(x,y) \\text{ с параметрами из } A\\text{ так, что } s = \\{(a,b) \\in M \\times M : M \\models \\varphi(a,b)\\}. $$$
Lean4
/-- A 2-dimensional version of `Definable`, for `Set (M × M)`. -/
def Definable₂ (s : Set (M × M)) : Prop :=
A.Definable L {x : Fin 2 → M | (x 0, x 1) ∈ s}
