Godel's theorem tells us that any sufficiently powerful consistent formal theory of the integers is incomplete; but what about formal theories of the real numbers? More precisely, what about theories of the real numbers that are categorical (i.e. have only one model)? One such theory is given by the ordered field axioms plus the least upper bound axiom (every non-empty set of reals that is bounded above has a least upper bound). Note that the usual Archimedean property is not the kind of axiom we can include in a theory of the reals if we want it to be a complete theory, because then we'll need axioms that explain what an integer is, and these will cause us to fall prey to Godel's theorem.
Tarski's decision procedure for real-closed fields is somewhat relevant, but note that it does not answer my question, since the field of real numbers is not the only real-closed field.
Incompleteness is a slippery subject, and I'm glossing over important technicalities (I suspect that a logician would say I should be more specific about what I mean by "every non-empty set of reals"), so experts should feel free to edit my post if it's clear to them that my question is based on some misapprehension (as long as it's also clear to said experts how I would ask the question once my misapprehension were cleared up!).
UPDATE: Maybe my question should have been something more like: Is there a meta-theorem that guarantees that all the questions that are likely to arise in a real analysis course are decidable? Or: Is there a decision-procedure for an interesting fragment of real analysis that includes all the standard theorems from a first course in real analysis? Perhaps the right context for this question would be some first-order theory that has the set of subsets of the reals and the set of functions from the reals to itself as primitives, with enough (but not too many!) axioms.
Best Answer
Let me address the updated version of your question.
There is a philosophical current running through parts of descriptive set theory, and this includes anything that might be described as classical real analysis, to the effect that the realm of Borel mathematics is comparatively immune to the chaos of independence. On this view, one regards the Borel functions, relations and objects as being the most explicitly given, and the land of the Borel is the land of explicit mathematics.
For example, an important emerging field is the theory of equivalence relations under Borel reducibility, arising out of the observation that many of the most natural equivalence relations arising in other parts of mathematics, such as isomorphism relations on classes of algebraic structures, turn out to be Borel equivalence relations on a standard Borel space. Set-theorists seek to understand the comparative difficulty of the corresponding classification problems for these relations by considering the relations under Borel reducibility. This concept provides us with a precise way to measure the comparative difficulty of two classification problems, which then assemble themselves into a complex hiearchy, increasingly revealed to us. To give one example, it falls out of this theory that there can be no Borel classification of the finitely generated groups up to isomorphism by means of countable objects (this relation is not "smooth").
This theory has been largely immune from the independence phenomenon, for several reasons. Perhaps the best explanation of this is the fact that Borel assertions have complexity $\Delta^1_1$, which lies below the Shoenfield absoluteness theorem.
Theorem(Shoenfield Absoluteness) Any statement of complexity $\Sigma^1_2$ is absolute between any two models of set theory with the same ordinals.
In particular, this implies that the method of forcing is completely unable to affect existence assertions about Borel objects, since such assertions would have complexity $\Sigma^1_1$, as well as more complex assertions. Because forcing is one of the principal tools by which set-theorists have come to exhibit independence, this means that Borel mathematics is completely immune from the forcing technology.
Furthermore, when there are sufficient large cardinals, then one can attain an even greater degree of absoluteness in various senses. For example, in the presence of large cardinals there are various strong senses in which the theory of $L(\mathbb{R})$ is invariant by forcing. Thus, even the realm of projective mathematics ($\Sigma^1_n$ for any $n$) is unaffected by forcing, when there are sufficient large cardinals.
At the same time, we know that it isn't strictly true even that Borel mathematics is immune from independence, since the $\Delta^1_1$ level of complexity includes all of arithmetic, which therefore admits the Gödel incompleteness phenomenon. But because the method of forcing is struck down, however, none of the more spectacular independence results in the realm of analysis, such as the independence results concerning CH and cardinal invariants, arise at the Borel level of complexity. Thus, I believe that the realm of Borel mathematics may be the best, although imperfect, answer to your updated question.
At the same time, it must be said that although the method of forcing is ruled out as a means of proving independence for Borel existence assertions, we have no meta-theorem that says that there will not be some future method that is able to establish independence for such assertions. Surely a major lesson of logic over the past century is the pervasiveness of the independence phenomenon, and I believe that it is only a matter of time for such methods to arise.