Has anyone ever proposed additional axioms? According to Wikipedia, Godel's incompleteness theorem states:

No consistent system of axioms whose
  theorems can be listed by an
  "effective procedure" (essentially, a
  computer program) is capable of
  proving all facts about the natural
  numbers.

This obviously includes our current system. So has anyone proposed any additional axioms that seem credible?
 A: Adding additional axioms would make more truths provable. But it wouldn't make all truths provable (unless the axiom was inconsistent with the already given ones, in which case all falsehoods would also be provable too).
So adding additional axioms isn't going to help make all the truths provable. I guess you could just add, say, Goldbach's conjecture and the Riemann hypothesis as extra axioms and carry on doing mathematics-PLUS! but why would you want to?
A: Sure, the continuum hypothesis.  We know, thanks to the work of Godel and Paul Cohen, that this is a legitimate axiom, in that it doesn't destroy consistency: you can't disprove it (or prove it) using Zermelo-Frank set theory. 
People do actually use the continuum hypothesis in model theory, for instance, where there are several results that depend on it.  For an article about its uses, cf. the Tricki page.
A: Set theory is completely full of new axioms, some of them expressing fundamental set principles, and many of them having consequences even in natural number arithmetic that are not provable without them (via consistency strength statements).
In the past fifty years of research in set theory, a major lesson that has been learned is that many many fundamental questions about set theory are simply independent of the usual ZFC axioms. This includes most all of the questions about infinite cardinal arithmetic, but also subtle questons about infinite combinatorics.  For example, Is the exponential function (size of power set function) injective on infinite cardinalities? Independent of ZFC. Do Souslin trees exist?  Independent of ZFC. Is the size of the smallest dominating family of functions $f:\omega\to\omega$ necessarily $\aleph_1$?  Independent of ZFC. Can Lebesgue measure be more than countably additive, when CH fails?  Independent of ZFC. 
There are hundreds of examples. 
The response to this phenomenon was naturally to investigate the various hypotheses that go beyond ZFC. So we now know a great deal about what happens when CH holds, or when it fails, or when CH fails but the dominating number is low, and so on. The effect of this is to treat these hypotheses as semi-temporary axioms within a domain of research, which may not be the same usage of axiom that you inquired about, but the effect is the same. 
The powerful method of forcing, invented by Cohen in order to prove the consistency of $ZFC+\neg CH$, allows us to show that many other theories are also consistent. This method has given rise to a number of forcing axioms, such as Martin's Axiom, the Proper Forcing Axiom, Martin's Maximum and many others. 
A much larger and very interesting class of axioms are provided by the large cardinal hierarchy, involving such notions as inaccessible cardinals, measurable cardinals, Woodin cardinals and so on. A curious feature of these strong axioms of infinity is that they imply certain highly regular features to occur among the projective sets of reals. Thus, although the axioms themselves seem to have nothing to do with sets of reals, they imply very nice properties for the sets of reals that we can easily define. Many set theorists take this as some kind of positive evidence for their truth. Meanwhile, the large cardinal hypotheses are intensely studied as a fundamental research effort to understand the nature of mathematical infinity. But you cannot do this without assuming that these cardinals exist, since this is provably not provable in ZFC, if consistent, and so these large cardinal hypotheses constitute new axioms. 
