*To*: James Frank <james.isa at gmx.com>*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: Serguei Mokhov <serguei at gmail.com>*Date*: Sat, 5 Nov 2011 13:07:47 -0400*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4EB55A63.90202@gmx.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>*Reply-to*: mokhov at cs.concordia.ca

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

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

**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

- 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