## Stream: Lean for teaching

### Topic: definability in a FOL Structure

#### Mario Carneiro (Sep 17 2020 at 22:16):

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 (Sep 17 2020 at 22:32):

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 (Sep 17 2020 at 22:50):

You can prove the axiom using reflexivity

#### Mario Carneiro (Sep 17 2020 at 22:51):

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 (Sep 17 2020 at 22:52):

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

Last updated: Dec 20 2023 at 11:08 UTC