The standard Zermelo-Fraenkel axioms have lasted a century with only minor modifications—none of which altered what was provable—and there weren’t many false starts before that. There is argument over whether to include the axiom of choice, but as mentioned the formal methods of program construction naturally use constructivist mathematics, which doesn’t use the axiom of choice anyhow.
Is there a formal method for deciding whether or not to include the axiom of choice? As I understand it three of the ZF axioms are independent of the rest, and all are independent of choice. How would AGI choose which independent axioms should be accepted? AGI could be built to only ever accept a fixed list of axioms but that would make it inflexible if further discoveries offer evidence for choice being useful for example.
This blatantly contradicts the history of axiomatic mathematics, which is only about two centuries old and which has standardized on the ZF axioms for half of that. That you claim this calls into question your knowledge about mathematics generally.
You are correct, I don’t have formal mathematical training beyond college and I pursue formal mathematics out of personal interest, so I welcome corrections. As I understand it geometry was axiomatic for much longer, and the discovery of non-Euclidean geometries required separating the original axioms for different topologies. Is there a way to formally decide now whether or not a similar adjustment may be required for the axioms of ZF(C)? The problem, as I see it, is that formal mathematics is just string manipulation and the choice of which allowed manipulations are useful is dependent on how the world really is. ZF is useful because its language maps very well onto the real world, but as an example unifying general relativity and quantum mechanics has been difficult. Unless it’s formally decidable whether ZF is sufficient for a unified theory it seems to me that some method for an AGI to change its accepted axioms based on probabilistic evidence is required, as well as avoid accepting useless or inconsistent independent axioms.
The axiom of choice applies exclusively to infinite sets, and the finite restriction is a consequence of ZF without AC. Since we cannot actually construct infinite sets, infinitesimals, or even irrational numbers, the consequences of ZFC over and above ZF in the real world are negligible at most, and almost certainly nonexistent.
ZF is useful because its language maps very well onto the real world, but as an example unifying general relativity and quantum mechanics has been difficult.
These are not related statements. There are a lot of ways to choose axioms, but I’m not aware of any of them having any consequences in regimes applicable to physics. Any choice of axioms meant to describe the world has to support some basic conclusions like the validity of arithmetic, and that puts great restrictions on what the axioms are, and what they could possibly say about a physical theory.
As I understand it geometry was axiomatic for much longer, and the discovery of non-Euclidean geometries required separating the original axioms for different topologies.
Geometry was nominally axiomatic for many centuries, but not rigorously axiomatic until the study and development of non-Euclidean geometry, which was the beginning of the rigorous axiomatization of mathematics. Prior to that, statements were frequently taken as axioms on purely intuitionist grounds (in many subfields); it took the demonstration that Euclid’s fifth axiom (the parallel postulate) was unnecessary to make mathematicians actually check their assumptions and establish sets of axioms which were consistent.
Is there a formal method for deciding whether or not to include the axiom of choice? As I understand it three of the ZF axioms are independent of the rest, and all are independent of choice. How would AGI choose which independent axioms should be accepted? AGI could be built to only ever accept a fixed list of axioms but that would make it inflexible if further discoveries offer evidence for choice being useful for example.
You are correct, I don’t have formal mathematical training beyond college and I pursue formal mathematics out of personal interest, so I welcome corrections. As I understand it geometry was axiomatic for much longer, and the discovery of non-Euclidean geometries required separating the original axioms for different topologies. Is there a way to formally decide now whether or not a similar adjustment may be required for the axioms of ZF(C)? The problem, as I see it, is that formal mathematics is just string manipulation and the choice of which allowed manipulations are useful is dependent on how the world really is. ZF is useful because its language maps very well onto the real world, but as an example unifying general relativity and quantum mechanics has been difficult. Unless it’s formally decidable whether ZF is sufficient for a unified theory it seems to me that some method for an AGI to change its accepted axioms based on probabilistic evidence is required, as well as avoid accepting useless or inconsistent independent axioms.
The axiom of choice applies exclusively to infinite sets, and the finite restriction is a consequence of ZF without AC. Since we cannot actually construct infinite sets, infinitesimals, or even irrational numbers, the consequences of ZFC over and above ZF in the real world are negligible at most, and almost certainly nonexistent.
These are not related statements. There are a lot of ways to choose axioms, but I’m not aware of any of them having any consequences in regimes applicable to physics. Any choice of axioms meant to describe the world has to support some basic conclusions like the validity of arithmetic, and that puts great restrictions on what the axioms are, and what they could possibly say about a physical theory.
Geometry was nominally axiomatic for many centuries, but not rigorously axiomatic until the study and development of non-Euclidean geometry, which was the beginning of the rigorous axiomatization of mathematics. Prior to that, statements were frequently taken as axioms on purely intuitionist grounds (in many subfields); it took the demonstration that Euclid’s fifth axiom (the parallel postulate) was unnecessary to make mathematicians actually check their assumptions and establish sets of axioms which were consistent.