[opentheory-users] Wrong certificates

[Chantal Keller]

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

2 input type operators: -> bool
2 input constants: = T
1 assumption:
  |- x <=> T
1 theorem:
  |- (\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 :
> 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
> <chantal.keller at wanadoo.fr>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,
>>
>>
>> _______________________________________________
>> opentheory-users mailing list
>> opentheory-users at gilith.com
>> http://www.gilith.com/opentheory/mailing-list
>>
>>
> 
> 
> 
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list

-- 
Chantal KELLER
-------------- next part --------------
A non-text attachment was scrubbed...
Name: test.art
Type: image/x-jg
Size: 801 bytes
Desc: not available
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20121119/2bd58934/attachment.art>