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?

Date: 2010-09-27 06:06 am (UTC)From: [identity profile]
...Well, if you have a good theorem-prover, and if it has two different ways to prove the same theorem, then it will try both of them, right? And whichever one finishes the fastest, that is the proof-path it will use.

Date: 2010-09-28 03:46 am (UTC)From: [identity profile]
I think it is the former in Twelf: we do explicitly use weakening in an LF-this-is-free sense.

Additionally, I don't think the latter is a form you can actually represent in Twelf generally, but I'm not sure. It may rather be the case that, because the quantification is uniform (we don't case analyze the structure of the context Γ) that the two are somehow formally equivalent in the Twelf representation, but that's wild and uninformed speculation.

Date: 2010-09-28 06:44 am (UTC)From: [identity profile]
i think whenever i do it on paper, it's the latter -- give me the strongest induction hypothesis you can conjure up! but i think Rob's right in that it's not what we actually do in Twelf -- in Twelf, context quantification comes from the %worlds, i guess, and so it's further towards the outside than anything you can express in LF itself..



August 2014

17181920 21 2223

Most Popular Tags

Style Credit

Expand Cut Tags

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