Zulip Chat Archive

Stream: Lean for teaching

Topic: definability in a FOL structure

Alexandre Rademaker (Sep 17 2020 at 20:10):

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)

Last updated: Dec 20 2023 at 11:08 UTC