Hacker News Reader

Comment by Someone | Hacker News Reader

If builders of a huge castle place some stones incorrectly, does it collapse completely?

No. Such errors may be discovered soon and taken down, or stand for decades, sometimes with lots of stuff built on top of it, and sometime parts will collapse, but the overall structure of the castle is sound, and, sooner or later, errors will be corrected.

And of course, sometimes, somebody decides to start building an entire new wing to the castle using new rules, as, for example, happened when non-Euclidean geometry was discovered/invented.

View on HN

On the analogy of castles, I asked a professor whether Godel’s Incompleteness theorems affects their work. She told me Mathematics is this great castle, where in one quadrant you have the number theorist, in another the topologists. Every decade or century, the logicians would come running up from the basement with results confronting the foundations of math, but everyone else continued with their routine

Perhaps the point is that the basement of a castle is also called a dungeon.

Yeah, swapping out currently dominant logic with another one would redo the whole castle, like when a castle built in Gothic architecture is rebuilt into Baroque with some parts left intact. However, mainstream is so dominant and "better logics" either don't have sufficient manpower, are more complicated, are weaker or impractical, so that they never develop unless they solve something extraordinary quickly.

My memory from the logic classes I've taken was that after Godel, mathematicians largely abandoned Hilbert's, Russell's and Whitehead's ambition of founding mathematics on logic, and largely grew disinterested in foundational issues as a whole.

As such, mathematics doesn't have a solid foundation, and most contemporary mathematicians seem to be ok with that, as long as it works and they can get interesting results.

I agree with the rest of what you wrote, but doesn't have a solid foundation seems a bit far. Mathematicians hand-wave that their proofs can be reduced to ZFC set theory and despite reasonable wariness about that hand-waving, it has so far been borne out by all efforts at deeper inspection all the way up to full machine-checked formalization.

