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



Tim,

Thanks for the question, primarily so I can leave in a civilized manner and say something positive. By asking my question, I've made about 3 transitions.

It was functional programming, then proof assistants, and now it's all the same. In messing around with Isabelle for about a month, it raised my awareness so that I could see that Coq is a functional programming language. Coq provides me with a book which will teach me functional programming and the proof assistant software at the same time. Isabelle starts at the intermediate level in regards to functional programming. That's too high for me.

Everyone here has been very helpful, accessible, and professional. I'm not a professional, and I don't act like one.

Now to your questions.

SHORT ANSWER: Let f(x)=sin(x).

REFERENCE: http://www.angelo.edu/faculty/cdiminni/ . The area code is actually 325, not 915.

YOU ASK: What? Why?

Because the definition requires it.

Let f be a subset of AxB. Then f is a function if
1) for every x in A, their exists some y in B such that (x,y) is in f, and
2) if (x,y1) is in f, and (x,y2) is in f, then y1=y2.

We call A the domain of f, and we call B the codomain of f. The range of f is that subset of B... It's getting obnoxious at this point. The range is the actual values that the x's are mapped to.

YOU ASK AND SAY: To allow what? I'm not convinced that anyone deliberately decided that the definition of functions shouldn't correspond with how mathematicians actually think about them. I think it's just a long-standing imprecision.

I'm not a historian. I was speculating on the reasons. It doesn't make sense to continue to have such a loose definition of function unless there's an advantage. EXAMPLE: Definition of limit. Newton and Liebniz started limit (or used it). Weierstrass tightened it up. Everyone accepted the tighter epsilon-delta definition.

WE ARGUE:

Otherwise, a tighter definition of function becomes a big show stopper.
Why?  Can you give an example?


Let f(x)=sin(x). The details? You have to work them out. Reference? Above. For basic values of x, we can show the particular values to which some x is mapped to in the interval [-1,1]. For an arbitrary x in R, it gets difficult to show what value that x is mapped to. How do I know? I don't. Why am I willing to confess to not knowing such a basic thing? I'm not a professional. I don't have to maintain appearances. I can get rude, crude, and uncivilized, and flaunt my lack of knowledge, and use every email as an opportunity to pontificate.

For myself, I don't need an explicit example. The axiom of choice's "choice function" appears to me to be 100% built for what we're discussing.

Pg. 219, Set Theory, Seymour Lipschutz. "Recall that function f:{A_i: i in I} --> X, where each A_i is a subset of X, is called a choice function if f(A_i) = a_i belongs to A_i, for every i in I. In other words, f 'chooses' a point a_i in A_i for each set A_i".

It was in a linear algebra class that, after the professor gave a definition from "4.2 Linear Transformations From R^n to R^m" (Elementary Linear Algebra, Howard Anton), that someone raised their hand and asked, "What's the difference between the codomain and range?" It was the next class that the professor felt some obligation to clarify whatever he had said the previous class. He must have been thinking about it.

It's not surprising. In most, books, they don't even take the time to differentiate that there's both a codomain and a range. It's only implied in the definition of function.

Regards,
--James





On 11/9/2011 4:50 PM, Tim (McKenzie) Makarios wrote:
On 08/11/11 05:00, James Frank wrote:
To prove that f is a function, you have to show that for every element
in the domain, there exists an element in the codomain that it's mapped
to. But the best you might can do is show that it maps to an element in
some interval.
What?  Why?

So someone, somewhere back  in history, conveniently
decided to loosen up the definition of function to allow that.
To allow what?  I'm not convinced that anyone deliberately decided that
the definition of functions shouldn't correspond with how mathematicians
actually think about them.  I think it's just a long-standing imprecision.

Otherwise, a tighter definition of function becomes a big show stopper.
Why?  Can you give an example?

--James
Tim
<><





On 11/9/2011 4:50 PM, Tim (McKenzie) Makarios wrote:
On 08/11/11 05:00, James Frank wrote:
To prove that f is a function, you have to show that for every element
in the domain, there exists an element in the codomain that it's mapped
to. But the best you might can do is show that it maps to an element in
some interval.
What?  Why?

So someone, somewhere back  in history, conveniently
decided to loosen up the definition of function to allow that.
To allow what?  I'm not convinced that anyone deliberately decided that
the definition of functions shouldn't correspond with how mathematicians
actually think about them.  I think it's just a long-standing imprecision.

Otherwise, a tighter definition of function becomes a big show stopper.
Why?  Can you give an example?

--James
Tim
<><







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