*To*: Lawrence Paulson <lp15 at cam.ac.uk>, isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: James Frank <james.isa at gmx.com>*Date*: Sat, 05 Nov 2011 10:46:43 -0500*In-reply-to*: <ECA95F60-EF18-4223-966E-138C4918A57E@cam.ac.uk>*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>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:6.0.2) Gecko/20110902 Thunderbird/6.0.2

On 11/4/2011 6:13 PM, Lawrence Paulson wrote:

On 4 Nov 2011, at 19:31, James Frank wrote:The problem is with this ubiquitous "'a => 'b => 'c" type statement. It's not a part of 98% (a little less or little more) of the math world.I can't believe that any serious mathematician would struggle with this. Larry Paulson

--James ----------------------------------------------------------- Dr. Paulson,

There is a sense in which your question is not entirely meaningful...

Anything that you can define in higher-order logic is not merelyexplicable in traditional mathematical terms, but it is easily so. Butthere are plenty of things you can write in mathematics that areimpossible to formalise in higher-order logic.

--James On 11/4/2011 11:55 AM, Lawrence Paulson wrote:

Larry Paulson On 3 Nov 2011, at 18:45, James Frank wrote:

Here's the definition of comp from Fun.thy:

"f o g = (\<lambda>x. f (g x))"

Okay, what I really want is something like this:

"('b => 'c) => ('a => 'b) => 'a => 'c". What I've said above might could be summarized with this question:

Anyway, feel free to comment or not. Thanks, James

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

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

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

- Previous by Date: Re: [isabelle] Proof document to span multiple sessions
- 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