Re: [isabelle] General nitpick/sledge info & counterX found on 1 axiom 1 theorem



On Fri, 20 Jul 2012, Gottfried Barrow wrote:

Quantifying over functions has me a little worried.

Why? Semantically a function is just a set, and in mathematics you qantify over collections of sets all the time.

You can take HOL is a simplified version of FOL + set theory, but with an explicit type system. Paradoxically HOL is weaker that FOL + ZF set theory, despite arbitrary abstraction and quantification in HOL.

Anyway, in practice you don't need to worry about the foundations and their relative logical strenth. You just do your applications with high-level specification mechanims in Isabelle (datatype, function, inductive, locale etc.), better not axiomatization.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.