1
$\begingroup$

At this link you can read Nicola Gambino's slides on one way to approach the formal syntax of Martin-Löf dependent type theory. (They are concise and very readable.)

On slide 10, he gives a standard definition of a context as a list of the form $$x_1:A_1, \ldots, x_n:A_n $$ where the $x_i$ denote pairwise distinct variables.

Now, on slide 17, he gives a standard example of a structural rule for the type theory, often called the substitution rule:

$$ \frac{x : A, \Gamma \vdash J \quad a : A}{\Gamma[a / x] \vdash J[a / x]} $$ where $J$ denotes a consequent of a generic judgment. Note that $\Gamma$ is supposed to be a context in the premise.

But what exactly does $\Gamma[a / x]$ mean?

We need $\Gamma[a / x]$ to be a context for the conclusion of the rule to be a well-formed judgment, but just replacing the variable $x$ with the term $a$ may give $\Gamma[a / x]$ the wrong form since $a$ need not be a variable. Therefore, there seems to be an immediate issue here.

Could someone clarify the definition of substituting a term for a variable in a context?

$\endgroup$
  • 2
    $\begingroup$ You may know this, but I think an assumption would be that something of the form $x : B$ does not occur in $Γ$. So you will never be 'substituting' a term into the left of of a $y : B$, which indeed doesn't make sense, only for occurrences on the right, where it is fine for terms to occur. Can you give an example you were concerned about if this doesn't cover it? $\endgroup$ – Dan Doel Jun 15 at 0:30
  • $\begingroup$ @DanDoel Right! I made a silly oversight, thank you. $\endgroup$ – CuriousKid7 Jun 15 at 2:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.