incompleteness in real analysis 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.
 A: Some points which I missed in goldstern’s answer:


*

*A categorical theory is always complete. In particular, the second-order theory of the reals with the least upper bound axioms as you defined it in the question is complete.

*The question is sort of self-contradictory, because the least upper bound axiom implies the Archimedean property.

*In order to fall prey to Gödel’s theorem, the theory needs not only to define integers, but also to be recursively enumerable. The latter never holds for second-order theories, but it can fail even for first-order theories. For example, the set of all valid statements in the standard model of first-order arithmetic is complete despite containing integer arithmetic.
A: 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.
A: I think you are asking several questions, so there are several answers:


*

*It is important to distinguish between first order theories and higher order theories.  

*A first order theory (as long as it has an infinite model) is never categorical, by the Löwenheim-Skolem theorem.  

*For example, the first order theory of the reals as an orderd field has models in every infinite cardinality. The smallest model is the set of real algebraic numbers.  You cannot  formulate the least upper bound property in this theory, and you cannot formulate the property "is a natural number".   On the plus side, the theory has a nice set of axioms, and it is categorical in every uncountable cardinality.  (I.e., there is a unique model of size kappa, for each uncountable kappa.)  [Edit: This is not correct, as pointed out by Chris Eagle below. The first order theory of the complex field is uncountably categorical.]

*If you talk about second order theories, then the theory of the reals is categorical, and so is the theory of integers. (Also, in second order, the integers are definable within the reals.) In fact there is a finite set of second order statements (including "second order induction"; e.g. in the form "every nonempty set has a least element) characterizing the integers. (Or a single second order statement.) 

*There is no canonical concept of "second order provability". More precisely, the set of second order consequences (or even the set of first order consequences) of a second order axiom is in general not recursively enumerable (=not computably enumerable). This is one reason why proofs that are intended to be second order are usually formulated as first order proofs in set theory.  (For example, my claim that "the second order theory of the reals is categorical" is provable in first order set theory.  Of course, first order set theory cannot tell you explicitly what this second order theory is, by incompleteness) 
