What does $\text{dom}(\Gamma)$ mean in the context of an inference rule? In the wikipedia page on pure type systems, it gives the following inference rule:

$\frac{\Gamma \vdash A : s \quad x \notin \text{dom}(\Gamma)}{\Gamma, x : A \vdash x : A }\quad \text{(start)}$

What does $\text{dom}(\Gamma)$ mean here? These are string rewriting systems, so $\Gamma$ is supposed to be a string of symbols, a purely syntactic object. I'm not sure what a &quot;domain of a string&quot; is.
There are various ways to define contexts in type theories. In this style, we assume there is some infinite set of variable names $V$ and define the context $\Gamma : V \rightharpoonup S$ as a partial function from the set of variable names to the set of types. $\mathrm{dom}(\Gamma)$ is then the subset of $V$ on which $\Gamma$ is defined, i.e. the variables in the context $\Gamma$. To require that $x \notin \mathrm{dom}(\Gamma)$ is asking for $x$ to be a fresh variable for the context $\Gamma$.