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.

talkabout the integers. For example, the theory of real-closed fields is decidable, so does not let you distinguish a copy of the integers (because otherwise you could use it to pose Diophantine equations, which are undecidable). $\endgroup$ – Qiaochu Yuan May 16 '11 at 5:57moreof a worry, because, once one knows what sets are, it's rather easy to define "integer" (as "a member of the smallest set containing 0 and closed under adding and subtracting 1"). $\endgroup$ – Andreas Blass May 16 '11 at 13:379more comments