Proofs of Baire category theorem

I would like to have a list of proofs of the fact that the real line is not meager (also very useful would be a reference to such a list, if it already exists somewhere).

My motivation is the following: in the article Definably complete and Baire structures we defined a first-order notion of Baire structures, and I would like to prove that every definably complete ordered field is definably Baire. To do that, a possible approach would be to take a proof of the fact that $\mathbb R$ is not meager, and adapt it to the first-order situation. The main obstacle to such an adaptation is the fact that we cannot define sets by recursion.

-
I'm struggling to think of two proofs that are interestingly different. Don't they all basically involve finding a nested sequence of closed sets with intersection in the complement of the meagre set? –  gowers Oct 9 '10 at 21:45
One somewhat concrete proof is presented in Simpson's Subsystems of second order arithmetic. The proof of the Baire category theorem there is does not literally define sets by recursion, which also cannot be done in weak subsystems of second-order arithmetic. However, I would view that proof as essentially just an effectivization of the usual proof, and so if you do not have the ability to define even sequences of points by recursion then it is not clear that you will be able to recast the proof in your setting. –  Carl Mummert Oct 11 '10 at 0:53
@gowers: there are at least two different proofs of the fact that R is not meager (corresponding to the two cases of Baire category theorem): one using the fact that R is a complete metric space, the other using the fact that [0,1] is compact. –  Antongiulio Oct 11 '10 at 10:05