Inference rule for Non-Empty Domains

Question

I am currently experimenting with logic frameworks. I am basically using something along dependent types as in "Proof-assistants using Dependent Type Systems" by Henk Barendregt and Herman Geuvers. I then came across the idea to formulate the following rule:

G, y:t |- s:A
------------- (declE) y not in G, A
   G |- s:A

I call this rule declaration elemination. It removes declaring that the variable y has sort t und the side condition is that the proved formula A does not contain the variable y anymore.

Now I wonder whether this rule is necessary or not. Can we for example prove:

1) If A is closed then all variable declarations are anyway discharged.

Or alternatively maybe we can highlight:

2) What formula A can be proved, not having a variable y free, and where we would later like to discharge the variable y.

Bye

P.S.: declE can be formulate as the expression a:sort\b:prop\ ((x:a\b) -> b) where x not in b or equivalently a:sort\b:prop\ ((a -> b) -> b).

Answer 1

When you say you are working in some (unspecified) logical framework, you are not really telling us what logic you are actually working in. However, in type theories that allow empty types, your rule is not admissible: declaring $y$ to be a member of an empty type is a nontrivial assumption.

If you logic does have all types non-empty, then your rule is admissible, but it depends on the other rules of your logic whether it is necessary.

Answer 2

It seems that what I am asking for is more or less Proposition 2.33 from Conal Elliott's PhD thesis, Extensions and Applications of Higher-Order Unification.

Although the contexts/signatures are ordered. The proposition reads as follows. if we have

D, v:t, G |- s:A

And if v does not occur in G, s, A, then we can derive:

D, G |- s:A

So the error I made in my question is that I did not think of requiring v to not occur in s as well. And it seems that it is irellevant whether t is non empty or not.