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?
From:
Anonymous( )Anonymous This account has disabled anonymous posting.
OpenID( )OpenID You can comment on this post while signed in with an account from many other sites, once you have confirmed your email address. Sign in using OpenID.
User
Account name:
Password:
If you don't have an account you can create one now.
Subject:
HTML doesn't work in the subject.

Message:

 
Notice: This account is set to log the IP addresses of everyone who comments.
Links will be displayed as unclickable URLs to help prevent spam.

Profile

chrisamaphone

August 2014

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

Most Popular Tags

Style Credit

Expand Cut Tags

No cut tags
Page generated Oct. 22nd, 2017 12:48 am
Powered by Dreamwidth Studios