definability in a FOL Structure

Stream: Lean for teaching

[Mario Carneiro]

The two formulations are equivalent, but the def has an additional definitional equality (not a thing in FOL), and it also doesn't require any risky axioms

[Alexandre Rademaker]

But the latter can be manipulated on proofs. We could eventually have more axioms (or variables)

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

and try to proof things like ∀ n m, ¬ (father n m ∧ brother n m) , right? Using def we lose this clear logic-based approach, am I right?

[Mario Carneiro]

You can prove the axiom using reflexivity

[Mario Carneiro]

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

theorem 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)) :=
iff.rfl

[Mario Carneiro]

you could either prove b1 like that first and then use it in the proof, or elide b1 entirely and just unfold as necessary