Re: [Hol-info] Can I define a ZF FOL constant using only FOL symbols?

2012-09-07 Thread Gottfried Barrow
On 9/7/2012 4:41 AM, Josef Urban wrote: Hi, just a quick comment before this becomes into some HOL vs FOL issue: (conservative) extension by definitions (http://en.wikipedia.org/wiki/Extension_by_definitions) is a standard FOL method that used very often (e.g., when building up math in ZFC).

[Hol-info] [fm-announcements] RV 2012 - call for participation

2012-09-07 Thread Klaus Havelund
3rd International Conference on Runtime Verification (RV 2012) September 25-28, 2012 Koc University Research Center for Anatolian Civilizations in Pera Istanbul, Turkey http://rv2012.ku.edu.tr RV 2012 is the third conference in a series dedicated to the advancement of monitoring and analysis

Re: [Hol-info] Can I define a ZF FOL constant using only FOL symbols?

2012-09-07 Thread Josef Urban
Hi Gottfried, I think this may belong more to the FOM list. In short, I think people are OK with viewing a theory and its definitional extension as practically the same thing. Perhaps one way how to think about this could be to choose the names of newly defined symbols based on some Goedel