definability in a FOL structure

Stream: Lean for teaching

[Alexandre Rademaker]

In the Mathematical Introduction to Logic (Enderton) one section is devoted to exploring how relations can be defined in a structure using formulas with free variables. In the next section, sentences are used to express the properties of structures (models).

I wonder if we can make any relation between the definition of the relation brother vs the axiomatization of it:

constant U : Type
constant father : U → U → Prop   -- `father x y`
constant mother : U → U → Prop   -- `mother x y`

def brother (i j : U) : Prop :=
  ∃ x, (father x i ∧ (father x j ∨ mother x j)) ∨ (mother x i ∧ (father x j ∨ mother x j))

axiom b1 : ∀ i j, brother i j ↔
 ∃ x, (father x i ∧ (father x j ∨ mother x j)) ∨ (mother x i ∧ (father x j ∨ mother x j))

variables n m : U
#check ∀ n m, ¬ (father n m ∧ brother n m)