Live data from Hacker News

Parallels Between Math and Software Engineering

beta.oreilly.com

81–90 of 97 posts

Re: Parallels Between Math and Software Engineering

#81

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…

First time I heard someone talking about mathematics syntax:

(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.

Re: Parallels Between Math and Software Engineering

#83

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…

If you just reverse the typical ordering, then the least element of {1/n : n >= 1} is 1, so this doesn't seem all that strange to me.

That's too trivial, so I doubt that's what the theorem is about.

Re: Parallels Between Math and Software Engineering

#84
post #83

Earlier quoted context omitted.

If you just reverse the typical ordering, then the least element of {1/n : n >= 1} is 1, so this doesn't seem all that strange to me.

That's too trivial, so I doubt that's what the theorem is about.

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 (xIt'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.)

Re: Parallels Between Math and Software Engineering

#85

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…

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?

Re: Parallels Between Math and Software Engineering

#86

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…

If you just reverse the typical ordering, then the least element of {1/n : n >= 1} is 1, so this doesn't seem all that strange to me.

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 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. :)

Re: Parallels Between Math and Software Engineering

#87
post #86

Earlier quoted context omitted.

If you just reverse the typical ordering, then the least element of {1/n : n >= 1} is 1, so this doesn't seem all that strange to me.

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 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 clas…

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.

Re: Parallels Between Math and Software Engineering

#88
post #73

Earlier quoted context omitted.

>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 mathemati…

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. An…

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).

Re: Parallels Between Math and Software Engineering

#89
post #86

Earlier quoted context omitted.

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 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 clas…

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…

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!

Re: Parallels Between Math and Software Engineering

#90
post #36

Earlier quoted context omitted.

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 fou…

> 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 o…

This is a silly argument.

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.

Post reply on HN