![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
(no subject)
Sep. 26th, 2010 05:23 pmsomething you stop thinking about after awhile of using LF's context as your object context is where the context gets quantified in the statement of a theorem.
consider identity for an intuitionistic sequent calculus: "for any prop A, there is a sequent derivation of Γ, A => A." the proof proceeds by induction on A. but in each use of the induction hypothesis, do you get to pick Γ, or is it fixed at the outset of the whole induction over A? in other words, are you proving
"for all Γ, [for all A, [Γ, A => A] by induction on A]", or
"for all A, [for all Γ, Γ, A => A] by induction on A"?
you can do the proof either way, but, if you have monotonicity uniformly sprinkled throughout your rules (that is you get to keep whatever left-assumption you break down in each subgoal), then what you do after applying the IH is different: one (the former) requires weakening, and one requires instantiation of a universal quantifier. (inspiration of this post: i had students do it both ways on their constructive logic homework.)
my question is: which one are we doing when we do it in Twelf? i think it's the former because of all the ignored LF-lambda-bound variables, but i'm not positive. and relatedly, is there a way to express the alternative?
consider identity for an intuitionistic sequent calculus: "for any prop A, there is a sequent derivation of Γ, A => A." the proof proceeds by induction on A. but in each use of the induction hypothesis, do you get to pick Γ, or is it fixed at the outset of the whole induction over A? in other words, are you proving
"for all Γ, [for all A, [Γ, A => A] by induction on A]", or
"for all A, [for all Γ, Γ, A => A] by induction on A"?
you can do the proof either way, but, if you have monotonicity uniformly sprinkled throughout your rules (that is you get to keep whatever left-assumption you break down in each subgoal), then what you do after applying the IH is different: one (the former) requires weakening, and one requires instantiation of a universal quantifier. (inspiration of this post: i had students do it both ways on their constructive logic homework.)
my question is: which one are we doing when we do it in Twelf? i think it's the former because of all the ignored LF-lambda-bound variables, but i'm not positive. and relatedly, is there a way to express the alternative?
