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.

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