Re: [isabelle] Trying to fit HOL to traditional math verbiage




JFYI, perhaps you should bring up some of these questions on the
Foundations of Mathematics (FOM) mailing list to get some of the
insight from the "other side" and see what they have to say about HOL
and FOM.

http://www.cs.nyu.edu/mailman/listinfo/fom

-s
Serguei,

Thanks for the link, but definitely not.

If I gave you the impression that I'm one of the few people that have an in-depth understanding of foundations, then I deceived you.

I have my first-order logic books, and my axiomatic set theory books, and they're on my todo list, and now higher-order logic puts me back to where I don't know where the bottom is for the foundation that I may have to use, not that I'm definitely committed to higher-order logic.

As far as public forums such as mailing lists and blogs, they're bad for me. I insult people and then can't get back to thinking about what I need to think about.

--James





On 11/5/2011 12:07 PM, Serguei Mokhov wrote:
James,

On Sat, Nov 5, 2011 at 11:46 AM, James Frank<james.isa at gmx.com>  wrote:

Anything that you can define in higher-order logic is not merely
explicable in traditional mathematical terms, but it is easily so. But there
are plenty of things you can write in mathematics that are impossible to
formalise in higher-order logic.
The good news is that different foundations converge at a higher point where
they a lot of math in common.

Again, there's no real problem. Very few people have an in-depth
understanding of the foundations of math, so there's a lot of skipping that
low level stuff anyway, or totally ignoring it.

--James
JFYI, perhaps you should bring up some of these questions on the
Foundations of Mathematics (FOM) mailing list to get some of the
insight from the "other side" and see what they have to say about HOL
and FOM.

http://www.cs.nyu.edu/mailman/listinfo/fom

-s







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