I am trying to get a deeper understanding of why the rules in logic and type theories exist, and am now looking at the simply typed lambda calculus, the typing rules on Wikipedia.
The first one is this:
$${\frac{x\mathbin{:}\sigma \in \Gamma}{\Gamma \vdash x\mathbin{:}\sigma} }$$
Why is that rule necessary? It seems like the premise and the conclusion say the same thing. It's hard to understand why this is necessary. The natural language form of that on Wikipedia even sounds like they both say the same thing:
If $x$ has type $\sigma$ in the context, we know that $x$ has type $\sigma$.
The only thing that seems different in the natural language interpretation of that formula, is that in the conclusion, you know that $x$ has type $\sigma$, while in the premise you don't necessarily know, but you do observe or see it has that type, maybe because syntactically that's how it's written down. So maybe a slightly more informative translation is, "if you observe $x$ has type $\sigma$, then you know $x$ has type $\sigma$". Is that all it's saying?
Why does there need to be a rule for this? It seems along the lines of saying "things that exist, exist" or something equally as obvious. Couldn't this just be considered a notational definition rather than a typing rule? In that sense, it seems like this is all you really need: "By definition, $x:\sigma$ means $x$ is of type $\sigma$". Why is that not enough?
Basically just looking for an insight to more deeply understand why this rule is necessary, because otherwise it seems so obvious that, when I try to explain it to others, I end up just saying "I don't know why it's there, it's just there because it needs to be for some reason." I can't seem to come up with a good reason why it's there.
We want to be able to make typing judgments like $\vdash \lambda x\cdot x : \sigma \to \sigma$. And to do this we have to use the rules and nothing else to construct a formal derivation of this typing judgment. In this example, the derivation looks like this:
$$\begin{array}{c} x : \sigma \in \{x : \sigma\}\\\hline x : \sigma \vdash x : \sigma\\\hline \vdash \lambda x \cdot x : \sigma \to \sigma \end{array} $$
I.e., we construct a tree whose root (bottom line) is the typing judgment we want to make and whose nodes are instances of the typing rules (in this case there is no branching in the tree, so it just look like a list of judgments).
The rule that you are concerned with is the one I used in the top node in the tree. It does just say "in a context that declares $x$ to have type $\sigma$, we can assign type $\sigma$ to the term $x$" and that does sound very trivial. However, without it you wouldn't be able to get started with building the tree.
The presentation of the rule in the wikipedia article is a little unusual. The formula $x : \sigma \in \Gamma$ above the line is really a side-condition: it's saying if $x : \sigma$ appears in the context $\Gamma$, then $\Gamma \vdash x : \sigma$ is a valid typing judgment. It would be more usual to express this using pattern matching and just say that any instance of the following is an axiom, i.e., a rule that creates a typing judgment from scratch:
$$ \Gamma, x : \sigma \vdash x :\sigma $$
The derivation above would then be written just as: $$\begin{array}{c} x : \sigma \vdash x : \sigma\\\hline \vdash \lambda x \cdot x : \sigma \to \sigma \end{array} $$ where the top node in the tree is an instance of the axiom with $\Gamma$ empty.