When the mathematical community consider the inclusion of a new axiom?.

Solution 1:

In general, new axioms now are included if you can prove their independence from foundations and you need the axiom to prove other interesting statements. For instance, when Cohen proved the independence of the continuum hypothesis from ZFC, it ceased to be a conjecture and instead it (and it's negation) became an axiom in the recipe book for certain strong theories.

There are a number of statements that have been proved independent of ZFC, many inconsistent with each other. These are mixed and matched with the foundations depending on the needs of the mathematician at the time, often to prove things well into the strange world of large cardinals and other monsters.

Occasionally we go the other way however and attempt to do work trying to prove what axioms are necessary to prove a statement, and then we work in the world of reverse mathematics, proving the axioms from the theorems; For instance determining the minimum requisite axioms to prove something about primes in the natural numbers chaining down to which axioms in ZFC are required. Here we may decide that the orthodox system isn't granular enough and then replace the foundations for something more granular, or perhaps something that is more suitable for mechanized reasoning such as NGB, with its finite axiomization.

Then we change the foundations themselves. We often use ZFC as a starting point because its a familiar starting ground that is roughly equivalent to other foundations, and it has a strong trending name recognition, but we switch foundations around when we want some other properties; Finite axiomization, granular weakness, or perhaps even a more compact representation, or extensibility with objects like classes or semantics of other formal systems like higher order logic.

For more specific examples that are less foundational, at other times we want a very weak axiom system that is decidable, such as Pressburger arithmetic, but we decide that we want more expressible statements so we make conservative extensions that preserve its satisfiability. This is where many satisfiable modulo theory axioms come from, convenient because we can use SAT solvers instead of first order theorem provers. At other times we want to weaken an undecidable theory like Peano arithmetic to make it finitely axiomizable, and now we have Robinson arithmetic.

In any case new axioms are added when they're demonstrated independent from the foundations or the foundations themselves are undesirable for the task at hand.

http://en.wikipedia.org/wiki/List_of_statements_undecidable_in_ZFC http://en.wikipedia.org/wiki/Reverse_mathematics

Solution 2:

Not the same question but maybe relevant: Believing the Axioms by Penelope Maddy.

http://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms1.pdf http://www.cs.umd.edu/~gasarch/BLOGPAPERS/belaxioms2.pdf