3 of 3 formatting; spelling & grammar; slight reword of the very last phrase

Mathematics is not based on assumptions and beliefs, although the axiom systems are. It is based on the notion of computation. The notion of computation is invariant, it is the same in any sufficiently complex axiom system, so that the computers described by PRA, PA, ZF, ZFC, ZF+large-cardinals, or any other axiom system of sufficient power to describe a computer; are all the same.

This is different from other concepts in mathematics—the set of real numbers for example is notoriously different from axiom system to axiom system and within a given axiom system, from model to model. In some axiom systems for set theory, the real numbers have cardinality aleph-1 (the first uncountable cardinal), the most prominent being V=L (Godel's constructible universe). In some models of ZFC it has cardinality aleph-19. The question of the cardinality real numbers is not absolutely meaningful, because it is not computational.

If you use a computational foundation, you can get rid of your confusion—what I'll call "Godel disease". Every mathematician goes through Godel-disease when they hear about Godel's theorem, until actually studying logic. Godel's argument is essentially only showing that the notion computation, which is absolute, can be used to make axiom systems stronger, until you reach the limits of computation.

One can (reasonably) define mathematics as follows:

The problem of figuring out which computer programs halt and which ones don't.

The thing about computer programs, is that if they halt, you can see it in finite time (but it might take too long to wait), and if they don't, you can sometimes prove it (but it might take too long to find the proof, or the axiom system might be too weak). These things are absolute, and refer only to integers, and operations that are clearly meaningful. The only possibly non-meaningful thing here is the limit of infinite time, but I will assume that you can accept this mildest of all infinities.

To see that this definition includes nearly all of ordinary mathematics, consider any conjecture C, and ask:

Do the axioms of ZF (or ZF+large cardinals) imply C?

This question is about the halting of a computer program; it is asking:

Consider the computer program DEDUCE, which starts with the axioms of ZF and applies logic, and if it finds statement C halts. Does DEDUCE halt?

If you can solve the halting problem, you know which theorems are consequences of ZF.

But this is not quite all of mathematics, as you can see by taking statement "C" to be "program R doesn't halt", where R is the code of the program DEDUCE itself. This construction proves Godel's theorem.

Godel's theorem is not a limitation on mathematics, and Chaitin's intepretation is likely completely false. If you add the axiom that the program above doesn't halt (this is equivalent to the consistency of the axioms of ZF), then you get a stronger system. Iterating Godel's construction over all countable computable ordinals (the kind you can manipulate on a computer), for all we know, _proves every theorem of the form "Program P does not halt" (and even with oracles, so that it produces the answer to all matheamtical questions).

The iteration process makes the axiom system more complex, and allows even Chaitin's questions to be answered (demonstrably slowly, only as the ordinal becomes complex enough to have computational complexity greater than the complexity of the program you want to prove is minimal length). This makes mathematics incomplete at the upper end--- you need to give ever more precise descriptions of large countable ordinals.

This point of view places computations at the foundations, since unlike any other foundational concept, the concept of computation is independent of the axioms--- it is Turing computation in all reasonable definitions. Expressing all mathematical questions computationally makes it clear when they are testable, and the computational representations of models of set theory make it obvious that Banach Tarsky is just as false as true, since it can be forced either way.

The best way to rid yourself of Godel disease is as follows:

  • Ordinal analysis: This is Hilbert's program under a new name. It is alive and well in Germany. It is groping toward proving the consistency of ZF from a large countable ordinal. A highlights of this is Kripke-Platek set theory, which, unlike ZF, has an ordinal complexity which is entirely understood.
  • Cohen forcing: This is the analysis of models of set theory, but allowing one to adjoin new elements to the model which occur in any set where you have an infinite number of binary choices to select an element (like the set of reals, which have an infinite number of binary digits). Forcing makes it obvious that Banach Tarsky might as well be false (ZFC is not accurate in modeling the intuitive reals), you can take every subset of R measurable, you can make the continuum hypothesis true or false, and generally, you get absolutely undecidable questions about all collections that are too big to enumerate on a computer.
  • Reverse mathematics: This tries to identify the exact axiomatic strength of each theorem in mathematics

Each of these are reasonably active things in logic, but they are not advertised because logicians tend to speak in obscure jargon and keep things to themselves by erecting high barriers to entry around their field. You can find a good introduction to logic, and especially forcing, in Manin's book. There are good English articles online (by the German school) on ordinal analysis, and Harvey Friedman is the founder of the program of reverse mathematics.

If you start by learning the completeness theorem, this is the first step to getting rid of Godel disease, which is not the insurmountable dilemma that it appears to be.