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.
signature.asc
Description: This is a digitally signed message part.
