On 09/08/2012, at 20:26, Rob Arthan <r...@lemma-one.com> wrote:
> Michael,
>
> On 9 Aug 2012, at 11:06, Michael Norrish wrote:
>>
>> I can do all the rest of your proof, and will have that assumption
>> everywhere. I will then eliminate it at the very end with the theorem
>>
>> ?cf. !P x. P x ==> P (cf P)
>>
>> and existential elimination.
>
> But where does that theorem come from?
>
It's derived from AC.
>> Sure, that proof is of what HOL4 has as "SKOLEM_THM", which we derive from
>> our Hilbert choice axiom. I still think my argument is good for the fact
>> that
>>
>> 1) we can derive the choice operator from SKOLEM_THM
> But SKOLEM_THM is AC.
Indeed.
>> 2) we need to/should accept the definitional principle that allows (closed)
>> existential theorems to justify signature extension with constants,
>> recognising that this doesn't assume AC
>
>
> I wasn't making any statements about what should or should not be in HOL, but
> I seem to have lost the plot here. You appeared to be saying that the
> epsilon--axiom was conservative over simple type theory without any form of
> AC. But apparently you aren't. So what are you claiming?
>
Freek said something along the lines of "I'm fine with AC, but I'm
skeptical/uneasy about the Hilbert choice operator". (This was all part of the
"formalist on the weekends" post.)
I pointed out that AC gives us Hilbert Choice very directly in HOL, as long as
one buys the new_specification principle, and believes it to not already depend
on Hilbert choice itself (which is how it is implemented in HOL Light). Freek
cavilled a little at that, so I described the construction whereby the use of
the constant that was called into existence by use of that principle could be
eliminated, so that that principle is indeed conservative and does not need AC.
Of course, I was having a slight dig at HOL Light because that system will only
give you new_specification if you're already bought into Hilbert Choice. It's
hard to know how to get around this if you don't want to put the existential
quantifier into your system as one of its primitive constants.
Michael
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
