En general, los nuevos axiomas ahora se incluyen si usted puede demostrar su independencia de las fundaciones y necesita el axioma de probar otras declaraciones interesantes. Por ejemplo, cuando Cohen demostró la independencia de la hipótesis continua de ZFC, que deja de ser una conjetura y en su lugar (y es la negación) se convirtió en un axioma en el libro de recetas para ciertos fuerte teorías.
Hay una serie de declaraciones que han demostrado ser independiente de ZFC, muchos incompatibles el uno con el otro. Estos son mezclados y emparejados con las bases en función de las necesidades de la matemática en el tiempo, a menudo para probar las cosas bien en el extraño mundo de los grandes cardenales y otros monstruos.
De vez en cuando nos ir a otro lado, sin embargo, y de intentar hacer el trabajo tratando de demostrar de lo que son los axiomas necesarios para demostrar que un enunciado, y luego trabajamos en el mundo de la inversa de matemáticas, demostrando que los axiomas a partir de los teoremas; Por ejemplo, determinar el mínimo requisito de axiomas para demostrar algo acerca de los números primos de los números naturales encadenamiento hacia abajo para que los axiomas de ZFC son necesarios. Aquí se puede decidir que el sistema ortodoxo no es granular suficiente y, a continuación, reemplace las bases para algo más granular, o tal vez algo que es más adecuado para el mecanizado de razonamiento como NGB, con sus finito axiomization.
A continuación, vamos a cambiar los fundamentos mismos. A menudo utilizamos ZFC como un punto de partida, debido a sus familiares punto de partida que es aproximadamente equivalente a la de otras fundaciones, y tiene una fuerte tendencia de reconocimiento de nombre, pero nos interruptor de fundaciones de todo cuando queremos algo de otras propiedades; Finito axiomization, granular debilidad, o tal vez incluso una representación más compacta, o extensibilidad con objetos como las clases o la semántica de otros sistemas formales, como la lógica de orden superior.
Para obtener más ejemplos específicos que son menos fundamentales, en otras ocasiones deseamos un muy débil sistema de axiomas que se decidable, tales como Pressburger aritmética, pero decidimos que queremos más expresable declaraciones lo que hacen conservador extensiones que preservar su satisfiability. Aquí es donde muchos conste que el modulo de la teoría de los axiomas vienen, conveniente, ya que podemos utilizar SAT solvers lugar de primer orden teorema de provers. En otras ocasiones queremos debilitar un indecidible teoría como la aritmética de Peano para hacer finitely axiomizable, y ahora tenemos Robinson aritmética.
En cualquier caso, los nuevos axiomas se agregan cuando está demostrado independiente de las bases o los fundamentos mismos no son deseables para la tarea a mano.
http://en.wikipedia.org/wiki/List_of_statements_undecidable_in_ZFC
http://en.wikipedia.org/wiki/Reverse_mathematics
