This is an attempt to revive this closed question, which I think is a perfectly fine question about which much can be said, and which has not been answered yet on this site to my knowledge. The question is:

When we say things like "let $G$ be a group" or "let $X$ be a topological space" or "let $f : X \to Y$ be a function," what exactly do these statements mean?

Some people seem to think the answer is obvious; I genuinely do not understand what they think the obvious answer is, but maybe they think the answer is that "let" refers to universal quantification. I don't agree that this suffices as an account of what "let" means, because "for all groups $G$" is not a complete sentence but "let $G$ be a group" is. So their grammar is meaningfully different.

A different "obvious" answer might be that "let" just refers to a definition, e.g. "let $G$ be a group" just defines the meaning of the symbol $G$. I also don't agree that this suffices as an account of what "let" means, because in a pair of sentences like "let $G$ be a group of order $400$. Prove that the Sylow subgroups of $G$ have [some property]," it seems that we are doing something involving universal quantification after all: aren't we being asked to prove that, for all groups of order $400$, [etc]?

To me the meaning of "let" seems to have something to do with the introduction rule for the universal quantifier (which does not appear to be explained anywhere on e.g. the Wikipedia article on the universal quantifier, although universal generalization seems closely related), and also something to do with a typing declaration or typing judgment (which I don't know any explanation of in a mathematical context). But it would be great to have something more precise and detailed to point to.

To try to state the question more forcefully: is the sentence "let $G$ be a group" a sentence in ZFC set theory? If not, what is it?

Edit: The question How to interpret "let" in mathematics? is related but I am not satisfied by any of the answers there, none of which discuss universal generalization or typing declarations / judgments. John Hughes' answer discussing "opening a context" and Joe's answer discussing universal generalization are the closest to what I'm looking for, but I am hoping for even more detail than this. What does "opening a context" actually mean? What is a context?

To try to indicate the direction of what I'm looking for, after you say "let $G$ be a group," the variable $G$ is now "in scope," in computer science terms; it is part of the "local memory" that can be addressed in the rest of the discussion. I think we clearly have an intuitive sense of how this works from experience but I have never seen anyone give a precise explanation or formalization of it. Is there one? This came up previously in What are the rules of scope?.

This is an attempt to revive this closed question, which I think is a perfectly fine question about which much can be said, and which has not been answered yet on this site to my knowledge. The question is:

When we say things like "let $G$ be a group" or "let $X$ be a topological space" or "let $f : X \to Y$ be a function," what exactly do these statements mean?

Some people seem to think the answer is obvious; I genuinely do not understand what they think the obvious answer is, but maybe they think the answer is that "let" refers to universal quantification. I don't agree that this suffices as an account of what "let" means, because "for all groups $G$" is not a complete sentence but "let $G$ be a group" is. So their grammar is meaningfully different.

A different "obvious" answer might be that "let" just refers to a definition, e.g. "let $G$ be a group" just defines the meaning of the symbol $G$. I also don't agree that this suffices as an account of what "let" means, because in a pair of sentences like "let $G$ be a group of order $400$. Prove that the Sylow subgroups of $G$ have [some property]," it seems that we are doing something involving universal quantification after all: aren't we being asked to prove that, for all groups of order $400$, [etc]?

To me the meaning of "let" seems to have something to do with the introduction rule for the universal quantifier (which does not appear to be explained anywhere on e.g. the Wikipedia article on the universal quantifier, although universal generalization seems closely related), and also something to do with a typing declaration or typing judgment (which I don't know any explanation of in a mathematical context). But it would be great to have something more precise and detailed to point to.

To try to state the question more forcefully: is the sentence "let $G$ be a group" a sentence in ZFC set theory? If not, what is it?