Constraining `Sigma` types, and ModelTheory.Semantics setup

Stream: mathlib4

[Shaopeng]

Dear community,
I have some questions in the two captioned topics that could really use your wisdom.
They are recorded in the comments of the following code snippet that I wrote.

import Mathlib.ModelTheory.Basic
import Mathlib.ModelTheory.Syntax
import Mathlib.ModelTheory.Semantics
import Mathlib.Combinatorics.Quiver.Basic
set_option linter.unusedVariables false

open FirstOrder
universe u v w x y
variable (𝓛: Language.{u, v}) (T: 𝓛.Theory) (β : Type v)(γ: Type w)(M A: Type y)[𝓛.Structure A]
#check Π (N : Type x)[𝓛.Structure N][N ⊨ T], Set (N → N)
/- A term of the type above is a dependent type function that given any 𝓛 Structure N modeling T,
returns a set of maps N → N. -/
def Trivial_Func : Π (N : Type x)[𝓛.Structure N][N ⊨ T], Set (N → N)
 := λ (N: Type x) => ∅


#check Σ (N : Type x), Set (N → N)
/- A term of this type is a dependent-type pair. However: -/
/-! #check Σ (N : Type x)[𝓛.Structure N][N ⊨ T], Set (N → N)
Question 1: The line above gets Unexpected token `[`.
How do I make a dependent-type pair that successfully imposes some conditions
on the 1st component, if possible? -/


/- Question 2: I am also confused about why the assertion
"an instance 𝓜 of `𝓛 structure defined on M` models the 𝓛 theory T"
is not a well-typed Proposition. That is,
why do the last lines below get "overloaded errors" and how to fix?
-/
#check (A ⊨ T) ∨ (T.Model A) /-Prop.
- As declared in Line 9 above, `A` is promised to assume a certain 𝓛 Structure. -/
variable (𝓜: 𝓛.Structure M) /- 𝓜 is an 𝓛.Structure defined on M-/
#check 𝓜.funMap
#check 𝓜.RelMap
/-! #check 𝓜 ⊨ T
#check T.Model 𝓜 both got "overloaded errors." Shouldn't 𝓜 ⊨ T make sense?

Question 2.5: If it is preferred to declare 𝓛-structures using brackets like
`variable (A: Type w)[𝓛.Structure A]` rather than `𝓜: 𝓛.Structure M`, which seems to be
what most theorems in `Mathlib.ModelTheory.Semantics` are doing, how to avoid caveats
like "can't pass constraint to 1st component" in Question 1? -/

Any help or advice would be greatly appreciated. Thanks!

[Floris van Doorn]

Question 1: you can use any of the following. I strongly recommend the last option, since it immediately gives you names to all 4 components.

#check Σ' (N : Type x) (_ : 𝓛.Structure N) (_ : N ⊨ T), Set (N → N)
#check Σ (N : Type x) (_ : 𝓛.Structure N),  {_s : Set (N → N) // N ⊨ T }

structure Foo where
  N : Type x
  str : 𝓛.Structure N
  mySet : Set (N → N)
  hyp : N ⊨ T

[Floris van Doorn]

Question 2: use #check M ⊨ T.

[Floris van Doorn]

Note: the (𝓜: 𝓛.Structure M) is typically left unnamed, and you should not have to use a name for it.

[Floris van Doorn]

I hope that also answers question 2.5?

[Shaopeng]

Thank you so much for your clarification on both questions, Professor Doorn.
I'm still a bit unclear about Question 2:

import Mathlib.ModelTheory.Basic
import Mathlib.ModelTheory.Syntax
import Mathlib.ModelTheory.Semantics
import Mathlib.Combinatorics.Quiver.Basic
set_option linter.unusedVariables false

variable (𝓛: Language.{u, v}) (T: 𝓛.Theory) (M: Type w)(𝓜₁: 𝓛.Structure M)(𝓜₂: 𝓛.Structure M)
#check M ⊨ T /- Prop -/

But which structure is it checking?
Say instead of just declaring the names, I defined 𝓜₁ and 𝓜₂
by explicitly giving their respective funMap and RelMaps so that first order
theory of 𝓜₁ agrees with T and theory of 𝓜₂ does not, which structure is
used when evaluating M ⊨ T ?

[Floris van Doorn]

You should avoid having two L-structures on the same type. If you have 2 structures on 2 different types, then there is no ambiguity. If you absolutely need to have more than 1 L-structure on the same type, then there are ways around it (usually by introducing a type synonym).
Please read
https://leanprover-community.github.io/mathematics_in_lean/C06_Structures.html
for more information about classes.

[Shaopeng]

Thank you so much for your further clarification, Professor van Doorn. Now I see.
Also thank you very much for the book!