Extension of a Signature

Question

I came across the following rule about signature extension in Harper's 1993 classical paper on LF (see page 5, Figure 1).

$$\frac{\Sigma:sig\quad\vdash_\Sigma A:Type\quad c\not\in dom(\Sigma)}{\Sigma,c:A:sig} $$

I understand what the rule means: given that $\Sigma$ is a valid signature and $A:Type$ is derivable from $\Sigma$ and the empty context, then given that $c$ is a fresh constant in $\Sigma$, we shall extend $\Sigma$ with $c:A$.

My question is: how to understand the judgement $c:A$ in the conclusion of this rule? I cannot follow from the three premises that $c$ is a proof object of $A$, and so why it is permissible to declare that $c:A$?

Thanks!!!

Answer 1

Your objection makes the implicit assumption that from the judgment $\Sigma,c:A:sig$ it would follow that $c:A$. Yet $c:A$ is not a judgment, so it doesn't make sense to derive it. The judgment you can derive does make sense, since it is assuming the signature (using b-const-obj as the final step): $$\vdash_{\Sigma,c:A} c:A$$.

Answer 2

This rule means:

Given a signature $\Sigma$, a type $A$ defined in the context of this signature, and a symbol $c$ that is not already part of the signature, then you can define the extended signature $\Sigma, c:A$, consisting in the signature $\Sigma$ extended with the new symbol $c$ of type $A$.

$c:A$ is then a valid construction in the context defined by this new signature - but this is not defined by this rule.