Model Theory:`DefinableFun` definition and preimage lemma.

Stream: mathlib4

[Zikang Yu]

I need to handle definable functions and formulas with definable functions a lot so I created and proved the following defintions and lemmas:

def DefinableFun (L : Language) [L.Structure M] (A : Set M) (f : (α → M) → M) : Prop :=
  A.Definable L {v : ((α ⊕ Unit) → M)  | f (v ∘ Sum.inl) = v (Sum.inr ())}

def DefinableMap (L : Language) [L.Structure M] (A : Set M) (F : (α → M) → (β → M)) : Prop :=
  ∀ i : β, DefinableFun L A (fun x => F x i)

lemma definable_exists_fintype [Finite β] {A : Set M} {S : Set ((α ⊕ β) → M)}
    (hS : A.Definable L S) :
    A.Definable L { v : α → M | ∃ u : β → M, Sum.elim v u ∈ S } := by ...

lemma definable_preimage_of_definableMap
    {α β : Type} [Finite β] {A : Set M}
    {F : (α → M) → (β → M)} (hF : DefinableMap L A F)
    {S : Set (β → M)} (hS : A.Definable L S) :
    A.Definable L { v : α → M | F v ∈ S } := by ...

You can check full details and some other lemmas in my repo of definablity-refactor branch.

I have a few questions regarding this approach:

1. Existing Code: Is there already a similar or more general form of DefinableFun and the preimage lemma in Mathlib that I might have missed?

2. Design for Mathlib: Is this design suitable for Mathlib? Should I do some modification or add something missing?

3. API Suggestions: If this is the right direction, what other "must-have" corollaries or utility lemmas would you expect to see derived from definable_preimage to make the API more usable? (e.g., composition, graphs, fibers?)

Any feedback or pointers would be greatly appreciated!

[Dexin Zhang]

That's an impressive work! I'd like to see them PRed to mathlib and I'd like to review them :slight_smile:

[Dexin Zhang]

Zikang Yu said:

1. Existing Code: Is there already a similar or more general form of DefinableFun and the preimage lemma in Mathlib that I might have missed?

No, as far as I know there is no "preimage of a definable set is definable" result in Mathlib. #26332 gives a similar API for definable functions, but it's for functions definable by a term.

[Dexin Zhang]

One question come up in my mind is your definition of DefinableMap. How is it compared to this one?

def DefinableMap (L : Language) [L.Structure M] (A : Set M) (F : (α → M) → (β → M)) : Prop :=
  A.Definable L {v : ((α ⊕ β) → M)  | f (v ∘ Sum.inl) = v ∘ Sum.inr}

[Dexin Zhang]

Zikang Yu said:

3. API Suggestions: If this is the right direction, what other "must-have" corollaries or utility lemmas would you expect to see derived from definable_preimage to make the API more usable? (e.g., composition, graphs, fibers?)

I think we could have the following things also:

1. if f and s is definable, then image f '' s and preimage f ⁻¹' s is definable (you already have this);
2. if f and g are definable, then {x | f x = g x} is definable.

I think any results that you feel can be used to automatically derive definability should be added. A future PR could add them into aesop rules and provide a definablility tactic.

[Zikang Yu]

@Dexin Zhang Thanks for your appreciation!

Dexin Zhang 說：

functions definable by a term.

Yeah I proved this as well with my definition.

Dexin Zhang 說：

One question come up in my mind is your definition of DefinableMap. How is it compared to this one?

def DefinableMap (L : Language) [L.Structure M] (A : Set M) (F : (α → M) → (β → M)) : Prop :=
  A.Definable L {v : ((α ⊕ β) → M)  | f (v ∘ Sum.inl) = v ∘ Sum.inr}

This is more general and when β is finite, I believe it could be proved to be equivalent to my definition using my lemmas.

Dexin Zhang 說：

{x | f x = g x} is definable.

This is a good example of applying my preimage lemma. Suppose f and g are definable n-ary functions. Then we can construct F : (Fin n → M) → (Fin 2 → M) to map an n-tuple v to 2-tuple (f v, g v). Clearly {v : Fin 2 → M | v 0 = v 1} is definable. Then we can use lemma and complete the proof by checking definitional equality.

[Dexin Zhang]

Zikang Yu said:

Dexin Zhang 說：

{x | f x = g x} is definable.

This is a good example of applying my preimage lemma. Suppose f and g are definable n-ary functions. Then we can construct F : (Fin n → M) → (Fin 2 → M) to map an n-tuple v to 2-tuple (f v, g v). Clearly {v : Fin 2 → M | v 0 = v 1} is definable. Then we can use lemma and complete the proof by checking definitional equality.

That makes sense. So {x | f x = g x} would be a useful corollary of the preimage lemma.

[Dexin Zhang]

Zikang Yu said:

Dexin Zhang 說：

One question come up in my mind is your definition of DefinableMap. How is it compared to this one?

def DefinableMap (L : Language) [L.Structure M] (A : Set M) (F : (α → M) → (β → M)) : Prop :=
  A.Definable L {v : ((α ⊕ β) → M)  | f (v ∘ Sum.inl) = v ∘ Sum.inr}

This is more general and when β is finite, I believe it could be proved to be equivalent to my definition using my lemmas.

I agree with that. I'm not sure which definition is more natural in model theory. One advantage of the alternative version would be that you can show the definability of preimage without asserting Finite β, but the disadvantage is that every DefinableMap can only be nontrivial on a finite set of β.

[Zikang Yu]

The PR #32744 is created. It is hard to decide the location of new imports. I'm not sure if DefinableFun should be a new module.