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?
> ....
> 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.
> 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?
Regards,
Rob.
------------------------------------------------------------------------------
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
