33 ms·

I wouldn't worry about that. I'm studying mathematics and I also feel stupid while reading new concepts on Wikipedia. The problem with mathematics is that, if y

I wouldn't worry about that. I'm studying mathematics and I also feel stupid while reading new concepts on Wikipedia. The problem with mathematics is that, if you don't know the idea behind the concept or which kind of problem is it trying to solve, it's almost impossible to really understand the definitions. And even when you understand the concepts and ideas, it can still be difficult to understand the definitions. Few months ago, a professor told us the 100% formal definition of a function: it wasn't easy to understand and we all had this "wtf" face.

jordigh 12y ago
Yeah, the thing with formal definitions is that they're like little programs you have to compile before you can see their output. Trying to understand what a function is from a statement such as "a function from A to B is a subset F of the cartesian product AxB such that for all (a1,b1), and (a2,b2) in F, b1=b2 whenever a1=a1" really obscures the notion this is all about "mapping" or "doing" something. This definition is more like something that you would feed to a computer who doesn't "understand" what really is going on. Or to a human, who would work through it piecemeal, and try to build a few functions following this definition until the a-ha moment would come and this human would form a different intuitive understanding of what a function is or does. But the reason we write definitions as little programs to be compiled is to make sure that there can be no room for ambiguity. You compile the definition and arrive at the same mathematical object as anyone else. If we define a function as a mapping or a procedure, then we just shifted one word for another and still have to elucidate what a mapping or a procedure is.
- ihm 12y ago
  Well, the set theoretic attempt to describe functions isn't a very nice one. Type theory gives a formal definition closer to the intuitive notion: a function from A to B is a program of type A -> B. I.e., a rule for turning things of type A into things of type B.
  - jordigh 12y ago
    I admit I don't know much about type theory. I assume "program" is a term of art? Also, does this allow for functions that have literally undescribable rules, such as a function arising from the application of the axiom of choice? Wanting to allow such undescribable functions is the reason for the set theoretic definition. I assume "rule" isn't a term of art? What's the book to read for this stuff?
    - ihm 12y ago
      Yes, program is a term of art. It means a "term" in the type theory under consideration. A type theory is essentially a programming language with a fancy type system, and there are many type theories, just as there are many programming languages. It does allow for functions without computable rules. In the case of the axiom of choice, one postulates as an axiom a program with a type that says something like "give me a type A and an A-indexed family of types, P : A -> Type, such that for all a:A, the type P a is non-empty, and I'll give you a function f : (a : A) -> P a". As far as I know, there is still no one comprehensive book on type theory. I think the type theory parts of the homotopy type theory book (https://hottheory.files.wordpress.com/2013/03/hott-online-611-ga1a258c.pdf https://hottheory.files.wordpress.com/2013/03/hott-online-61...) are quite good. Chapter 1 gives the basics of dependent type theory. Chapter 2 is about the groupoid interpretation of type theory and is quite nice. Chapter 3 is about "logical things" in type theory (things like axiom of choice). Chapter 5 is about inductive types which are quite central to type theory (these are generalizations of algebraic data types like trees and lists from functional programming languages).
monochromatic 12y ago
After a certain point, you don't understand mathematical ideas. You just get used to them.

jordigh 12y ago

Yeah, the thing with formal definitions is that they're like little programs you have to compile before you can see their output. Trying to understand what a function is from a statement such as "a function from A to B is a subset F of the cartesian product AxB such that for all (a1,b1), and (a2,b2) in F, b1=b2 whenever a1=a1" really obscures the notion this is all about "mapping" or "doing" something. This definition is more like something that you would feed to a computer who doesn't "understand" what really is going on. Or to a human, who would work through it piecemeal, and try to build a few functions following this definition until the a-ha moment would come and this human would form a different intuitive understanding of what a function is or does. But the reason we write definitions as little programs to be compiled is to make sure that there can be no room for ambiguity. You compile the definition and arrive at the same mathematical object as anyone else. If we define a function as a mapping or a procedure, then we just shifted one word for another and still have to elucidate what a mapping or a procedure is.

ihm 12y ago
Well, the set theoretic attempt to describe functions isn't a very nice one. Type theory gives a formal definition closer to the intuitive notion: a function from A to B is a program of type A -> B. I.e., a rule for turning things of type A into things of type B.
- jordigh 12y ago
  I admit I don't know much about type theory. I assume "program" is a term of art? Also, does this allow for functions that have literally undescribable rules, such as a function arising from the application of the axiom of choice? Wanting to allow such undescribable functions is the reason for the set theoretic definition. I assume "rule" isn't a term of art? What's the book to read for this stuff?
  - ihm 12y ago
    Yes, program is a term of art. It means a "term" in the type theory under consideration. A type theory is essentially a programming language with a fancy type system, and there are many type theories, just as there are many programming languages. It does allow for functions without computable rules. In the case of the axiom of choice, one postulates as an axiom a program with a type that says something like "give me a type A and an A-indexed family of types, P : A -> Type, such that for all a:A, the type P a is non-empty, and I'll give you a function f : (a : A) -> P a". As far as I know, there is still no one comprehensive book on type theory. I think the type theory parts of the homotopy type theory book (https://hottheory.files.wordpress.com/2013/03/hott-online-611-ga1a258c.pdf https://hottheory.files.wordpress.com/2013/03/hott-online-61...) are quite good. Chapter 1 gives the basics of dependent type theory. Chapter 2 is about the groupoid interpretation of type theory and is quite nice. Chapter 3 is about "logical things" in type theory (things like axiom of choice). Chapter 5 is about inductive types which are quite central to type theory (these are generalizations of algebraic data types like trees and lists from functional programming languages).

monochromatic 12y ago

After a certain point, you don't understand mathematical ideas. You just get used to them.