*To*: James Frank <james.isa at gmx.com>*Subject*: Re: [isabelle] Trying to fit HOL to traditional math verbiage*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Fri, 4 Nov 2011 16:55:21 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4EB2E13B.507@gmx.com>*References*: <4EB2E13B.507@gmx.com>

There is a sense in which your question is not entirely meaningful, because you're asking whether rigorous but informal mathematics is adequately captured by a particular formalisation, and such issues are ultimately subjective. However, traditional mathematics is often assumed to be based on set theory, and higher-order logic has very straightforward models in set theory. In particular, if you look at the function f o g, then you get exactly the same set of ordered pairs by either route, assuming you're in the mood to interpret a function as a set of ordered pairs. The situation with higher-order logic is very different from that presented by various constructive type theories you may have seen, where you typically cannot regard a function as a set of pairs. Some of the other points that you mention relate to basic lambda-calculus. There is no need to study the lambda calculus in its full glory, as it is quite irrelevant to higher-order logic. Lambda-notation merely expresses the notion of a function, something that is curiously lacking in standard mathematical practice. The type of the composition operator is a well-known device, known as currying, for expressing functions that take multiple arguments. Again, traditional mathematics is quite careless in such situations. You remark that functions have domains and ranges, but typically the function composition operator is not written in such terms at all, and is allowed to apply to any compatible pairs of functions whatever. In the language of set theory, it is a class function. 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. This is because mathematics is essentially open-ended. Larry Paulson On 3 Nov 2011, at 18:45, James Frank wrote: > I'll ask the easy question first. In my inbox, there's isabelle-users at cl.cam.ac.uk and cl-isabelle-users at lists.cam.ac.uk . Does it make any difference which address I use to send in a question? If it doesn't, you don't need to answer that question. > > I've tried not to ask different forms of my next question. That's because after studying enough type theory, lambda calculus, functional programming, and files from ~~/src/HOL, I'll figure out most of the answers. But that could be up to a years worth of work, and I'm trying to get a feel for where this road is going, and whether I may need to travel the road less traveled. > > My question, stated very general, is this: "Can I take a file such as ~~/src/HOL/Fun.thy, rephrase the definitions in the language of standard math definitions and theorems, with a few changes to accommodate types, and have these standard definitions/theorems be describing the same objects as the Isabelle definitions and lemma?" I'm not talking about starting with a different logical framework or set of axioms, and ending up at the same place. > > Below I ask related questions which are probably more straight forward to answer, and, if answered, might answer the question just posed. > > To get more specific, I'll ask some questions about "definition comp" in Fun.thy, which is the definition of function composition. > > First, here are some related goals to set the context, for why I'm thinking about this now: > 1) I want to cater to mathematicians who are doing traditional mathematics. Therefore, the language of my definitions and theorems needs to be reasonably familiar to them. I'd like to start rephrasing Isabelle defs and thms now. > 2) I want to build on, and learn from, what others have done. Therefore, my first choice is HOL rather than ZF, since the library is larger, even though HOL is not as "traditional". > > Here's the definition of comp from Fun.thy: > > definition comp :: "('b => 'c) => ('a => 'b) => 'a => 'c" (infixl "o" 55) where > "f o g = (\<lambda>x. f (g x))" > > Studying Haskell is what led me to Isabelle, and I studied just enough functional programming to know that comp is a function that takes type "('b => 'c)" and returns type (('a => 'b) => 'a => 'c)). I guess that's right, although I ask below about (\<lambda>x. f (g x)), and about its domain and range. > > Functions have domains and ranges. You won't be surprised here, but never once have I seen "function composition" be defined with the domain being a set of functions, and the range being a set of functions whose elements are functions, which take functions, and return functions. > > Here's what I want out of "definition comp", using more standard math language: > > DEFINITION 1.1.1 (comp). Let g:'a-->'b and f:'b-->'c. Then (f o g):'a-->'b, where (f o g)(x) = f(g(x)). > > Notice that I tweak the definition to use types rather than sets. I was also tempted to stick "(f o g) = (%x. f(g x))" in there, not that I know much more than what it symbolizes. The details and groundwork could be worked out if it's basically the same thing as "comp". > > A pertinent point here is that with a definition such as DEFINITION 1.1.1, I'm not making many demands on someone. They might be willing to go with it even with only an intuitive understanding of types and lambda calculus. However, it's important to me that something like DEFINITION 1.1.1 and "comp" be the same thing. Not be like, "think of them as the same", but "are the same". > > Okay, what I really want is something like this: > (f o g) = {(a,c) in AxC | ThereExists b in B, such that (a,b) is in g and (b,c) is in f}. > > You can tell me different, but I assume I'm correct in saying that "comp" is not this set, and can't be this set, though with some work, some form of equivalence could be shown. Again, I guess that's right. > > Somewhere in this question is me trying to figure out how different "comp" is from a standard definition of composition. Is "comp" close enough to a standard definition to try and phrase it using standard language, or it's "functional programming, type theory, and lambda calculus", and I should just accept it for what it is. Regardless, it is what it is, and I want to describe it as what it is, but describe it using language other than Isabelle code. > > POINT 1: In a standard definition of function composition, there are typically three functions, "f", "g", and "f o g". > > POINT2: In "comp", there are four functions, "f", "g", "(\<lambda>x. f (g x))", and the function of type > "('b => 'c) => ('a => 'b) => 'a => 'c". > > What I've said above might could be summarized with this question: > What is this thing, this function "('b => 'c) => ('a => 'b) => 'a => 'c"? > > If I have to incorporate that into my traditional-style definition, then it's no longer traditional-style. If I have to do that, then I'm doing something different. > > If it's necessary details, and a way of specifying "g:'a-->'b, f:'b-->'c, and (f o g):'a-->'b", and I can easily formalize the connection prior to my function composition definition, then the situation is salvageable. > > Anyway, feel free to comment or not. > > Thanks, > James > > > > > >

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

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

- 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