Hello,
I wonder if there is a mistake in the specification of the CHOOSE rule
in HOL-Light
<http://www.cl.cam.ac.uk/~jrh13/hol-light/HTML/CHOOSE_UPPERCASE.html>.
Indeed, with the specification that is in this url, I would be able to
have a proof of false:
|- ?x:bool. (x <=> y) ==> F
(y <=> y) ==> F |- F
--------------------------- CHOOSE (`y`,
(|- ?x:bool. (x <=> y) ==> F))
|- F
because y is not free either in F either in ((y <=> y) ==> F) - {((x <=>
y) ==> F)[y/x]} which is the empty context. And the two premisses have
to be correct.
Fortunately, when I try to apply this rule in HOL-Light with the two
premisses above, I get the following error: "Exception: Failure
"CHOOSE".". That is why I conclude that the specification would be false
rather than that HOL-Light would be unsound.
Perhaps in the specification, one must add that v should not be free in s?
Thank you,
Chantal.
------------------------------------------------------------------------------
Crystal Reports - New Free Runtime and 30 Day Trial
Check out the new simplified licensing option that enables unlimited
royalty-free distribution of the report engine for externally facing
server and web deployment.
http://p.sf.net/sfu/businessobjects
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
