MathOverflow will be down for maintenance for approximately 3 hours, starting Monday evening (06/24/2013) at approximately 9:00 PM Eastern time (UTC-4).
show/hide this revision's text 3 added 4 characters in body

By Gödel's incompleteness theorem, there can't be any such axiom in a first-order, recursively enumerable theory.

You can axiomatize $\mathbb N$ by adding an infinitary rule of inference, the Hilbert $\omega$-rule:

$$P(0)\wedge P(1) \wedge P(2) \wedge \cdots \over \forall n P(n)$$

to PA for each arithmetic predicate P. This says, if predicate P holds for all each of the natural numbers (0,1,2...) then you can deduce the formula $\forall n P(n)$. The resulting system is called ω-logic.

Obviously this is something of a "cheat" since you no longer have an effective theory. As one example (maybe there are better ones) of how it can be used, Michael Rathjen's article "The Art of Ordinal Analysis" describes using the $\omega$-rule to analyze stronger and stronger arithmetic theories, and is pretty interesting.
show/hide this revision's text 2 edited body; added 40 characters in body

By Gödel's incompleteness theorem, there can't be any such axiom in a first-order, recursively enumerable theory.

You can axiomatize $\mathbb N$ by adding an infinitary rule of inference, the Hilbert $\omega$-rule:

$$P(0)\wedge P(1) \wedge P(2) \wedge \cdots \over \forall n P(n)$$

to PA for each arithmetic predicate P. This says, if predicate P holds for all the natural numbers (0,1,2...) then you can decude deduce the formula $\forall n P(n)$. The resulting system is called ω-logic.

Obviously this is something of a "cheat" since you no longer have an effective theory. As one example (maybe there are better ones) of how it can be used, Michael Rathjen's article "The Art of Ordinal Analysis" describes using the $\omega$-rule to analyze stronger and stronger arithmetic theories, and is pretty interesting.
show/hide this revision's text 1

By Gödel's incompleteness theorem, there can't be any such axiom in a first-order, recursively enumerable theory.

You can axiomatize $\mathbb N$ by adding an infinitary rule of inference, the Hilbert $\omega$-rule:

$$P(0)\wedge P(1) \wedge P(2) \wedge \cdots \over \forall n P(n)$$

This says, if predicate P holds for all the natural numbers (0,1,2...) then you can decude the formula $\forall n P(n)$. The resulting system is called ω-logic.

Obviously this is something of a "cheat" since you no longer have an effective theory. As one example (maybe there are better ones) of how it can be used, Michael Rathjen's article "The Art of Ordinal Analysis" describes using the $\omega$-rule to analyze stronger and stronger arithmetic theories, and is pretty interesting.