Dear Chantal, Now I agree your example is surprising and may point to a flaw in the inference kernel. However, I will wait for Joe to comment. One other possibility is that we're equivocating on the semantics of a theory package. >From the OpenTheory webpage: "A higher order logic theory package Γ ⊳ Δ consists of a proof that the theorems in Δ logically derive from the assumptions in Γ". In higher-order logic it's conventional to treat free variables as universally quantified. Hence it is reasonable to deduce falsity from the assumption |- x <=> T, just as it would be unsurprising if you were to assume |- !x. x <=> T and deduce falsity. To put it another way, is there any context in which you could use your test.art to prove falsity while only assuming the axioms of HOL? Is it possible to create an article that satisfies the assumption |- x <=> T, without again assuming something equivalent? Cheers, R[a]mana <div class="gmail_extra"> <div class="gmail_quote">On Mon, Nov 19, 2012 at 2:14 PM, Chantal Keller <<a href="mailto:chantal.keller@wanadoo.fr" target="_blank">chantal.keller@wanadoo.fr</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Rumana, I forgot to mention the key point leading to such a problem: it consists in applying [absThm] to an assumption with open terms. [absThm] check that we do not abstract over a free variable of the context, but not over a free variable of the assumptions. I do not understand your problem with the "x"s: the theorem is closed, I could as well have obtained <div class="im"> 2 input type operators: -> bool 2 input constants: = T 1 assumption: |- x <=> T 1 theorem: </div> |- (\y. y) = \y. T (see attached). An interpretation that satisfies the assumptions but not the theorems is simple : [x ↦ T]. Le 19/11/2012 14:53, Ramana Kumar a écrit : <div class="im HOEnZb">> Hi Chantal, > > I haven't looked at your article yet, but one possibility that comes to > mind is that the two "x"s on the left hand side of the theorem are distinct. > What is your interpretation that satisfies the assumptions but not the > theorem? > Does it still work if the x under the binder has a variable type (while the > x in the body has type bool)? > > Ramana > > > On Mon, Nov 19, 2012 at 1:46 PM, Chantal Keller > <<a href="mailto:chantal.keller@wanadoo.fr">chantal.keller@wanadoo.fr</a>>wrote: > >> Dear OpenTheory users and developers, >> >> It appears to me that opentheory checks as correct wrong certificates. >> >> Attached is an example. opentheory answers: >> >> 2 input type operators: -> bool >> 2 input constants: = T >> 1 assumption: >> |- x <=> T >> 1 theorem: >> |- (\x. x) = \x. T >> >> But I think this should be forbidden: there is an interpretation of the >> variables that satisfies the assumptions but not the theorems. >> >> Perhaps you should restrict assumptions to close terms, or add a side >> condition to the absThm rule? >> >> Thanks, >> >> </div><div class="HOEnZb"><div class="h5">>> _______________________________________________ >> opentheory-users mailing list >> <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> >> <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> >> >> > > > > _______________________________________________ > opentheory-users mailing list > <a href="mailto:opentheory-users@gilith.com">opentheory-users@gilith.com</a> > <a href="http://www.gilith.com/opentheory/mailing-list" target="_blank">http://www.gilith.com/opentheory/mailing-list</a> </div></div>-- Chantal KELLER </blockquote></div> </div>