On 09/08/12 21:12, Roger Bishop Jones wrote: > On Thursday 09 Aug 2012 11:06, Michael Norrish wrote: > >> 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 > > Is this a cue for reopening the discussion about whether the > conservative extension rules are optimal (maximal)? > (or about whether optimal is the same thing as maximally > liberal) > > Do you have an opinion on Rob's proposal on this front, and > or on my sketch of how to incorporate type constructors into > the scheme?
I'm not sure I've seen the latter, but Rob's proposal is an "issue" on our wishlist of things to do. See: https://github.com/mn200/HOL/issues/72 Certainly, my feelings about it are generally positive. On the other hand, I do notice that the new proposal's emulation of the old new_specification depends on Hilbert choice. This is a definite wart in my opinion. 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
