*To*: mokhov at cs.concordia.ca*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: James Frank <james.isa at gmx.com>*Date*: Sat, 05 Nov 2011 18:32:52 -0500*Cc*: isabelle-users at cl.cam.ac.uk, Serguei Mokhov <serguei at gmail.com>*In-reply-to*: <CAJ5BkY7TLKEZpU5D_1zm-==wNSrZbBAB32W9YJ8wd9iaJpHvXQ@mail.gmail.com>*References*: <4EB2E13B.507@gmx.com> <2A23DDB6-B2FF-485F-95B2-851CAEA425A7@cam.ac.uk> <4EB43DA4.2020902@gmx.com> <ECA95F60-EF18-4223-966E-138C4918A57E@cam.ac.uk> <4EB55A63.90202@gmx.com> <CAJ5BkY7TLKEZpU5D_1zm-==wNSrZbBAB32W9YJ8wd9iaJpHvXQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2

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.

--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. --JamesJFYI, 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

**References**:**[isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Lawrence Paulson

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*James Frank

**Re: [isabelle] Trying to fit HOL to traditional math verbiage***From:*Serguei Mokhov

- Previous by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Date: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Previous by Thread: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Next by Thread: Re: [isabelle] Trying to fit HOL to traditional math verbiage
- Cl-isabelle-users November 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list