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



On Fri, 20 Jul 2012, Gottfried Barrow wrote:

On 7/20/2012 9:34 AM, Makarius wrote:
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.

Because I read things that I don't completely understand that make me worry, such as that certain things can be proved about FOL that can't be proved about HOL. Was that "completeness" that I read about? I don't even look it up.

Depends you how completeness is formalized. The book by Peter B. Andrews "An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof" contains the standard canon of correctness and completeness 3 times: (1) propositional logic, (2) first-order logic, (3) higher-order logic. The latter goes back to Henkin 1950, who was discussing the Church 1940 version of HOL, which was not called HOL back then.

For using Isabelle/HOL, all of this is of little practical relevance. You just do mathematical modelling with the definitional mechanisms that the system gives you, and trust that the internal foundations (implementation wrt. the core logic) work out. It is like getting on a high-speed train: you merely need to buy a ticket to participate, not study all the technical manuals first.


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.

Here, I don't even know what "weaker" means because I've found no standard definition anywhere for "logically weaker".

However, I've found enough information to assume that it means that everything you can prove with HOL can be proved with FOL+ZF, but not vice versa.

Yes. HOL can live semantically in a small subspace of FOL+ZF. So you can do most of classic mathematics with some restrictions. It will take a long time until you get to the foundational limits, though.


	Makarius





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