Is there a first-order-logic for calculus?

I just finished a course in mathematical logic where the main theme was first-order-logic and little bit of second-order-logic. Now my question is, if we define calculus as the theory of the field of the real numbers (is it?) is there a (second- or) first-order-logic for calculus? In essence I ask if there is a countable model of calculus.

I hope my question is clear, english is my third language.

-
Important parts of calculus are captured in Differential Algebra. There are even nice model-theoretic results. – André Nicolas Jan 27 '12 at 14:53
Can we define calculus as the theory of the field of real numbers? Calculus also uses the poset structure of the reals. – user23211 Jan 27 '12 at 15:16
I have added [model-theory], which I am ~80% sure fits. If someone disagrees feel free to remove it. – Asaf Karagila Jan 27 '12 at 17:14
@ymar: actually one can define the poset structure in purely field-theoretic terms (namely $a \le b$ iff there exists $c$ such that $a + c^2 = b$). See en.wikipedia.org/wiki/Real_closed_field . – Qiaochu Yuan Jan 27 '12 at 17:17
@user23823: I am not sure if I agree with your definition of calculus. Shouldn't "calculus" include, at the very least, a notion of the limit of a sequence? – Qiaochu Yuan Jan 27 '12 at 17:28

The first order theory of the algebraic and order properties of the real numbers is the theory of real closed fields, and you will find various axiomatizations when you follow the link.

A structure with the first order properties of the real numbers may not satisfy the completeness axiom, which is not first order. For example, the field of hyperreal numbers has the same first order properties as the field of real numbers, but the set of finite numbers is nonempty and bounded above by any infinite number, yet has no supremum.

-

Fields can be studied in the first-order signature $(0,1,+,\times, =)$. For the reals, you could move to a larger language for ordered fields. It is very common for model theorists to study fields in this way.

By the Lowenheim-Skolem theorem, any first-order theory with an infinite model has a model that is countably infnite. This includes the set of all statements in the language of fields that are true in $\mathbb{R}$. It also includes ZFC.

-

Real analysis, including set theory, can be formalised within ZFC. As a first-order theory, ZFC has a countable model by the Löwenheim-Skolem theorem, so the answer to your question is yes.

You ask whether there is a "logic for calculus", which is a little bit misleading: we usually think of a logic as a language together with a proof system and a semantics. First and second order logic are logics or formal systems under this description.

What is needed for calculus in addition to the basic formal system is a signature consisting of those non-logical constants required to pick out those relations, functions and constant elements which we would need to refer to in order to axiomatise the structures involved (in this case, the complete ordered field), and a set of axioms sufficient to prove the theorems of calculus.

As I said above, the background theory employed is usually that of set theory, but in fact that's not necessary: one could drop the powerset axiom and in its place just assert the existence of $\mathbb{R}$, and perhaps the set of functions $2^\mathbb{R}$, depending on how much one wanted to prove.

-

As others have mentioned, you aren't looking for a logic in which to do analysis, but a signature and a model. In this respect you must be somewhat careful: the structure $(\mathbb{R},0,1,+,\cdot,\leq)$ will not give you analysis. In fact, it admits quantifier elimination and is decidable, so it is quite boring. The classical structure of analysis is the structure $(\mathbb{R},\mathbb{Z},0,1,+,\cdot,\leq)$, with a "name" for the integers. This allows tuple coding, and all the good stuff that comes with it. Of course, by Lowenhiem-Skolem, you can get countable models that admit analysis.

-

I take the view that the proper logical framework in which to do model theory for structures in analysis is continuous logic. For more information on the subject, look up the webpage of Ward Henson.

-