It is slightly imprecise notation. The notation Γ′ᵢ ∈ x̅ means that the i'th variable in the context is a first order variable y, which is in the list x̅ of dependencies. Using Dom(Γ′ᵢ) ⊆ x̅ is not correct as it would also include second order variables if their dependencies are in the list. A more precise way to state this is ∃ y s, Γ'ᵢ = (y : s) ∧ y ∈ x̅.
On Fri, Aug 22, 2025 at 4:44 PM 'Bulhwi Cha' via Metamath < [email protected]> wrote: > There are the definitions of FV(e) and F̲V̲(e̅::Γ′) on page 27 (Section > 1.4.4 Well-formedness) of Mario Carneiro's PhD thesis about Metamath > Zero[0]: > > FV(x) = {x} > FV_Γ(φ) = x̅ where (φ : s x̅) ∈ Γ > FV(f e̅) = F̲V̲(e̅::Γ′) ∪ {eᵢ | Γ′ᵢ ∈ x̅} where f(Γ′) : s x̅ > > F̲V̲(·::·) = ∅ > F̲V̲((e̅, y)::(Γ′, x : s)) = F̲V̲(e̅::Γ′) > F̲V̲((e̅, e′)::(Γ′, φ : s x̅)) = F̲V̲(e̅::Γ′) ∪ (FV(e′) ∖ {eᵢ | Γ′ᵢ ∈ x̅}) > > I think {eᵢ | Dom(Γ′ᵢ) ⊆ x̅} should be substituted for {eᵢ | Γ′ᵢ ∈ x̅} > in these definitions. Γ′ᵢ is of the form x : s, so Dom(Γ′ᵢ) is of the > form {x}. > > [0] https://digama0.github.io/mm0/thesis.pdf > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/metamath/1945193.fG6EfdGv7r%40desktop.semmalgil.com > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CAFXXJSs%2B7j3k3w_iPoZ_Ue19fZb3zJ5NpVRMgTJwFK4%3DW9CMmw%40mail.gmail.com.
