Sep. 26th, 2010

something 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?

Profile

chrisamaphone

August 2014

S M T W T F S
     12
3456789
10111213141516
17181920 21 2223
24252627282930
31      

Most Popular Tags

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Oct. 21st, 2017 05:43 pm
Powered by Dreamwidth Studios