3
$\begingroup$

In the answer to a previous question I have been recommended to read this paper by Philipp Haselwarter and Andrej Bauer. In this paper a class of dependent type theories is formally defined.

We are given a signature $\Sigma$. A raw type theory over $\Sigma$ is a family of raw rules over $\Sigma$ (Definition 2.16). Such a family determines an associated deductive system. I am expecting that these associated deductive systems are deductive systems, that is: families of closure rules. It is probably the case, but I didn't understand what boundary closure rules are. For these rules, we have a link to Figure 2.6, which does not provide closure rules but raw-rule boundaries (Definition 2.9). Each raw-rule boundary with some fresh symbol determines a raw rule (Definition 2.10). I am wondering if the boundary closure rules are the closure rules determined by such raw rules. But for which symbols? And what would be the point to give raw-rule boundaries instead of raw rules directly? Moreover, if we consider, for instance TT-BDRY-TM that has the premise $\Gamma; \Theta \vdash A \: \mathsf{type}$ and the conclusion $\Gamma; \Theta \vdash \square : A$, the metavariable $A$ could be instantiated by some uninhabited type and it seems to me that we would rather not have such a closure rule.

I am aware that the answer to my question is probably in the paper, that's why I hesitated to ask my question but the paper is hard to read to me.

$\endgroup$
12
  • $\begingroup$ Before I answer the question, let me ask: why do boundary closure rules confuse you (Figure 2.6) but the equality closure rules do not (Figure 2.5)? They have precisely the same status and both feature in Definition 2.16, so my understanding why one confuses you but the other does not will help me guess what's going on. $\endgroup$ Feb 9 at 14:38
  • $\begingroup$ When you say that the boundary $\Gamma; \Theta \vdash \Box : A$ should be undesirable when $A$ is (instantiated to) an empty type, that makes me think that perhaps you have the wrong idea about boundaries. The judgement "$\Gamma; \Theta \vdash \Box : A$" does not state "$A$ has an element" but "the question 'does $A$ have an element?' is well-formed". (The answer might be "no, it does not have an element" and that is ok.) $\endgroup$ Feb 9 at 14:41
  • $\begingroup$ @AndrejBauer Premises and conclusions of Fig. 2.5 are hypothetical judgements in contrast with those of Fig. 2.6, which are hypothetical boundaries. Thus equality closure rules are really closure rules; more precisely, for instance, the TT-EqTy-Refl rule is not one closure rule but a set of closure rules in the same way as for the TT-Abstr rule as explained in Remark (3): for any metavariable context $\Theta$, for any variable context $\Gamma$, for any metavariable A$, we have one closure rule TT-EqTy-Refl_{\Theta, \Gamma, A}. That's fine to me because I expect to get a set of closure rules. $\endgroup$
    – Bruno
    Feb 11 at 1:46
  • 1
    $\begingroup$ For all type expressions (valid in whatever context, meta-context they appear). $\endgroup$ Feb 18 at 9:36
  • 1
    $\begingroup$ The conclusion of TT-Meta is never an abstraction. The conclusion of a specific rule is never an abstraction. $\endgroup$ Feb 21 at 16:02

1 Answer 1

1
$\begingroup$

I am not sure what bothers you, but a deductive system is any family of any closure rules, where a closure rule is just a pair of the form $([p_1, \ldots, p_n], c)$. The $p_i$'s are the premises and $c$ is the conclusion.

There is no a priori limitation on what the premises and the conclusion are. For example, here is a deductive system $D$ that uses numbers as premises and conclusions: $$D = \lbrace ([k_1, \ldots, k_n], m) \mid k_1, \ldots, k_n, m \in \mathbb{Z} \land \exists a_1, \ldots, a_n \in \mathbb{Z} . a_1 k_1 + \cdots a_n k_n = m \rbrace.$$ The deductive system $D$ is not entirely silly. It says that we may "conclude" $m$ from $k_1, \ldots, k_n$ if $m$ is a linear combination of $k_1, \ldots, k_n$ for some integer coefficient. Exercise: the deductive closure of $\{a, b\}$ is the set of multiples of $\gcd(a,b)$.

Now, in the paper at hand the deductive systems contain as their premises and conclusions both the hypothetical judgements and the hypothetical boundaries. You can just think of the hypothetical boundaries as another kind of judgement forms (in addition ot the four "standard" ones). If we felt like it, we could also include raindrops and roses and whiskers on kittens, but we decided not to. In fact, the last paragraph of section 2.2 says explicitly (emphasis added):

Henceforth we shall consider solely deductive systems on the set of hypothetical judgements and boundaries.

I hope that helps clear up the confusion.

$\endgroup$
2
  • $\begingroup$ Thanks! For some psychological reason I thought a deductive system couldn't contain hypothetical and boundary judgments together: I see deductive systems as a way to specify derivations and we have either derivations with only hypothetical judgements or with only boundary judgements (right?). If it is right, we could define an associated hypothetical deductive system and an associated boundary deductive system instead of an associated deductive system. If derivations indeed don't mix the two kinds of judgements, it would be equivalent but, perhaps, closer to the intuition. $\endgroup$
    – Bruno
    Feb 12 at 0:32
  • $\begingroup$ Definition 2.8 specifies that the closure rule associated with a raw rule has as one of its premises a hypothetical boundary, so derivations will in general contain both kinds of premises. Note that Theorem 3.19 shows that the rule without the hypothetical boundary premise is admissible for finitary type theories. $\endgroup$ Feb 12 at 6:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.