5 ms·

I'm sure AI could contribute to this, but this is already a well-developed field of mathematics, and most of the consequences of additional axioms have been wor

I'm sure AI could contribute to this, but this is already a well-developed field of mathematics, and most of the consequences of additional axioms have been worked out. (The most productive hypothesis has been what's called "projective determinacy", if you're curious.) Mathematicians have also gone in the opposite direction, and tried to work out what are the weakest foundations where different results hold. This is called "reverse mathematics".

kdavis 25d ago
What name does this "well-developed field of mathematics" go by? (I just want to get a taste of what the field is like.) I also thought that there are an infinite set of possible extra axioms, e.g. axiomize any statement that's true but not provably so via Gödel's First Incompleteness Theorem, though maybe the vast majority of such axioms are "uninteresting".
- QuesnayJr 25d ago
  "Descriptive set theory" is a good starting point, though it's the bulk of what set theorists in general do. It's true that there's an infinite possible set of axioms. It does seem that the types of axioms that have consequences that humans are interested in fall into simple families. For example, many seemingly unrelated questions are settled by assume the existence of very large sets (larger than can normally constructed in set theory).
kdavis 25d ago
Looking a bit more into this, it doesn't seem your claim "most of the consequences of additional axioms have been worked out" holds up. Yes, metamathematics is well-developed, but I don't think that most of the consequences of any particular additional set of axioms have been worked out. Each such new set requires re-deriving all of this alternate mathematics from scratch. This is a lot of work! So I think my original claim---mathematicians select interesting axioms and AI figures out their implications---still seems a possible way forward. PS: I'd guess descriptive set theory under determinacy is the one place where projective determinacy, as you stated, pays off.
- QuesnayJr 25d ago
  I don't see how you came to that conclusion, since I'm telling you the actual state of play. There's a big literature on what results require the Axiom of Choice, for example. (The book Handbook of Analysis and Its Foundations covers this thoroughly.) There are many results on what follows from the Continuum Hypothesis or other cardinal arithmetic axioms. There is a big literature on what follows from assuming the existence of large cardinals. There's a separate literature on adding "forcing axioms", like Martin's maximum. There are hundreds of papers on open questions that are settled by adding additional axioms to ZFC, and to identifying the weakest axioms to add to settle various open questions. In another direction, there's even a literature on what happens when you allow sets to contain themselves as members, like Aczel's Anti-Foundation Axiom. There's literatures on purely constructive versions of set theory, where everything has to be computable. Like I mentioned before (reverse mathematics), there's work on what happens when you adopt much weaker axiom sets, like second-order arithmetic but weak choice principles such as taking Kruskal's tree theorem as an axiom. So while AI would accelerate this work, the existing body of work on alternate axioms is tremendous. A surprisingly large amount of it translates between systems, and there are precise tools to measure how weak or strong a system is, relative to its competitors.
  - kdavis 25d ago
    While the existing body of work on alternate axioms is tremendous, it's finite. The set of possible axiom systems is infinite. Does current the current body of work cover all consequences of all possible axiom systems?

kdavis 25d ago

What name does this "well-developed field of mathematics" go by? (I just want to get a taste of what the field is like.) I also thought that there are an infinite set of possible extra axioms, e.g. axiomize any statement that's true but not provably so via Gödel's First Incompleteness Theorem, though maybe the vast majority of such axioms are "uninteresting".

QuesnayJr 25d ago
"Descriptive set theory" is a good starting point, though it's the bulk of what set theorists in general do. It's true that there's an infinite possible set of axioms. It does seem that the types of axioms that have consequences that humans are interested in fall into simple families. For example, many seemingly unrelated questions are settled by assume the existence of very large sets (larger than can normally constructed in set theory).

kdavis 25d ago

Looking a bit more into this, it doesn't seem your claim "most of the consequences of additional axioms have been worked out" holds up. Yes, metamathematics is well-developed, but I don't think that most of the consequences of any particular additional set of axioms have been worked out. Each such new set requires re-deriving all of this alternate mathematics from scratch. This is a lot of work! So I think my original claim---mathematicians select interesting axioms and AI figures out their implications---still seems a possible way forward. PS: I'd guess descriptive set theory under determinacy is the one place where projective determinacy, as you stated, pays off.

QuesnayJr 25d ago
I don't see how you came to that conclusion, since I'm telling you the actual state of play. There's a big literature on what results require the Axiom of Choice, for example. (The book Handbook of Analysis and Its Foundations covers this thoroughly.) There are many results on what follows from the Continuum Hypothesis or other cardinal arithmetic axioms. There is a big literature on what follows from assuming the existence of large cardinals. There's a separate literature on adding "forcing axioms", like Martin's maximum. There are hundreds of papers on open questions that are settled by adding additional axioms to ZFC, and to identifying the weakest axioms to add to settle various open questions. In another direction, there's even a literature on what happens when you allow sets to contain themselves as members, like Aczel's Anti-Foundation Axiom. There's literatures on purely constructive versions of set theory, where everything has to be computable. Like I mentioned before (reverse mathematics), there's work on what happens when you adopt much weaker axiom sets, like second-order arithmetic but weak choice principles such as taking Kruskal's tree theorem as an axiom. So while AI would accelerate this work, the existing body of work on alternate axioms is tremendous. A surprisingly large amount of it translates between systems, and there are precise tools to measure how weak or strong a system is, relative to its competitors.
- kdavis 25d ago
  While the existing body of work on alternate axioms is tremendous, it's finite. The set of possible axiom systems is infinite. Does current the current body of work cover all consequences of all possible axiom systems?