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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and