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.
On Sat, Aug 23, 2025 at 2:40 PM 'Bulhwi Cha' via Metamath < [email protected]> wrote: > 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. > > -- > 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/9716512.Jy0nUZJEyI%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/CAFXXJSuZK6RbrtdCgLAFm8EbunUEsew%2BLtaaeLHKtb4hwshoww%40mail.gmail.com.
