What a great article. Paraphrased "Math is a designed thing, for humans and by humans, not an absolute truth." Also this post is the BEST introduction to linear algebra that I have seen.
to assume that maths is itself the absolute truth ,which suppesedly actual mathematics are supposed to lead to, is an apt syllogism. It's saying, any kind of math that doesn't reveal an absolut truth isn't real maths.
I've had a similar thought as the author, and often wondered - could we develop alternative systems for intermediate-to-advanced mathematical concepts that would make it easier to parse?
"Geometric algebra and its extension to geometric calculus unify, simplify, and generalize vast areas of mathematics that involve geometric ideas, including linear algebra, multivariable calculus, real analysis, complex analysis, and euclidean, noneuclidean, and projective geometry. They provide a unified mathematical language for physics (classical and quantum mechanics, electrodynamics, relativity), the geometrical aspects of computer science (e.g., graphics, robotics, computer vision), and engineering."
It has been called many things ("general abstract nonsense", etc.), but I don't know if it has ever been called "an easier way to explain things to non-mathematicians." :)
Nobody thinks category theory is easy for nonmathematicians, but the point of it is that it provides a common language for talking about common behaviors across many different, seemingly disparate, fields of mathematics, for mathematicians.
Very much so. This has in recent times become something of a lingua franca for mathematicians in recent times. The most useful (and astounding) property is that it gives formal definitions that apply across disciplines, which often perfectly coincide with informal usages of the same names for similar constructs in different fields.
For example, in mathematics we often have the notion of a product of two structures. The simplest is the product of two sets A and B, which in computer programming terms would just be a structure containing a field of type A and a field of type B. There are more subtle and sophisticated examples in other fields like topology, but it turns out that the categorical definition[1] matches the definition of product mathematicians were already using in each of these fields, even though it came about much later!
I'm a big fan of linear algebra because it's the best example of why learning math is useful. Sure knowing about equation and calculus come in handy, but linear algebra is pure modelling superpowers and a much more valuable tool overall.
I definitely think linear algebra has a lot of practical applications, but I'm not sure I would necessarily call it the "best" nor the "most valuable tool overall". It certainly provides the most bang for your buck if you are doing certain kinds of modeling, but even just within modeling which tool will be the most useful will depend a ton on what you are doing. For example, for dynamical systems you may be using linear algebra, but mostly as a computational tool for solving differential equations. In this case, analysis of your problem at the level of calculus is extremely important if you want to come up with an accurate and computationally feasible model.
I don't think you can say of any topic in mathematics that it's the best example of why learning math is useful. What about calculus? It's an immensely powerful tool that, by harnessing the power of the infinite and the infinitesimal, unlocks a massive body of practical applications in nearly every field of quantitative knowledge. And what about discrete math? Without it there would be no such thing as a computer. Differential equations, the tool for modeling dynamical systems?
Mathematics is a vast topic that every quantitative discipline must necessarily draw from. Each field of study will benefit more from certain topics of it.
> What about calculus [...and...] differential equations ?
I agree that calculus and diff. equations techniques are important, but if you look closely, you'll see they are only "necessary" for engineers and physicists, and other "hard" sciences, and not so essential for non-science studies.
Imagine "pitching" the benefits of learning university-level math to a class of Arts students. Can you honestly say their lives will be improved if they were to learn about a bunch of techniques of integration?
On the other hand, I wouldn't hesitate to recommend learning LA to them. Thinking about operators, vector spaces, dimensions, etc. is applicable much more widely. (I speak from experience here, because I've been "finishing up" the applications chapter in my LA book and I keep finding new applications to cover: balancing chemical equations, electric currents and other network flows, nutrition, least squares approximations, linear programming, cryptography, network coding, error correcting codes, Fourier analysis, prob. theory, and quantum mechanics. The LA party just don't stop ;)
I remember in my college linear algebra class (I think it was) that my prof made the joke that his wife was the projection of the vector representing all the attributes of his ideal woman into the space that represented the pool of all women who would date him.
I thought it was hilarious. Almost made me want to be a math major (I was just a physics major). Which makes me think of: https://www.xkcd.com/435/
I certainly wouldn't pick linear algebra as generally useful for "Arts students". Certainly something like probability or statistics is of much more general benefit to a typical person.
Not trying to evangelize but FP was an great hint for that. Seeing 'tangible' (that I can create, see, step through) incarnations of groups, monoids, transitive relations etc gave an operational grounding to abstract algebra. Something needed for some of us before see the abstraction behind the notation, and understanding it.
The perception of FP as being somehow more "math-y" is nothing but a bias. There is no intrinsic magical property of "mathiness", it's just that the operational semantics of functional languages are much more well-defined. Logic programming is itself firmly based in axiomatic semantics and has a similar a priori system of reasoning to it, though distinct from FP. Imperative languages can be modeled well on Hoare logic, too, and Dijkstra did plenty of research on it, known as predicate transformer semantics. It is comparatively understudied, though.
How come is it a bias ? FP takes root in recursive functions, and inductive reasoning. The same ideas we learn in math classes.
And describing pre / post invariants of imperative statements, turns them into typed functions isn't it ? I'm having a hard time seeing the difference.
Well, nobody is proposing that Turing Machines be the foundation of mathematics, whereas the sort of type theory used in FP is being taken pretty seriously as a foundation.
I agree that FP isn't more mathematical than other forms of programming.
the operational semantics of functional languages are much more well-defined.
No. The operational semantics of any language that has a compiler or interpreter is as well-defined as possible. What you may mean is that the meta-theory of (pure) FP is better understood than the meta-theory of other paradigms, typically because FP has simpler meta-theoretic properties.
Logic programming is itself firmly based in axiomatic semantics
This is a non-standard use of the term "axiomatic semantics" which is usually referring to Hoare-logic with pre- and post-conditions. Prolog has (simplifying a bit) a proof-theoretic / proof-search / resolution-unification-based semantics.
[Hoare-logics for imperative languages] is comparatively understudied, though.
That used to be the case, but the last decade has seen extreme progress in this matter, and Hoare logics for imperative languages are routinely used these days.
It is also interesting that there are many parallels between software engineering and the design of mathematical proofs (or theoretical CS proofs, which I am more familiar with).
In theoretical CS, people talk of catching and fixing "bugs" in proofs, namely, mistakes that make the proof fail but can hopefully be fixed while sticking to essentially the same idea.
One can "refactor" proofs, in superficial ways (e.g., renaming of concepts), but in deeper ways also, e.g., extract part of a proof to make it an independent lemma that you can reuse (or "invoke") from other parts of the proof. One often tries to "decouple" large proofs into independent parts with clearly defined "interfaces", that the reader can understand separately from each other, though this usually implies a tradeoff (a more tightly integrated proof requires more mental space but is usually shorter overall).
One can think of the statement of sub-results (lemmas) as providing an "interface" to invoke them elsewhere, which you try to "decouple" from the actual "implementation", namely, the way the lemmas are really proven. It takes practice to find the right way to abstract away the essence of a result to state it correctly, without burdening it with implementation details, but without forgetting an important aspect of the result that will be necessary later. As in software engineering, once a result is proven, you stop burdening your mind with the implementation and mostly think about the statement (i.e., what the result is supposed to be doing) when using it.
In software engineering, one must decide which part of the code is "responsible" for checking certain properties on the objects, and that code may "assume" some preconditions on its inputs and must "guarantee" some preconditions on its outputs. In the same way, in proofs, one often wonders where certain conditions should be verified. Should they be part of the definition of the object? Does this lemma enforce more conditions on the object than what is guaranteed by its statement?
The parallel is not perfect. In software engineering, you can rely on the computer to check that your code is correct, and to execute it. In mathematics you rely on other humans to do this and check that they are convinced by your proofs. This means you can get away with appeals to human intuition which are not fully formal, but on the other hand there is no safety net when you make an error in your reasoning, no reality check that you can invoke to avoid exploring erroneous consequences. Also, this does not apply to all types of proofs; but it applies especially well to proofs that describe a construction, i.e., a way to "build" a certain abstract object, often to justify that an object with a certain desirable set of properties exists.
If you are writing programs in Coq or another dependently typed programming language, these parallels between math and programming are not just incidental; they are one and the same. Theorems are stated as functions, whose type signatures reflect the theorem being proven. Even the gap that you mention at the end of your post is bridged, since the type checker will verify that your proof is correct (modulo the trust in the metatheory of the language itself, and its implementation). Things like refactoring, choosing more or less specific statements of theorems (e.g. more or less abstraction in a library), interfaces, etc, all become exactly analogous to the same kinds of problems faced in software engineering. It's really quite remarkable.
(Disclaimer: I'm hardly an expert in these languages; I just dabble.)
I've never taken a college-level linear algebra course, and I've found KhanAcademy's linear algebra course to be a good gentle introduction. I just skip the parts I already know.
Very good article. Studying computer science as my sole field, I am starting to realize how much I have missed out on getting an alternative take on things.
The other day I realized that a man-made law is also a bit like mathematics or computer software. It is carefully designed and constructed. Ideally, it is intended to work like a machine with as little room for human discretion as possible. And just like mathematics, adding an another "axiom" to the law has far, far-reaching consequences.
> And just like mathematics, adding an another "axiom" to the law has far, far-reaching consequences.
Actually mathematicians virtually never do this. Almost all of mathematics (from arithmetic to calculus to category theory) operates in the confines of ZFC[1] and adds no further axioms. All of these fields may add definitions, but these are just shorthand; the are conservative and have no actual consequences. It is more like fixing Newton's laws and then experimenting with all the machines you can build with them.
Most mathematicians don't spend their time considering extensions of ZFC, but mathematicians are always adding axioms in a different sense. Add a commutativity axiom to group theory and you get commutative group theory. Add an axiom that "the space has total measure 1" to measure theory and you get probability theory. And so on.
These are generally called axioms, but these are totally distinct from axioms in the sense of ZFC's axioms. They are simply part of the definition of a group, commutative group, etc. Since they are just part of the definition of the structure, choosing the "wrong axioms" will only result in a structure which has no actual instances, not in inconsistency of the underlying theory. As such, they most certainly don't have "far reaching consequences", except that some axioms may produce uninteresting structures.
> These are generally called axioms, but these are totally distinct from axioms in the sense of ZFC's axioms.
I wouldn't really say they're "totally distinct". For example, one could say that general group theory is studying the theory (in the logic sense) of a group (usually the second order theory rather than first order, but you get idea). Then adding assumptions about the structure of the group under consideration is like adding axioms and looking at the new theory.
This is a really hair-splitting distinction that only makes sense if mathematicians wrote proofs (e.g., about commutative group theory) while keeping ZFC's axioms in mind.
But even then, it's not really an appropriate distinction -- accidentally assuming inconsistency and moving forward with it is exactly as far-reaching as assuming inconsistency at the foundations. And, doing some obscure work on an inconsistent foundations that no body uses is exactly as harmless as doing some obscure work on a structure without elements.
> This is a really hair-splitting distinction that only makes sense if mathematicians wrote proofs (e.g., about commutative group theory) while keeping ZFC's axioms in mind.
They may not do so explicitly, but it is easy to see where the axioms become important when dealing with mathematical structures. For example, if you are considering the group of integers with addition, the existence of this group is predicated on the existence of the integers, which is predicated on the existence of the natural numbers as a set, which is an axiom of ZFC (axiom of infinity[1]). The case for other foundations is similar.
> But even then, it's not really an appropriate distinction -- accidentally assuming inconsistency and moving forward with it is exactly as far-reaching as assuming inconsistency at the foundations.
No, because when studying a mathematical structure we always consider concrete instances of it, which are usually in fact the motivation for the definition of the structure. So mathematics based on possibly (relatively) inconsistent structures (other than foundational systems) is not really a thing; group theory was not initiated prior to the discovery of structures satisfying the groups axioms, and neither was the study of rings, fields, modules, topological spaces etc. On the other hand, we cannot consider models of ZFC unless we build it within the assumptions of a foundational system (possibly ZFC itself). So at some point we have to pick a set of axioms to be the bottom of our ladder of turtles, and the axioms of that system are very special indeed.
Another difference is that the axioms of a group (or a field, or a topological space) cannot stand on their own; they clearly reference sets and functions. ZFC's axioms only reference sets, all of the fundamental properties of which are enumerated in the axioms themselves. If you gave an (english speaking) alien the definition of a group, he would need to ask you what the definition of sets and functions were. So even if we wanted the group axioms to be our foundations, this would not be possible.
For what odd-ball definition of "far reaching" is "anything" not "far reaching"? An assumption doesn't have to be an Axiom to have "far reaching" consequences. Period.
So, you're wrong -- assuming non-foundational axioms can have far reaching consequences. Assumptions are assumptions, and flaws are flaws. Assuming "false" is just as bad as working with an inconsistent foundations. It's just a fact.
That said, the actual difference you're trying to elucidate is sociological, not technical -- you suppose that people are less likely to accept non-foundational assumptions, and so that'll check back something from a sociological viewpoint. You assume people won't build results on top of a system with an unproven assumption thrown in.
That argument would be a lot more compelling if Mathematicians formalized their arguments in terms of an underlying foundations, because then we would always know that all assumptions are checked. But Mathematicians don't work like that. And errors creep in. And if people build on top of those errors, it can be pretty catastrophic.
In short, what matters is that people accept the incorrect fact and move forward from it, NOT whether that incorrectness comes from foundations or from something built on top of them. The impact of either depends entirely upon how many people trust the result and build on top of it.
The whole point is that all of the structural axioms are known to be consistent (relative to ZFC or another foundation) because there exist known models of them. The fact that we don't need to assume group axioms hold, but can instead prove they hold for at least one structure is a huge distinction. There is no way to prove there are models of ZFC or another (suitably powerful) foundational system without appealing to a foundational system in the first place. That is the content of Godel's second incompleteness theorem[1]. So the axioms of ZFC bear some scrutiny, while those of a group etc. don't. This is a completely technical distinction.
> That argument would be a lot more compelling if Mathematicians formalized their arguments in terms of an underlying foundations, because then we would always know that all assumptions are checked.
But they do! You can find many books on real analysis that prove that the reals exist from the foundation, as well as proving that the naturals and integers exist on the way. They don't constantly refer to the foundations, but they use facts that have been rigorously proved from the foundations. And although they don't write "axiom schema of specification" every time they consider a subset satisfying a property, that doesn't mean they don't know that it is required.
> In short, what matters is that people accept the incorrect fact and move forward from it, NOT whether that incorrectness comes from foundations or from something built on top of them. The impact of either depends entirely upon how many people trust the result and build on top of it.
My whole point is that you don't have to trust the group axioms, because they can (and typically are) validated relative to ZFC. Since the trivial group can be constructed within ZFC they are consistent in ZFC, full stop. The same goes for refinements like commutative groups. If the group axioms lead to a inconsistency, it can only be because ZFC itself is inconsistent. Do you not think that being a possible source of inconsistency or not is an important distinction?
>Actually mathematicians virtually never do this. Almost all of mathematics (from arithmetic to calculus to category theory) operates in the confines of ZFC[1] and adds no further axioms.
Except for all the non-ZFC foundations, like type theory or category-theoretic foundations.
Relatively speaking, there are very few mathematicians using those systems to discover new mathematics as opposed to studying them for their foundational interest.
They (and those who study ZFC extensions) are the reason I said "virtually"; they are most certainly a small minority among mathematicians. I myself have been studying homotopy type theory as of late.
Changes in law (almost) never add axioms because that would have global effects; instead, they tend to add folds to the manifold that law is. And many folds there certainly are. It is hard to find anything in law that holds universally. Examples (I’m picking mostly US law here, but I’m sure similar exceptions exist elsewhere):
- "Everyone has the right to take part in the government of his country, directly or through freely chosen representatives"? Not quite in the USA, as one must be born in the USA to become president.
- "higher education shall be equally accessible to all on the basis of merit": questionable in many countries, given the costs.
It seems there’s no rule so universal that it doesn’t have some exception. That, IMO, makes law so different from math that any analogy is useless.
If it were just that the axioms of law are more complicated in the sense of being more conditional, then law would be extremely math-like. After all, theorems with lots of conditional properties (e.g., very common in certain types of algebra, a lot of dynamics, any programming language theory, etc.) are still mathematical theorems.
Law is distinguished from Math in two ways:
1) Law has more politics and isn't immune from politics. Mathematical truth, at least, is.
2) In law, the atomic propositions are always difficult to quantify and require human judgement; there is rarely an algorithm for weighing the evidence and determining guilt (or constitutionality, etc).
>Ideally, it is intended to work like a machine with as little room for human discretion as possible
Actually, these laws are the most dystopian.
One concept that seems to have this design goal is strict liability: what you intended, what you believed, what elaborate conspiracies were created to deceive you, none of that matters. If you did it, you are guilty and will be punished, full stop. This is attractive because it's much harder to prove beyond a reasonable doubt that someone did something "with malice" or "intentionally" than to prove that they did it. This tends to show up around youth sexuality, probably because that's an area where social norms have changed quite a bit.
It doesn't matter if the 17.5-year-old you slept with presented a fake ID saying she was 18, took the lead in all sexual activity, etc. It doesn't matter if she shows up in court and begs the judge to let you go. People whose 18th birthday has not elapsed cannot give consent, full stop. Sex without consent is rape, rapists are bad people and should be made to suffer, so you're going to prison and then on to the sex offender registry. Your judge, and the judges you appeal to, all think this is ridiculous, but their hands are tied because the law was written like a computer program that failed to consider edge cases. (Literally edge cases - those that fall near numerical boundaries. Some states have patched their legal systems to allow consent between partners who are close in age but under the normal age of consent. Some have, but only for heterosexual couples. Some still haven't. My state actually tried and convicted two teenagers as adults for raping each other at the same time.)
Same with child porn. Child porn laws were created a time when taking and distributing a picture could only be part of a commercial publishing operation. Anyone who creates or possesses an image of a nude child is guilty of a child pornography offense. Seems reasonable. Now every teenager has an internet-connected camera in their process, and we found an edge case we forgot: the child pornographer is the child him/herself and the consumer is her long-term boyfriend, also underage. Still just as illegal and the same punishment is required. You would hope prosecutors would turn a blind eye, but "the law is the law."
These rather salacious examples are the most high-profile, but I'm sure the same problems happens in more mundane areas of law as well.
At some point you have to trust judges and you have to empower bureaucrats to help people get out of obviously ridiculous situations. Laws are much more difficult to change than computer programs; there needs to be a reasonable amount of discretion for a manual override until the law can be fixed.
Well said. Advanced math is mostly about working with properties higher up the chain of abstraction, and then seeing what happens when you bring the insights learned up there back down to more concrete examples.
From an OO point of view, the real numbers inherit almost every useful trait: they're a field, they have a topology, they have a measure. Studying the parent classes, so to speak, gives you abstract algebra, topology, and analysis, respectively.
Once you get the basics of each, you can study how they interact. Then, once that stuff is clear, they can be recombined in beautiful ways to give you new objects to study.
"Well said. Advanced math is mostly about working with properties higher up the chain of abstraction, and then seeing what happens when you bring the insights learned up there back down to more concrete examples."
I came here to say the same thing. I went through a lesser known engineering discipline, "Mathematics and Enigneering" [0] and found that the type of thinking one learns doing pure math proofs has served me well in my eventual career in aerospace systems engineering. I find that the thought process in considering a proof as a high level whole/black box or being able to drill down to the finest detail while still keeping the big picture in mind has translated quite well to my day to day traversal up and down the abstraction ladder at work.
Context: I never did too well in statistics, and in general I was always pretty bad at understanding simple Math notation like sigma notation, multi-variate calc, or linear algebra.
For me to understand the paper, I had to go through the code to piece out the Math jargon, even though the Math behind it is really quite simple. Another way of saying this is, "I'm dumb," sure. Not gonna argue with anyone there.
Though I still think it's curious why it's easier for me to understand a concept through code than it is through Math. It's sort of reminiscent of when you first learned Algebra, your teacher would tell you to replace the variable with an easy number and work through it to understand the mechanics of equations.
I think code is an example of that - literally working through the mechanics of algorithms to understand what they actually do and how they work.
I think it's probably just that you have far more relevant experience with reading code. Math is its own language, and math departments only really start teaching how to read and write it in Real Analysis classes. As my math professor stepfather said his advisor once put it, "Everything before that is just to keep the children from running in the halls."
This is too perfect. I did a minor in math, and covered two semesters of real analysis and two of algebra, plus an optimization class and some advanced (undergraduate) statistics, and holy crap I felt like I was joining the grown up table when I started.
I've always wondered why Real Analysis isn't introduced earlier in math education. It might make it easier to grasp concepts introduced in upper-level math.
That's why so many people point to Spivak's Calculus book, since it has been hinted it should be called an analysis text. Strang's Calculus, as do others, start with real-world examples. Personally, I had to do the Strang route, and then come back to Spivak, since I had to admit to myself, I don't have that ability to think 100% abstractly; I need motivation from the real world.
Not surprising at all. If someone is not familiar with the notation it can certainly get in the way. Furthermore math notation is very context sensitive, so possibility of confusion abounds.
Mathematical truths and objects are real things with existence independent of our minds that we "discover," not just designed things. The author seems to believe that the language used to describe mathematics (which is indeed a designed thing, just like software) is the only thing "there." She is probably a formalist.
I think it is important to remember this, because mathematics, like a computer, "fights back." You cannot simply dream up whatever structure you want and have it mean what you want and behave how you want. See Godel's incompleteness theorems. No matter what you are doing, your mathematical constructs (including your implicit Turing Machines in your computer programs) must obey certain underlying constraints that are completely mind-independent. These constraints are what mathematicians study, albeit through a glass, darkly.
Regardless of ontological issues with the post, I like that it emphasizes the designed nature of our mathematical tools. The space of possible tools is so large that there is near-limitless room for human creativity and design in mathematical research. It is a shame that most mathematics classes don't really get that across.
You can simply dream up whatever axioms, undefined terms, and rules of logic you want. However, one runs the risk of having an inconsistent system or a system that is not interesting to others. Godel's Incompleteness Theorem does not say that this can't be done. Furthermore the "underlying contraints" imposed by Godel's Incompleteness Theorem is not at all what most mathematicians study. Unless I'm misinterpreting your meaning here.
There are knowledgeable people who do not believe that mathematics is independent of our minds. It's not too far fetched of an idea. While I do not personally agree with this, I won't downplay such beliefs.
>Mathematical truths and objects are real things with existence independent of our minds
What makes you say this? Isn't this an open philosophical question? What makes you say that mathematical objects exist independent of our minds? I can dream up a set of axioms of my own and do maths from there, so I don't think mathematics necessarily exists in some Platonic ideal dimension independent of our minds.
>Mathematical truths and objects are real things with existence independent of our minds that we "discover," not just designed things.
While its almost certainly true that the content of mathematics is mind independent, it is far from obvious that these objects are "real things".The real meat of the issue is how exactly the mind-independence is cashed out. Different ideas paint a vastly different picture of mathematics and even the universe. For example platonism vs. nominalism. Lets not be so quick to put forward as an obvious truth the critical issue in question.
Can't a mathematical theory compress, generalize, and map out many relevant empirical facts very well without needing ontological commitments to the generalizations themselves?
The real numbers seem to be a perfect example: if you work in physics at scales where quantization doesn't noticeably apply, the only way to calculate correct predictions is really to use real numbers and continuous (mostly Euclidean) spaces. But that doesn't mean physical objects are ontological shadows of our mathematical abstractions, as Plato's Allegory of the Cave portrayed it. Quite the reverse: when you get down to a sufficiently small, fundamental level, objects, space, and time stop being continuous and correct experimental predictions only come from using discrete formalisms.
You can then proceed to ask, which one is Platonically real, the continuous mathematical spaces or the discrete physical ones? But I think the answer there might be, "Who says anything is Platonically real? The map is not the territory, so shut up and calculate."
>Can't a mathematical theory compress, generalize, and map out many relevant empirical facts very well without needing ontological commitments to the generalizations themselves?
Maybe, but its not obvious. The fact that the same generalizations are multiply realizable in different processes/structures certainly says something interesting. The consequences of this multiple realizability hasn't been fully investigated.
Your response seems to be arguing against my post which was mainly about mind-independence, by arguing against platonism. I don't see that mind-independence necessarily implies platonism. In fact, I find all forms of platonism extremely distasteful.
>The map is not the territory, so shut up and calculate.
Right, but this in fact goes to the heart of the question of the philosophy of mathematics. When someone says that mathematical objects are mind-independent, they are not talking about the notation itself (the map), but rather the content of the notations (the territory), i.e. the structure revealed through the notation. It should be pretty obvious that there are many interesting questions about the mind-independent structure of the territory. "Shut up and calculate" isn't an answer to this question, but rather the attitude that the answer simply doesn't matter. For many fields the answer doesn't matter, but the question is worth asking nonetheless.
I don't think math exists without sentience, it is a construct . What math describes can and is "real" in the traditional sense, but that doesn't necessarily make objects, concepts in mathematics "real objects." I take this position with language as well, it's all a metaphor.
But observations of real world systems can be identical to a specific mathematical system. I.e. the time it takes for a thing to fall at specific gravity at specific height, the frequency of a particular pendulum, and so on...(i.e. the rest of modern physics).
True, it is our observation and our model which are similar, so I suppose the philosophical question then is up to what point we can trust our observations. And if we trust our observations, I would conclude that the similarity of our observations and math means that the real world can at least exhibit 'maths', which means our minds are not the only place where math can exist.
The smartphone I'm typing this on leads me to conclude that lots of our observations are highly trustworthy :)
Yes, I think that humans have some ways to make sense of the external world, and math is one of them. May not be highly developed, could be buggy. Probably lots of things we could never figure out, like rats who can't solve mazes where they need to turn at prime numbers.
Our math sense could even conflict with our other useful facilities (as is the case with how easily fooled humans are when it comes to statistics).
>You cannot simply dream up whatever structure you want and have it mean what you want and behave how you want. See Godel's incompleteness theorems.
That is not at all what the Incompleteness Theorems actually say. They say literally nothing whatsoever about what sorts of structures you can implement inside a given foundational theory, except that there will always be more, because given any foundational theory, you can construct two more foundational theories as extensions (one in which the Goedel statement is unprovable, and one in which the theory believes it's inconsistent).
Interesting article. I always thought math felt like programming but in a language far higher level than any of the available programming languages. So like programming but with a lot less friction when going from thought to symbols.
For example, creating new domain specific control flows with Lisp macros versus defining a Dirac delta function using limits and integrals. In programming it's easy for bugs to seep in because there are more little/subtle details and leaky abstractions. But math on the other hand feels much more abstract and clean.
Perhaps this is just because dumb silicon boxes interpret our code and humans interpret our math which gives us a much more sophisticated base language to work with.
At the end of the article, the author mentions how we could possibly find other designs of mathematics. Well, some people already have!
Some mathematicians did not like the law of excluded middle, which states that for any proposition A, either A is true or A is false. So they invented intuitionistic logic, which is normal logic without the excluded middle, and started rewriting mathematical proofs in this new system. Turns out there's a lot of stuff you can prove in intuitionistic logic.
Some mathematicians did not like the axiom of choice. One of the consequences of this axiom is that every subset of the real numbers has a least element according to some ordering. Think about it, what is the least element of {1/n : n >= 1} ? Who knows! So what did they do? Some people found it so weird they either replaced it with a weaker axiom or a contradictory one.
There's even syntax arguments in mathematics! What's the derivative of a function f? is it f'(x) or df/dx ? Is multiplication represented by a dot (.) or a cross (x) or by a juxtaposition of expressions?
Sometimes we use big existing proofs in the middle of a proof to save time. And sometimes we use the big proof to prove something far simpler than the big proof. This creates a big dependency and some people dislike hate these dependencies because the reader of the new proof will have trouble understanding the proof completely. It's like dropping in some magic in the middle of the proof and saying: "if you want to understand this proof completely, go read this other 50 page article" Sound familiar? Some mathematicians hate this so much they insist on proving things from the ground up whenever possible so that the proof is as comprehensible as possible. This is the mathematical equivalent of dependency management.
> One of the consequences of this axiom is that every subset of the real numbers has a least element according to some ordering.
An even weirder consequence of AC is the Banach-Tarski paradox [1].
Other examples of how mathematicians come up with alternative
perspectives are non-Euclidean geometries that replace the parallel postulate of the common Euclidean geometry, e.g. Lobachevskian [2] and Riemannian geometry [3].
Yup! (I think rathereasy chose an unfortunate example.) The point is that AC implies that there is a way to put an ordering on all of R such that every nonempty subset has a smallest element.
It's easy to find such an ordering for any countable subset -- i.e., one that set-theoretically is no bigger than the integers. For instance, we can do it for all the rational numbers by saying that we order numbers p/q (p,q integers, no common factor, q positive) by converting p/q to 2^signbit(p) 3^|p| 5^|q| or something of the kind, where signbit(x)=0 is what in C you write as (x<0), and comparing the positive integers that result.
It's much harder to see how to do it for all the real numbers. In fact, you provably can't see how, in the sense that there actually is known to be no construction that does it -- no way to say explicitly which numbers to put before which.
(This is a common pattern; cases where you need AC to do something are always ones where there is no explicit construction that does it. That kinda has to be true, because there are models of set theory in which AC is false.)
The point is that there is one ordering in which every subset of real numbers has a minimum.
For the rational numbers, this is not difficult, since we can enumerate the rational numbers. As the ordering we could then pick "a <= b" if the index of "a" in the enumeration is less than the index of "b". The least element of any set of rational numbers is then the rational number with the least index in that set.
However, the real numbers are uncountable. Tricks like this cannot work.
----
The real culprit is the axiom of excluded middle, which confounds the notions of existence and embodiment. Under classical logic it may be proven that P = NP, even though no algorithm actually exists. This already happened for certain graph problems... (=> Graph minor theorem, moving from minor-closed graph property to finite set of excluded minors is essentially non-constructive.)
Without excluded middle, the axiom of choice is exactly as trivial as it sounds: Given a non-empty set, give me an element in that set. In order to show that a set is non-empty you need to give enough information to construct an element in that set. So the proof contains the information to validate the "axiom".
With excluded middle, the proof that a set is non-empty doesn't contain enough information to pick an element from that set. So adding both excluded middle and choice takes you into an axiomatic system whose connection with the real world is rather tenuous.
----
The article is spot on: Not only is mathematics a designed system, but the analogy between programming languages and logic is perfect in view of the Curry-Howard correspondence. Elevating Zermelo-Fraenkel set theory is like insisting that your software project has to be built using Turing machines. After all, everything else is just encoding. There is a huge design space in logics as well as in programming languages. For instance, you can do physics in the setting of synthetic differential geometry and work without preconditions and use theorems which are literally impossible in ZFC.
A soundness proof for a new logic is, by the way, the logical equivalent of building a compiler. :)
Careful, the axiom of choice doesn't state that non-empty sets contain an element (this is a triviality). Rather (an equivalent of) it states that the Cartesian product of non-empty sets is non-empty. If we take a product of finitely many such sets, then we can prove it, but we need the axiom of choice for the infinite case.
The reason is intuitively clear: in order to prove that the infinite product is non-empty, we need to produce an infinitely long vector. Well, since the individual sets are non-empty, we can just for each set choose an element and put it in the vector. But this takes infinitely many steps! and that's not allowed in mathematics. The axiom of choice is a way of collapsing infinitely many steps into 1 invocation of the axiom (so 1 step, so finitely many steps). Not too much to do with excluded middle.
There are many classically equivalent formulations of the axiom of choice, the one I gave is just the one I like best. :)
But you are right, the devil is in the details, so let me spell it out precisely:
The axiom states that for every set X, there is a function
\epsilon : P(X)/{\empty} -> X
If you want to restrict yourself to first-order logic, then you have to encode the function \epsilon (e.g. as a functional relation, where relations are in turn encoded as sets of ordered pairs, which are in turn encoded with Kuratowsky's construction). Set theorists like first-order logic and this encoding overhead is the reason why it's not the standard definition, even though it's arguably what the axiom is trying to express(1,2). Apart from that the statements are (classically) equivalent:
To go from the higher-order version to the cartesian product, note that the cartesian product of an I-indexed family of sets is a set of functions f from I to the union of all X_i's, such that f(i) \in X_i for all i. Let (X_i)_{i\in I} be an I-indexed family of sets, all of which are non-empty, then (i -> \epsilon(X_i)) is in the cartesian product of the X_i's, where we use \epsilon for the union of all X_i's. The reason we couldn't build that element without AC is precisely that we have no way of selecting exacly one element from each X_i, even though we know that they are non-empty.
In the other direction we can use Zermelo's well-ordering theorem to construct a well-order on X. We define \epsilon to pick out the minimum with respect to this order.
(1) This really is what the axiom of choice was meant to express. If you can read German, you can refer to Zermelo's own work:
https://eudml.org/doc/158167
Under point 2 in this paper, Zermelo assumes that there is such a choice function on a given set and from this he derives the well-ordering of that set.
(2) Another example of the drawbacks of working with a first-order axiomatization is the axiom of regularity. The idea we want to express is that there are no infinitely descending element chains ("every set is well-founded"), but expressing this in first-order logic leads to a convoluted statement which obscures the simple idea... and is also not a correct encoding of this idea in intuitionistic logic!
> There's even syntax arguments in mathematics! What's the derivative of a function f? is it f'(x) or df/dx ? Is multiplication represented by a dot (.) or a cross (x) or by a juxtaposition of expressions?
Those aren't arguments. All of those are very standard things to do.
There's a Spiked Math comic with some good mathematics-engineering trash talk, though, with the mathematicians shooing away a hapless engineer with comments like "do you even know how to spell 'imaginary'?" and "why don't you go jmagine you have friends?" Again, I wouldn't describe this as an area of active debate.
Weirdly enough, I always struggled with advanced syntax, but I recently understood that it was a lack of focus on the abstraction. Kinda like programming languages :)
But that's something you can't really understand when too young.
I would like to add, sometimes mathematicians bring up random variables/constants without explicitly naming or explaining them before. This is very upsetting for someone with a lower level, trying to understand what's going on.
Is there a version of mathematics, somewhere, that don't give you the impression of being snarked upon by an old dude twirling his mustache?
You can play creatively in a particular nexus of math and software engineering called Djinn [0], the Haskell program that writes your Haskell programs for you.
1. An ancestor of Djinn is automated theorem proving. Why can't machines prove math theorems for us? This quest goes back to the dawn of computing science.
2. A more recent development is the Curry-Howard Correspondence. Programming in a (typed) FP language is like playing tetris. Solving symbolic logic problems [1] is also like playing tetris. Djinn exposes the connection in a REPL you can play with. And see how the computer plays tetris for you!
3. Don't want to install Djinn? No problem, just hop over to the Haskell IRC [2]. Lambdabot has a working Djinn plugin.
Understanding programming languages definitely helped my understanding of Math. Smarter people than myself can do this the other way around, but I always needed to understand the why before it could start to stick. I didn't really understand programming languages until I could dig into the source code and the standard libraries to see how and why everything was done. The problem with modern math teaching is that is starts with fully baked axioms and it doesn't walk you through the process of discovery before it was all cleaned up into a neat terse explanation. One exception is a great book from the 40s called a Mathameticians Delight. It was recommended to my by my Yale professor and I highly recommend it.
96 comments
[ 2.8 ms ] story [ 169 ms ] threadFrom the first page:
"Geometric algebra and its extension to geometric calculus unify, simplify, and generalize vast areas of mathematics that involve geometric ideas, including linear algebra, multivariable calculus, real analysis, complex analysis, and euclidean, noneuclidean, and projective geometry. They provide a unified mathematical language for physics (classical and quantum mechanics, electrodynamics, relativity), the geometrical aspects of computer science (e.g., graphics, robotics, computer vision), and engineering."
For example, in mathematics we often have the notion of a product of two structures. The simplest is the product of two sets A and B, which in computer programming terms would just be a structure containing a field of type A and a field of type B. There are more subtle and sophisticated examples in other fields like topology, but it turns out that the categorical definition[1] matches the definition of product mathematicians were already using in each of these fields, even though it came about much later!
[1]: https://en.wikipedia.org/wiki/Product_(category_theory)
I'm a big fan of linear algebra because it's the best example of why learning math is useful. Sure knowing about equation and calculus come in handy, but linear algebra is pure modelling superpowers and a much more valuable tool overall.
Related: An awesome LA introductory lecture by Prof. Strang: http://ocw.mit.edu/courses/mathematics/18-06-linear-algebra-...
Related 2: A short tutorial on LA that I wrote: http://minireference.com/static/tutorials/linear_algebra_in_...
Mathematics is a vast topic that every quantitative discipline must necessarily draw from. Each field of study will benefit more from certain topics of it.
I agree that calculus and diff. equations techniques are important, but if you look closely, you'll see they are only "necessary" for engineers and physicists, and other "hard" sciences, and not so essential for non-science studies.
Imagine "pitching" the benefits of learning university-level math to a class of Arts students. Can you honestly say their lives will be improved if they were to learn about a bunch of techniques of integration?
On the other hand, I wouldn't hesitate to recommend learning LA to them. Thinking about operators, vector spaces, dimensions, etc. is applicable much more widely. (I speak from experience here, because I've been "finishing up" the applications chapter in my LA book and I keep finding new applications to cover: balancing chemical equations, electric currents and other network flows, nutrition, least squares approximations, linear programming, cryptography, network coding, error correcting codes, Fourier analysis, prob. theory, and quantum mechanics. The LA party just don't stop ;)
I thought it was hilarious. Almost made me want to be a math major (I was just a physics major). Which makes me think of: https://www.xkcd.com/435/
i.e. not Arts, History or Literature :)
And describing pre / post invariants of imperative statements, turns them into typed functions isn't it ? I'm having a hard time seeing the difference.
In theoretical CS, people talk of catching and fixing "bugs" in proofs, namely, mistakes that make the proof fail but can hopefully be fixed while sticking to essentially the same idea.
One can "refactor" proofs, in superficial ways (e.g., renaming of concepts), but in deeper ways also, e.g., extract part of a proof to make it an independent lemma that you can reuse (or "invoke") from other parts of the proof. One often tries to "decouple" large proofs into independent parts with clearly defined "interfaces", that the reader can understand separately from each other, though this usually implies a tradeoff (a more tightly integrated proof requires more mental space but is usually shorter overall).
One can think of the statement of sub-results (lemmas) as providing an "interface" to invoke them elsewhere, which you try to "decouple" from the actual "implementation", namely, the way the lemmas are really proven. It takes practice to find the right way to abstract away the essence of a result to state it correctly, without burdening it with implementation details, but without forgetting an important aspect of the result that will be necessary later. As in software engineering, once a result is proven, you stop burdening your mind with the implementation and mostly think about the statement (i.e., what the result is supposed to be doing) when using it.
In software engineering, one must decide which part of the code is "responsible" for checking certain properties on the objects, and that code may "assume" some preconditions on its inputs and must "guarantee" some preconditions on its outputs. In the same way, in proofs, one often wonders where certain conditions should be verified. Should they be part of the definition of the object? Does this lemma enforce more conditions on the object than what is guaranteed by its statement?
The parallel is not perfect. In software engineering, you can rely on the computer to check that your code is correct, and to execute it. In mathematics you rely on other humans to do this and check that they are convinced by your proofs. This means you can get away with appeals to human intuition which are not fully formal, but on the other hand there is no safety net when you make an error in your reasoning, no reality check that you can invoke to avoid exploring erroneous consequences. Also, this does not apply to all types of proofs; but it applies especially well to proofs that describe a construction, i.e., a way to "build" a certain abstract object, often to justify that an object with a certain desirable set of properties exists.
(Disclaimer: I'm hardly an expert in these languages; I just dabble.)
I've never taken a college-level linear algebra course, and I've found KhanAcademy's linear algebra course to be a good gentle introduction. I just skip the parts I already know.
Actually mathematicians virtually never do this. Almost all of mathematics (from arithmetic to calculus to category theory) operates in the confines of ZFC[1] and adds no further axioms. All of these fields may add definitions, but these are just shorthand; the are conservative and have no actual consequences. It is more like fixing Newton's laws and then experimenting with all the machines you can build with them.
[1]: https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_t...
I wouldn't really say they're "totally distinct". For example, one could say that general group theory is studying the theory (in the logic sense) of a group (usually the second order theory rather than first order, but you get idea). Then adding assumptions about the structure of the group under consideration is like adding axioms and looking at the new theory.
But even then, it's not really an appropriate distinction -- accidentally assuming inconsistency and moving forward with it is exactly as far-reaching as assuming inconsistency at the foundations. And, doing some obscure work on an inconsistent foundations that no body uses is exactly as harmless as doing some obscure work on a structure without elements.
They may not do so explicitly, but it is easy to see where the axioms become important when dealing with mathematical structures. For example, if you are considering the group of integers with addition, the existence of this group is predicated on the existence of the integers, which is predicated on the existence of the natural numbers as a set, which is an axiom of ZFC (axiom of infinity[1]). The case for other foundations is similar.
> But even then, it's not really an appropriate distinction -- accidentally assuming inconsistency and moving forward with it is exactly as far-reaching as assuming inconsistency at the foundations.
No, because when studying a mathematical structure we always consider concrete instances of it, which are usually in fact the motivation for the definition of the structure. So mathematics based on possibly (relatively) inconsistent structures (other than foundational systems) is not really a thing; group theory was not initiated prior to the discovery of structures satisfying the groups axioms, and neither was the study of rings, fields, modules, topological spaces etc. On the other hand, we cannot consider models of ZFC unless we build it within the assumptions of a foundational system (possibly ZFC itself). So at some point we have to pick a set of axioms to be the bottom of our ladder of turtles, and the axioms of that system are very special indeed.
Another difference is that the axioms of a group (or a field, or a topological space) cannot stand on their own; they clearly reference sets and functions. ZFC's axioms only reference sets, all of the fundamental properties of which are enumerated in the axioms themselves. If you gave an (english speaking) alien the definition of a group, he would need to ask you what the definition of sets and functions were. So even if we wanted the group axioms to be our foundations, this would not be possible.
[1] : https://en.wikipedia.org/wiki/Axiom_of_infinity
1. Assume false.
2. Anything follows.
For what odd-ball definition of "far reaching" is "anything" not "far reaching"? An assumption doesn't have to be an Axiom to have "far reaching" consequences. Period.
So, you're wrong -- assuming non-foundational axioms can have far reaching consequences. Assumptions are assumptions, and flaws are flaws. Assuming "false" is just as bad as working with an inconsistent foundations. It's just a fact.
That said, the actual difference you're trying to elucidate is sociological, not technical -- you suppose that people are less likely to accept non-foundational assumptions, and so that'll check back something from a sociological viewpoint. You assume people won't build results on top of a system with an unproven assumption thrown in.
That argument would be a lot more compelling if Mathematicians formalized their arguments in terms of an underlying foundations, because then we would always know that all assumptions are checked. But Mathematicians don't work like that. And errors creep in. And if people build on top of those errors, it can be pretty catastrophic.
In short, what matters is that people accept the incorrect fact and move forward from it, NOT whether that incorrectness comes from foundations or from something built on top of them. The impact of either depends entirely upon how many people trust the result and build on top of it.
> That argument would be a lot more compelling if Mathematicians formalized their arguments in terms of an underlying foundations, because then we would always know that all assumptions are checked.
But they do! You can find many books on real analysis that prove that the reals exist from the foundation, as well as proving that the naturals and integers exist on the way. They don't constantly refer to the foundations, but they use facts that have been rigorously proved from the foundations. And although they don't write "axiom schema of specification" every time they consider a subset satisfying a property, that doesn't mean they don't know that it is required.
> In short, what matters is that people accept the incorrect fact and move forward from it, NOT whether that incorrectness comes from foundations or from something built on top of them. The impact of either depends entirely upon how many people trust the result and build on top of it.
My whole point is that you don't have to trust the group axioms, because they can (and typically are) validated relative to ZFC. Since the trivial group can be constructed within ZFC they are consistent in ZFC, full stop. The same goes for refinements like commutative groups. If the group axioms lead to a inconsistency, it can only be because ZFC itself is inconsistent. Do you not think that being a possible source of inconsistency or not is an important distinction?
[1]: https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...
Except for all the non-ZFC foundations, like type theory or category-theoretic foundations.
- everybody can vote? Well, we have https://en.wikipedia.org/wiki/Felony_disenfranchisement and, on the other end of the spectrum, in the UK "Although the law relating to elections does not specifically prohibit the Sovereign from voting in a general election or local election, it is considered unconstitutional for the Sovereign and his or her heir to do so” (http://www.royal.gov.uk/MonarchUK/QueenandGovernment/Queenan...)
- everybody with a sufficiently high income must pay social security taxes? Not if you’re member of certain religious groups (https://faq.ssa.gov/link/portal/34011/34019/Article/3821/Are...)
Even the universal declaration of human rights (http://www.un.org/en/documents/udhr/) often has small exceptions. For example:
- "Everyone has the right to take part in the government of his country, directly or through freely chosen representatives"? Not quite in the USA, as one must be born in the USA to become president.
- "higher education shall be equally accessible to all on the basis of merit": questionable in many countries, given the costs.
It seems there’s no rule so universal that it doesn’t have some exception. That, IMO, makes law so different from math that any analogy is useless.
If it were just that the axioms of law are more complicated in the sense of being more conditional, then law would be extremely math-like. After all, theorems with lots of conditional properties (e.g., very common in certain types of algebra, a lot of dynamics, any programming language theory, etc.) are still mathematical theorems.
Law is distinguished from Math in two ways:
1) Law has more politics and isn't immune from politics. Mathematical truth, at least, is.
2) In law, the atomic propositions are always difficult to quantify and require human judgement; there is rarely an algorithm for weighing the evidence and determining guilt (or constitutionality, etc).
Actually, these laws are the most dystopian.
One concept that seems to have this design goal is strict liability: what you intended, what you believed, what elaborate conspiracies were created to deceive you, none of that matters. If you did it, you are guilty and will be punished, full stop. This is attractive because it's much harder to prove beyond a reasonable doubt that someone did something "with malice" or "intentionally" than to prove that they did it. This tends to show up around youth sexuality, probably because that's an area where social norms have changed quite a bit.
It doesn't matter if the 17.5-year-old you slept with presented a fake ID saying she was 18, took the lead in all sexual activity, etc. It doesn't matter if she shows up in court and begs the judge to let you go. People whose 18th birthday has not elapsed cannot give consent, full stop. Sex without consent is rape, rapists are bad people and should be made to suffer, so you're going to prison and then on to the sex offender registry. Your judge, and the judges you appeal to, all think this is ridiculous, but their hands are tied because the law was written like a computer program that failed to consider edge cases. (Literally edge cases - those that fall near numerical boundaries. Some states have patched their legal systems to allow consent between partners who are close in age but under the normal age of consent. Some have, but only for heterosexual couples. Some still haven't. My state actually tried and convicted two teenagers as adults for raping each other at the same time.)
Same with child porn. Child porn laws were created a time when taking and distributing a picture could only be part of a commercial publishing operation. Anyone who creates or possesses an image of a nude child is guilty of a child pornography offense. Seems reasonable. Now every teenager has an internet-connected camera in their process, and we found an edge case we forgot: the child pornographer is the child him/herself and the consumer is her long-term boyfriend, also underage. Still just as illegal and the same punishment is required. You would hope prosecutors would turn a blind eye, but "the law is the law."
These rather salacious examples are the most high-profile, but I'm sure the same problems happens in more mundane areas of law as well.
At some point you have to trust judges and you have to empower bureaucrats to help people get out of obviously ridiculous situations. Laws are much more difficult to change than computer programs; there needs to be a reasonable amount of discretion for a manual override until the law can be fixed.
From an OO point of view, the real numbers inherit almost every useful trait: they're a field, they have a topology, they have a measure. Studying the parent classes, so to speak, gives you abstract algebra, topology, and analysis, respectively.
Once you get the basics of each, you can study how they interact. Then, once that stuff is clear, they can be recombined in beautiful ways to give you new objects to study.
I came here to say the same thing. I went through a lesser known engineering discipline, "Mathematics and Enigneering" [0] and found that the type of thinking one learns doing pure math proofs has served me well in my eventual career in aerospace systems engineering. I find that the thought process in considering a proof as a high level whole/black box or being able to drill down to the finest detail while still keeping the big picture in mind has translated quite well to my day to day traversal up and down the abstraction ladder at work.
[0] http://www.mast.queensu.ca/meng/undergrad/info.php
But when I look at the implementation in code it's so obvious what's going on.
I can't fathom how someone who cannot understand the math formula can understand the code.
Here's the Hokusai paper: http://www.auai.org/uai2012/papers/231.pdf
And here's an implementation: https://github.com/dgryski/hokusai
For me to understand the paper, I had to go through the code to piece out the Math jargon, even though the Math behind it is really quite simple. Another way of saying this is, "I'm dumb," sure. Not gonna argue with anyone there.
Though I still think it's curious why it's easier for me to understand a concept through code than it is through Math. It's sort of reminiscent of when you first learned Algebra, your teacher would tell you to replace the variable with an easy number and work through it to understand the mechanics of equations.
I think code is an example of that - literally working through the mechanics of algorithms to understand what they actually do and how they work.
Interesting. I'll have to check it out. Thanks!
I think it is important to remember this, because mathematics, like a computer, "fights back." You cannot simply dream up whatever structure you want and have it mean what you want and behave how you want. See Godel's incompleteness theorems. No matter what you are doing, your mathematical constructs (including your implicit Turing Machines in your computer programs) must obey certain underlying constraints that are completely mind-independent. These constraints are what mathematicians study, albeit through a glass, darkly.
Regardless of ontological issues with the post, I like that it emphasizes the designed nature of our mathematical tools. The space of possible tools is so large that there is near-limitless room for human creativity and design in mathematical research. It is a shame that most mathematics classes don't really get that across.
edit: fixed misgendering, sorry, that was sexist.
There are knowledgeable people who do not believe that mathematics is independent of our minds. It's not too far fetched of an idea. While I do not personally agree with this, I won't downplay such beliefs.
What makes you say this? Isn't this an open philosophical question? What makes you say that mathematical objects exist independent of our minds? I can dream up a set of axioms of my own and do maths from there, so I don't think mathematics necessarily exists in some Platonic ideal dimension independent of our minds.
It's actually a she =)
Anyway, I do agree with you (and the author) that mathematics has the potential of being a superb pedagogical vehicle in teaching design thinking.
While its almost certainly true that the content of mathematics is mind independent, it is far from obvious that these objects are "real things".The real meat of the issue is how exactly the mind-independence is cashed out. Different ideas paint a vastly different picture of mathematics and even the universe. For example platonism vs. nominalism. Lets not be so quick to put forward as an obvious truth the critical issue in question.
The real numbers seem to be a perfect example: if you work in physics at scales where quantization doesn't noticeably apply, the only way to calculate correct predictions is really to use real numbers and continuous (mostly Euclidean) spaces. But that doesn't mean physical objects are ontological shadows of our mathematical abstractions, as Plato's Allegory of the Cave portrayed it. Quite the reverse: when you get down to a sufficiently small, fundamental level, objects, space, and time stop being continuous and correct experimental predictions only come from using discrete formalisms.
You can then proceed to ask, which one is Platonically real, the continuous mathematical spaces or the discrete physical ones? But I think the answer there might be, "Who says anything is Platonically real? The map is not the territory, so shut up and calculate."
Maybe, but its not obvious. The fact that the same generalizations are multiply realizable in different processes/structures certainly says something interesting. The consequences of this multiple realizability hasn't been fully investigated.
Your response seems to be arguing against my post which was mainly about mind-independence, by arguing against platonism. I don't see that mind-independence necessarily implies platonism. In fact, I find all forms of platonism extremely distasteful.
>The map is not the territory, so shut up and calculate.
Right, but this in fact goes to the heart of the question of the philosophy of mathematics. When someone says that mathematical objects are mind-independent, they are not talking about the notation itself (the map), but rather the content of the notations (the territory), i.e. the structure revealed through the notation. It should be pretty obvious that there are many interesting questions about the mind-independent structure of the territory. "Shut up and calculate" isn't an answer to this question, but rather the attitude that the answer simply doesn't matter. For many fields the answer doesn't matter, but the question is worth asking nonetheless.
True, it is our observation and our model which are similar, so I suppose the philosophical question then is up to what point we can trust our observations. And if we trust our observations, I would conclude that the similarity of our observations and math means that the real world can at least exhibit 'maths', which means our minds are not the only place where math can exist.
The smartphone I'm typing this on leads me to conclude that lots of our observations are highly trustworthy :)
Our math sense could even conflict with our other useful facilities (as is the case with how easily fooled humans are when it comes to statistics).
That is not at all what the Incompleteness Theorems actually say. They say literally nothing whatsoever about what sorts of structures you can implement inside a given foundational theory, except that there will always be more, because given any foundational theory, you can construct two more foundational theories as extensions (one in which the Goedel statement is unprovable, and one in which the theory believes it's inconsistent).
For example, creating new domain specific control flows with Lisp macros versus defining a Dirac delta function using limits and integrals. In programming it's easy for bugs to seep in because there are more little/subtle details and leaky abstractions. But math on the other hand feels much more abstract and clean.
Perhaps this is just because dumb silicon boxes interpret our code and humans interpret our math which gives us a much more sophisticated base language to work with.
Some mathematicians did not like the law of excluded middle, which states that for any proposition A, either A is true or A is false. So they invented intuitionistic logic, which is normal logic without the excluded middle, and started rewriting mathematical proofs in this new system. Turns out there's a lot of stuff you can prove in intuitionistic logic.
Some mathematicians did not like the axiom of choice. One of the consequences of this axiom is that every subset of the real numbers has a least element according to some ordering. Think about it, what is the least element of {1/n : n >= 1} ? Who knows! So what did they do? Some people found it so weird they either replaced it with a weaker axiom or a contradictory one.
There's even syntax arguments in mathematics! What's the derivative of a function f? is it f'(x) or df/dx ? Is multiplication represented by a dot (.) or a cross (x) or by a juxtaposition of expressions?
Sometimes we use big existing proofs in the middle of a proof to save time. And sometimes we use the big proof to prove something far simpler than the big proof. This creates a big dependency and some people dislike hate these dependencies because the reader of the new proof will have trouble understanding the proof completely. It's like dropping in some magic in the middle of the proof and saying: "if you want to understand this proof completely, go read this other 50 page article" Sound familiar? Some mathematicians hate this so much they insist on proving things from the ground up whenever possible so that the proof is as comprehensible as possible. This is the mathematical equivalent of dependency management.
An even weirder consequence of AC is the Banach-Tarski paradox [1].
Other examples of how mathematicians come up with alternative perspectives are non-Euclidean geometries that replace the parallel postulate of the common Euclidean geometry, e.g. Lobachevskian [2] and Riemannian geometry [3].
[1] https://en.wikipedia.org/wiki/Banach%E2%80%93Tarski_paradox
[2] https://en.wikipedia.org/wiki/Hyperbolic_geometry
[3] https://en.wikipedia.org/wiki/Elliptic_geometry
It's easy to find such an ordering for any countable subset -- i.e., one that set-theoretically is no bigger than the integers. For instance, we can do it for all the rational numbers by saying that we order numbers p/q (p,q integers, no common factor, q positive) by converting p/q to 2^signbit(p) 3^|p| 5^|q| or something of the kind, where signbit(x)=0 is what in C you write as (x<0), and comparing the positive integers that result.
It's much harder to see how to do it for all the real numbers. In fact, you provably can't see how, in the sense that there actually is known to be no construction that does it -- no way to say explicitly which numbers to put before which.
(This is a common pattern; cases where you need AC to do something are always ones where there is no explicit construction that does it. That kinda has to be true, because there are models of set theory in which AC is false.)
For the rational numbers, this is not difficult, since we can enumerate the rational numbers. As the ordering we could then pick "a <= b" if the index of "a" in the enumeration is less than the index of "b". The least element of any set of rational numbers is then the rational number with the least index in that set.
However, the real numbers are uncountable. Tricks like this cannot work.
----
The real culprit is the axiom of excluded middle, which confounds the notions of existence and embodiment. Under classical logic it may be proven that P = NP, even though no algorithm actually exists. This already happened for certain graph problems... (=> Graph minor theorem, moving from minor-closed graph property to finite set of excluded minors is essentially non-constructive.)
Without excluded middle, the axiom of choice is exactly as trivial as it sounds: Given a non-empty set, give me an element in that set. In order to show that a set is non-empty you need to give enough information to construct an element in that set. So the proof contains the information to validate the "axiom".
With excluded middle, the proof that a set is non-empty doesn't contain enough information to pick an element from that set. So adding both excluded middle and choice takes you into an axiomatic system whose connection with the real world is rather tenuous.
----
The article is spot on: Not only is mathematics a designed system, but the analogy between programming languages and logic is perfect in view of the Curry-Howard correspondence. Elevating Zermelo-Fraenkel set theory is like insisting that your software project has to be built using Turing machines. After all, everything else is just encoding. There is a huge design space in logics as well as in programming languages. For instance, you can do physics in the setting of synthetic differential geometry and work without preconditions and use theorems which are literally impossible in ZFC.
A soundness proof for a new logic is, by the way, the logical equivalent of building a compiler. :)
The reason is intuitively clear: in order to prove that the infinite product is non-empty, we need to produce an infinitely long vector. Well, since the individual sets are non-empty, we can just for each set choose an element and put it in the vector. But this takes infinitely many steps! and that's not allowed in mathematics. The axiom of choice is a way of collapsing infinitely many steps into 1 invocation of the axiom (so 1 step, so finitely many steps). Not too much to do with excluded middle.
But you are right, the devil is in the details, so let me spell it out precisely:
The axiom states that for every set X, there is a function
If you want to restrict yourself to first-order logic, then you have to encode the function \epsilon (e.g. as a functional relation, where relations are in turn encoded as sets of ordered pairs, which are in turn encoded with Kuratowsky's construction). Set theorists like first-order logic and this encoding overhead is the reason why it's not the standard definition, even though it's arguably what the axiom is trying to express(1,2). Apart from that the statements are (classically) equivalent:To go from the higher-order version to the cartesian product, note that the cartesian product of an I-indexed family of sets is a set of functions f from I to the union of all X_i's, such that f(i) \in X_i for all i. Let (X_i)_{i\in I} be an I-indexed family of sets, all of which are non-empty, then (i -> \epsilon(X_i)) is in the cartesian product of the X_i's, where we use \epsilon for the union of all X_i's. The reason we couldn't build that element without AC is precisely that we have no way of selecting exacly one element from each X_i, even though we know that they are non-empty.
In the other direction we can use Zermelo's well-ordering theorem to construct a well-order on X. We define \epsilon to pick out the minimum with respect to this order.
(1) This really is what the axiom of choice was meant to express. If you can read German, you can refer to Zermelo's own work:
Under point 2 in this paper, Zermelo assumes that there is such a choice function on a given set and from this he derives the well-ordering of that set.(2) Another example of the drawbacks of working with a first-order axiomatization is the axiom of regularity. The idea we want to express is that there are no infinitely descending element chains ("every set is well-founded"), but expressing this in first-order logic leads to a convoluted statement which obscures the simple idea... and is also not a correct encoding of this idea in intuitionistic logic!
Those aren't arguments. All of those are very standard things to do.
There's a Spiked Math comic with some good mathematics-engineering trash talk, though, with the mathematicians shooing away a hapless engineer with comments like "do you even know how to spell 'imaginary'?" and "why don't you go jmagine you have friends?" Again, I wouldn't describe this as an area of active debate.
(MIT Sussman, SICM book) http://mitpress.mit.edu/sites/default/files/titles/content/s...
Weirdly enough, I always struggled with advanced syntax, but I recently understood that it was a lack of focus on the abstraction. Kinda like programming languages :) But that's something you can't really understand when too young.
1. An ancestor of Djinn is automated theorem proving. Why can't machines prove math theorems for us? This quest goes back to the dawn of computing science.
2. A more recent development is the Curry-Howard Correspondence. Programming in a (typed) FP language is like playing tetris. Solving symbolic logic problems [1] is also like playing tetris. Djinn exposes the connection in a REPL you can play with. And see how the computer plays tetris for you!
3. Don't want to install Djinn? No problem, just hop over to the Haskell IRC [2]. Lambdabot has a working Djinn plugin.
[0] https://hackage.haskell.org/package/djinn
[1] https://www.coursera.org/course/intrologic
[2] https://wiki.haskell.org/IRC_channel
I have a keen interest in neural networks and it requires good foundation of Math.