How has mathematics gotten so abstract?

And a lot of what goes on in foundations of mathematics could be described as "testing the axioms", i.e. identifying which theorems require which axioms, what are the consequences of removing, adding, or modifying axioms, etc.

In practice when proofs of research mathematics are checked, they go out to like 4 grad students. This isn't a very glamorous job for those grad students. If they agree then it's considered correct...

But note this is just the bleeding edge stuff. The basic stuff is checked and reproven by every math undergrad that learns math. Literally millions of people have checked all the proofs. As long as something is taught in university somewhere, all the people who are learning it (well, all the ones who do it well) are proving / checking the theory.

Anyway, when the scientific community accepts a bad proof what effectively happens is that we've just added an extra axiom.

Like when you deliberately add new axioms, there are 3 cases

- Axiom is redundant: it can be proven from the other axioms. (this is ... relatively fine? we tricked ourselves into believing something that is true is true, the reason is just bad.)

This can get discovered when people try to adapt the bad proof to prove other things and fail.

Also people find and publish and "more interesting", "different" proofs for old theorems all the time. Now you have redundancy.

- Axiom contradicts other axioms: We can now prove p and not p.

I wonder if this has ever happened? I.e. people proving contradictions, leading them to discover that a generally accepted theorem's proof is incorrect. It must have happened a few times in history, no?

o/c maybe the reason this hasn't happened is that the whole logical foundation of mathematics is new, dating back to the hilbert program (1920s).

There are well known instances of "proofs" being overturned before that, but they're not strictly logically proofs in the hilbert-program sense, just arguments. (Of course they contain most of the work and ideas that would go into a correct proof, and if you understand them you can do a modern proof)

e.g. https://mathoverflow.net/a/35558

Cauchys proof that, if a sequence of continuous functions converges [pointwise] to a function, the limit function is also continuous (cauchys proof only holds for uniform convergence, not pointwise convergence - but people didnt really know the difference at the time)

- Axiom is independent of other axioms: You can't prove or disprove the theorem.

English doesn't have a "I'm just hypothesizing all of this" voice, if it did exist this post should be in it. I didn't do enough research to answer your question. Some of the above may be wrong, e.g. the part about the 4 grad students. One should probably look for historical examples.

If I'm following you, then most "mathematical" CS is based on constructivist foundations? E.g. while a halting problem Oracle might "exist" in the mathematical sense, it's not considered to "exist" for most purposes of deciding complexity classes, etc.

> The real question isn't whether this oracle exists. It is what you want the word "exists" to mean.

I was going to say the same thing. I'm not sure what "exists" means in some of these discussions.

As for what exists means, here are the three basic philosophies of mathematics.

The oldest is Platonism. It is the belief that mathematics is real, and we are trying to discover the right way to do it. Ours is not to understand how it is to exist, it is to try to figure out what actually exists. Kurt Gödel is a good example of someone who argued for this. See https://journals.openedition.org/philosophiascientiae/661 for a more detailed exploration of his views, and how they changed over time. (His Platonism does seem to have softened over time.)

Historically this philosophy is rooted in Plato's theory of Forms. Where our real world reflects an ideal world created by a divine Demiurge. With the rise of Christianity, that divine being is obviously God. This fit well with the common idea during the Scientific Revolution that the study of science and mathematics was an exploration of the mind of God.

Formalism dates back to David Hilbert. In Hilbert's own description, it reduces mathematics to formal symbol manipulation according to formal rules. It's a game to figure out what the consequences are of the axioms that were chosen. As for existence, "If the arbitrarily posited axioms together with all their consequences do not contradict each other, then they are true and the things defined by these axioms exist. For me, this is the criterion of truth and existence." See page 39 of https://philsci-archive.pitt.edu/17600/1/bde.pdf for a reference.

In other words if we make up any set of axioms and they don't contradict each other, the things that those axioms define have mathematical existence. Whether or not we can individually describe those things, or learn about them.

Over on the constructivist side of the fence, there are a wide range of possible views. But they share the idea that mathematical things can only exist when there is a way to construct them. But that begs the question.

Finitism only accepts the existence of finite things. In an extreme form, even the set of natural numbers doesn't exist. Only individual natural numbers. Goodstein of the Goodstein sequence is a good example of a finitist.

Intuitionism has the view that mathematics only exists in the minds of men. Anything not accessible to the minds of men, doesn't exist. The best known adherent of this philosophy is Brouwer.

My sympathies generally lie with the Russian school, founded by Markov. (Yes, the Markov that Markov chains are named after.) It roots mathematics in computability.

Erret Bishop is an example of a more pragmatic version of constructivism. Rather than focus on the philosophical claims, he pragmatically focuses on what can be demonstrated constructively. https://www.amazon.com/Foundations-Constructive-Analysis-Err... is his best known work.