Metamath Zero's definition of free variables in an expression

[Bulhwi Cha]

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

[Mario Carneiro]

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̅.

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/1945193.fG6EfdGv7r%40desktop.semmalgil.com.

[Bulhwi Cha]

On Saturday, August 23, 2025 7:09:45 PM KST Mario Carneiro wrote:
> 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̅.

Ah, I guess I misunderstood the meaning of Dom(Γ′ᵢ). For instance, if
Γ′ᵢ = (φ : wff x y), is it true that Dom(Γ′ᵢ) = {x, y}? I thought that
Dom(Γ′ᵢ) = {φ} in this case.

[Mario Carneiro]

Ah, well I suppose that isn't defined either, so it's really a question of what notation makes the most intuitive sense so that it's easily grokked even without a definition. The paper uses Dom(Γ), and it means the set of variables (both first and second order) but not Dom(Γ′ᵢ). If it is just always a singleton then it seems kind of unnecessary and it would be better to have a notation for picking out the variable itself, and that's what Γ'ᵢ is supposed to denote. (It might also be used to refer to the full variable declaration including the sort, as I did in my last message.) It is of course possible to define all of this more precisely with inductive specs and functions, but deciding where *not* to formalize in a mathematical text is a skill and a balancing act.

--
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 metamath+u...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/metamath/9716512.Jy0nUZJEyI%40desktop.semmalgil.com.