Although I am starting to get out of my depth, my impression was that ZFC itself is (per Godel's results) inconsistent or incomplete. Here is some research to this effect:

If this is indeed the case (as it seems to my unprofessional first glance to be) then mathematics does not in fact have a solid foundation, despite its appeal to ZFC.

I'd love to hear a professional logician weigh in on this, if there are any on here.

[1] - https://www.researchgate.net/profile/Costas_Drossos/post/Is_...

[2] - https://arxiv.org/abs/1203.0494

The short answer is "incompleteness is not a big deal" and the slightly longer answer is "if it's inconsistent, the proof of inconsistency is devilishly hard to find." If it does exist, the inconsistent part seems likely to be sufficiently esoteric that it could be "built around."

ZFC is incomplete. There are many celebrated results that are independent of ZFC (continuum hypothesis, large cardinals (a lot aren't even known to be consistent with ZFC), Suslin's Hypothesis, etc. However, by Godel we know this is true for any reasonable foundation of mathematics (i.e. anything capable of expressing the usual version of arithmetic). So it is not something that particularly troubles either logicians or other mathematicians.

Godel's results also show that we cannot use ZFC to prove that ZFC is consistent. However, it is strongly suspected that ZFC is consistent.

In practice, very few of the results independent of ZFC affect day to day mathematical work unless you're a logician or set theorist (which honestly start to blend into each other).

Oh I forgot to add. The inability to prove its own consistency is also something any reasonable foundation will have.

Logicians are often unsatisfied with ZFC as a foundation for other reasons. These mainly amount to the clunkiness of set theory encodings. They have no notion of types so you can pose nonsense questions such as "is the number 2 a subset of the addition function?" There's no formal way of dealing with objects "larger" than sets (e.g. the collection of all sets) other than as syntactic formulas. They obscure relationships between different mathematical fields by resulting in completely different encodings for analogous structures.

This is why logicians will sometimes talk your ear off about how category theory is so much better as a foundational theory than set theory.

Again though, for the working mathematician, these flaws in ZFC as a foundation rarely matter.

I have a general algebra textbook that uses category theory as a foundation, and although I haven't gotten very far into it, my impression is that either category theory or ZFC can be used to derive the other one. As a result, it doesn't matter a whole lot where you start since you get both eventually anyway. If category theory adds tools that make it easier to prove theorems, that's great and useful, but no one really cares if it was foundational or derived.

This is one main reason why the larger mathematical community does not closely follow these foundational discussions (there are foundations that are strict extensions of ZFC but these extensions are usually conservative).

The usual response is that it would be nice if the formal foundations of mathematics corresponded more closely to the informal intuitions of mathematicians, which is arguably not true of set theoretic foundations and perhaps is more true of category theory. Whether or not you agree about the correspondence or whether even if you agree you find it at all convincing is up to you.

TBH, the construction of Riemann surfaces from the natural numbers is pretty well understood by the average UK undergraduate. (Natural->Integer->Rational->Real->Complex->Foundations of Reimann Surfaces). The expression of the rules of natural numbers in ZFC is fully understood by far fewer, but that’s mostly because it’s tedious.

AFAICT mathematical logic has always felt like a curious side show in the greater math community. If you were to ask professional mathematicians to list off all the axioms of ZFC they'd probably shrug if they didn't get all of them. They probably wouldn't know about the more exotic parts of set theory such as large cardinals nor would they would probably know too much about alternate foundations of mathematics. They might not be familiar at all with the specifics of model theory.

The logical foundations of mathematics have always had a much smaller impact on the day to day lives of mathematicians than their foundational nature might suggest.

I wonder what fraction of web programmers understand transistor physics?

Well maybe not quite that extreme. It's more analogous to the fact that most professional programmers do not fully understand the programming language they use (nor honestly do they need to for the most part).

Nonetheless, it's perhaps surprising for a beginning student of pure mathematics when all they can see is the sky-high demand for rigor that "professional" pure mathematics is seemingly content to hand-wave its foundations. (For the most part this hand-waving is the postrigorous stage described by Terence Tao https://terrytao.wordpress.com/career-advice/theres-more-to-... rather than the pre-rigorous hand-waving of the student).

> what fraction of web programmers understand transistor physics?

I'm not an engineer, but I imagine that even most professional electrical/electronic engineers do not understand transistor physics in full details. In engineering, a transistor is essentially treated as a blackbox, and its behavior is described and approximated by various small-signal and large-signal models (i.e. treated as a lumped component), with their parameters characterized empirically by vendors through experiments. How exactly things work at atomic or quantum level is essentially for a transistor to work, yet, a subject of study unrelated to electrical engineering.

On the other hand, I imagine there is no shortage of EEs who have studied a physics major, or EEs with a background of semiconductor physics - they can understand transistor physics really well.

So we can say the relation between EE and transistor physics sounds a lot similar to mathematicians and logicians, it's a good analogy.

That's because formal logic is a (relatively) recent attempt to formalize the intuitions behind the math that people were already doing. Doing mathematics doesn't really depend on foundational logic in the same way that, e.g., a web app depends on transistor physics.

As somebody once said, if we ever found a contradiction in the ZFC axioms, we wouldn't throw out math, we'd just throw out ZFC.

> Doing mathematics doesn't really depend on foundational logic in the same way that, e.g., a web app depends on transistor physics.

Web apps don't depend on transistor physics at all, though. An important consequence of Turing universality is that computer science is not a subfield of electrical engineering.

Also, mathematics underwent very dramatic transformations during the late 1800s and early 1900s alongside the early development of formal logic and set theory. To say that logicians were merely "formalizing the intuitions behind the math that people were already doing" strikes me as misguided at best. The mathematics that rose to prominence in that era was very different from what preceded it, often controversially so.

>if we ever found a contradiction in the ZFC axioms, we wouldn't throw out math, we'd just throw out ZFC.

It's like saying: if we ever found a contradiction in the base case of a mathematical induction, we wouldn't throw out mathematical induction, we'd just throw out the base case. The indudction step remains sound.

https://en.wikipedia.org/wiki/Mathematical_induction

My impression is that today we know that there can be no single foundation, which means that there is no way to undermine all areas at once.

The analogy I’d make is to bugs in software. Most software has bugs, but they’re only triggered in specific circumstances. Stay away from those cases and you’re usually fine. If you happen to hit a new bug, you might lose some data, but it’s not going to render the entire application useless.

So a proof might claim to prove a theorem about a whole class of numbers or other mathematical objects. But if there is bug in one of its lemmas it would mean its results are true of only a subset of the mathematical objects claimed. That would be like getting an error on specific inputs.

The proof then remains a valid proof of something although not exactly a proof of everything its authors claim it to be a proof of.

An erroneous proof is also usually useful because it is not clearly wrong in most cases since nobody has come up with counter-examples so far that would prove the proof incorrect, yet.

I don't think it's necessarily like that. The error could make the theorem wrong in all cases.

I think it's more that the mathematician has a top-down way of reasoning, where they can see things like "I want to get from New York City to Los Angeles, so I have to board the bus, take a flight, and then take the bus from the airport at LA". There are certain parts where you basically know that a proof will be possible, because it seems true, like "I can get to LA's airport with public transit", so usually a specific hiccup, like a bus being delayed, won't prevent you from getting there.

Right, it's possible to get to LA's airport with public transit, but the amount of time it takes cannot be upper bounded using currently known techniques.

Well, this is "hacker news", and I imagine there are quite a few people around who have plenty of first hand experience with programming but not so much mathematical proofs. And there are a lot of examples of "a few stones placed incorrectly" taking down a huge edifice when it comes to software.[1]

So it may be true that math doesn't work like that, but I don't think it's obvious why. Many people have suggested that software would be better if habitually proved correct, but then, why is it not 100% necessary that proofs be perfect? Why should proofs be more resilient than software?

[1]https://gcn.com/articles/1998/07/13/software-glitches-leave-...

Reply on news.ycombinator.com