Let $P:=\bigcup_{n\in \mathbb{N}} \mathcal{P}_n$ and $F:=\bigcup_{n\in \mathbb{N}} \mathcal{F}_n$, where $P\cap F=\varnothing$. Let $\mathcal{L}:=P\cup F$.

The sets $\mathcal{P}_n$ are the ones that contains all the $n$-ary relation symbols and the sets $\mathcal{F}_n$, all the $n$-ary function symbols. So set $\mathcal{L}$ is a lexicon. The symbols in $\mathcal{P}_0$ are called propositional letters and the ones in $\mathcal{F}_0$ are called constant symbols.

I'm trying to describe a first order theory $T$ for the real numbers.

Consider $\mathcal{L}:=\{0,1,+,\cdot, \leq\}$, where $0,1\in \mathcal{F}_0$, $+,\cdot \in \mathcal{F}_2$ and $\leq\, \in \mathcal{P}_2$, and $T$ the set of the sentences enumerated below.

  1. $\forall x\forall y \forall z(x+(y+z)=(x+y)+z)$
  2. $\forall x \forall y \forall z(x\cdot (y\cdot z)=(x\cdot y)\cdot z)$
  3. $\forall x \forall y(x+y=y+x)$
  4. $\forall x \forall y (x\cdot y=y\cdot x)$
  5. $\forall x(x+0=x)$
  6. $\forall x(x\cdot 1=x)$
  7. $\forall x \exists y(x+y=0)$
  8. $\forall x(x\neq 0 \rightarrow \exists y(x\cdot y=1))$
  9. $\forall x \forall y \forall z(x\cdot (y+z)=(x\cdot y)+(x\cdot z))$
  10. $\forall x(x\leq x)$
  11. $\forall x \forall y((x\leq y \land y\leq x)\rightarrow x=y)$
  12. $\forall x \forall y \forall z((x\leq y \land y\leq z) \rightarrow x\leq z)$
  13. $\forall x \forall y (x\leq y \vee y\leq x)$
  14. $\forall x \forall y \forall z(x\leq y \rightarrow x+z\leq y+z)$
  15. $\forall x \forall y((0\leq x \land 0\leq y) \rightarrow 0\leq x\cdot y)$

I want know how we may write the Axiom of Completeness for the real numbers knowing that the intended first order formula would evolve some quantification over sets of numbers, as well as quantification over numbers themselves. To try to avoid this problem I tried the following.

An ordered field is an $\mathcal{L}$-structure $\mathfrak{A}=(A,I)$ such that $\mathfrak{A}\models \varphi$, for each $\varphi\in T$. We'll denote each $I(s)$ by $s_\mathfrak{A}$.

An ordered field $\mathfrak{R}=(R,{[-]}_\mathfrak{R})$ is complete iff every non-empty subset of $R$ having an upper bound in $R$ have a least upper bound in $R$. We could write this as:

$$\mathfrak{R}\models (\forall X\in \mathcal{P}(R)\setminus \{\varnothing\})((\exists x\in R)(\forall y\in X)(y\leq x)\rightarrow (\exists x\in R)((\forall y\in X)(y\leq x) \land (\forall z\in R)(\forall y\in X)(y\leq z\rightarrow x\leq z))).$$

I've read some answers in Math Stack Exchange that said that the problem is that this axiom is a second order one, not a first order one (I think it's because of the quantification over sets of numbers), but I also have seen some people saying that it evolves a ``many-sorted logic'', which I don't understand what the difference is from the second order logic.

What am I struggling with? A second order theory is based on first order logic just like first order theories? Is there a difference between a second order theory and a two-sorted logic? I appreciate any suggestions of readings too. Thanks in advance!

For whom would like to know the books I'm using: I'm studying Kunen's ``The Foundations of Mathematics''. I've read the first chapter which talks about ZFC and now I'm studying the second one which talks about models and formal proofs. I'm sorry for any english mistakes: my first language is Portuguese.

  • 2
    $\begingroup$ You are right: there is no intrinsic difference between first and second order. In your example, the problem is that the theory of real closed fields is a very tame one but when you add completeness it gets very wild. You move from model theory to set theory, so to say. But the problem more a sociological one than a mathematical one. $\endgroup$ Mar 30, 2022 at 7:54
  • 1
    $\begingroup$ I has a second look to your axiomatization. If you do not add a form of comprehension axiom your completeness axiom tells almost nothing. $\endgroup$ Mar 30, 2022 at 12:41
  • 1
    $\begingroup$ @PrimoPetri is correct; you need some axioms that assert existence of some sets, otherwise you simply cannot state Dedekind-completeness of ℝ. This means that you cannot give a usable axiomatization of ℝ that has desired properties relative to ℕ without invoking at least a small amount of some set theory. If you want to see how it can actually be done, let me know. $\endgroup$
    – user21820
    May 1, 2022 at 21:20
  • 1
    $\begingroup$ Okay, first read this post, which gives a practical deductive system for FOL plus suitable rules/axioms for both PA and ST (Set Theory). One can do everything within ST, but for just real analysis one can first work within ST to construct ⟨ℤ,ℚ,ℝ,0,1,+,−,·,/,<⟩ and prove these axioms. Thereafter, you can do most real analysis using mainly those axioms and only occasionally using ST (e.g. using type-notation and comprehension). $\endgroup$
    – user21820
    May 4, 2022 at 19:59
  • 1
    $\begingroup$ For example, take a look at this construction of the positive square-root of 2 in ℝ, which only constructs a single set, and uses only those axioms after that. The point is that when you make everything 100% precise then it is clear that you cannot get anything from the Dedekind-completeness axiom if you cannot construct anything that you can apply it to. Feel free to post any questions about these things in this chat-room. $\endgroup$
    – user21820
    May 4, 2022 at 20:03

2 Answers 2


Similar to the inductive property of the integers, the completeness of the reals likely cannot be finitely axiomatized without appealing to set theory or higher order logics. Roughly speaking, the completeness of the reals asserts that each nonempty bounded set admits a supremum, so to state this as a single statement in first order logic, it is necessary to quantify over sets, propositions, or something else similarly powerful.

You can produce an infinite axiom schema for completeness however, by taking a hint from modern treatments of Peano. Originally, Peano's axioms stated the axiom of Induction by referencing sets, which at the time were (relatively) poorly understood. In modern study of Peano, to avoid dependence on sets, we replace "set" with "definable class" which gives us a first order axiom schema that acts as an analogue to the axiom of Induction. We can do the exact same thing to get a first order analogue of the completeness axiom of the reals. For each first order formula $\phi$ with free variables $x,v_1,\cdots,v_k$, assert the following as an axiom about real numbers. $$\forall(v_1,\cdots,v_k), \big[[\exists x, \phi(x,\overline{v})]\land[\exists y, \forall x, x\leq y \lor \neg\phi(x,\overline{v})]\big]\implies [\phi(\cdot,\overline{v})\text{ has supremum}]$$

Where $[\phi(\cdot,\overline{v})\text{ has supremum}]$ is shorthand for $[\exists y, \forall x, y\leq x \iff [\forall z, [z\leq x] \lor \neg\phi(z,\overline{v})]]$. Informally, this sentence says that if the class $\{x\in\mathbb{R} : \phi(x,v_1,\cdots,v_k)\}$ is nonempty and bounded, then it has a supremum. By asserting that this holds for every formula $\phi$ with any selection of parameters, we effectively assert that every definable class of real numbers obeys the Completion axiom. The only downside is that your list of axioms goes from 15 to infinity.

  • $\begingroup$ You have swept another downside under the rug. You say every definable collection of real numbers obeys the Completion axiom, but the second order version says every collection obeys the axiom. As there are only countably many definable collections, the first order version is weaker. As I understand it, that makes the proof that the complete ordered field is categorical fail. $\endgroup$ Apr 3, 2022 at 4:05
  • 1
    $\begingroup$ @RossMillikan Definability is relative to a given theory: mathoverflow.net/questions/44102/…. The proof power issue is correct, but this would overcomplicate the answer and is ultimately irrelevant. Moreover, sufficiently verbose theories of the reals will inherit the undecidability of the integers, so there is no effectively axiomatizable theory that proves every correct statement about the reals; not even $\sf ZFC$. No incomplete theory is first order categorical. $\endgroup$ Apr 3, 2022 at 4:22
  • $\begingroup$ But we really like that the reals are categorical. I am not a mathematician, but it seems we would rather accept a second order axiom than give up on the reals being categorical. $\endgroup$ Apr 3, 2022 at 4:40
  • 1
    $\begingroup$ @RossMillikan I agree that second order theories are both more useful and intuitive on subjective grounds, but that isn't what the question is about. The question is about first order axiomatizations and model theory, presumably because the asker is interested in these subjects. $\endgroup$ Apr 3, 2022 at 6:29

A second order logic is not quite the same as a first order logic.

To see this, notice that, given a a structure $M$, to verify e.g. $M\models \forall x \exists y(x+y=0)$, it suffices to check that for each $a\in M$, $M$ has an element $b$ such that $a+^Mb=0$. $M$ holds all the data needed to check this: it knows its zero, it knows its elements, and it knows how to apply the function $+^M$ to pairs of its elements.

On the other hand, to check whether a second order formula holds in $M$, we need data that is external to $M$: we need to know exactly what subsets it has.

As a consequence, satisfaction of a second order formula is not absolute (even when passing to an inner model of ZFC), while satisfaction of (even infinitary) first order formulas is absolute between transitive models: if $V\subseteq V'$ are models of set theory, $V$ transitive in $V'$, the set $\mathbf R^V$ that $V$ thinks is the field $\mathbf R$ of real numbers will still be a real closed field (and one consisting of real numbers, for an appropriately chosen construction of real numbers) according to $V'$, but it will not (in general) be complete, e.g. if $V'$ is a Cohen forcing extension of $V$: the elements of $\mathbf R^V$ are same in $V$ and $V'$ (by transitivity), but the power set is different.

Now, as you suggest, this "externality" can be circumvented by adding another sort to $M$: a sort containing all subsets of $M$, along with membership relation between the home sort and the new sort.

Call the resulting structure $M^{\mathcal P}$. Then it is easy to see that for each second-order formula $\varphi$, we can find a first-order formula $\varphi^{\mathcal P}$ such that for each $M$ we have $M\models \varphi\iff M^{\mathcal P}\models \varphi^{\mathcal P}$.

In fact, we can go even further: can also add sorts for subsets of arbitrary products of sorts if $M$ is multi-sorted, and we can also iterate this construction as many times as we want (even transfinitely many times). If we do that a strongly inaccessible $\kappa$ number of times, the resulting structure looks basically like $M$ with a model of ZFC stacked on top of it. In this structure, we can similarly treat sentences of logics of arbitrary order up to $\kappa$ as if they were first-order.

Here comes the kicker, though: being an $M^{\mathcal P}$ is not a first order property. For example, if we consider $\mathbf R^{\mathcal P}=(\mathbf R,\mathcal P(\mathbf R),\in)$, then by the Lowenheim-Skolem theorem, we can find a countable subfield $K\subseteq \mathbf R$ and a countable subset $\mathfrak X\subseteq \mathcal P(\mathbf R)$ such that $(K,\mathfrak X,\in)$ is an elementary substructure, and in particular, elementarily equivalent to it, so if $\varphi$ is a second-order formula expressing completness of the linear order, then $(K,\mathfrak X,\in)\models \varphi^{\mathcal P}$. However, since there is no countable complete dense linear order (with more than 1 point), it is obviously not true that $K\models \varphi$, so $(K,\mathfrak X,\in)$ is not $K^{\mathcal P}$ (indeed, $\mathfrak X$ is, effectively, only a countable family of subsets of $K$, so it can't be its power set).

  • $\begingroup$ I don't have a deep knowledge of Model Theory, so I don't understand most of what you wrote in your answer. Do you suggest me some book to understand these things? $\endgroup$ Mar 31, 2022 at 16:51
  • $\begingroup$ Well, there is both model theory and set theory involved. For the (first order) model theory part, I think (the introductory parts of) Marker's book and either of Hodges' books (all of them have model theory in the title, you should easily be able to find them) should be okay. I don't really use anything deep about second order logic here, only the definition of $\models$ (which is natural, especially once you know the definition for first-order formulas). For the set theory part, I'm not sure. Jech's set theory book is a standard reference, so it should probably have all the information. $\endgroup$
    – tomasz
    Mar 31, 2022 at 23:38
  • $\begingroup$ I know that you also talk about Set Theory. The thing is that most of what you said is about Model Theory, which I am studying through Kunen's book, as I mentioned. But I still don't understand the difference between two-sorted logic and second order logic. Is there any difference? Do you know any books that talk about theses differences? How do we state the Axiom of Completeness of the real numbers in first order logic terms? Can we do that using a two-sorted logic? I don't understand how what you wrote answer my questions because I don't have a great background in logic. $\endgroup$ Apr 1, 2022 at 16:38
  • 1
    $\begingroup$ The only difference between one-sorted and many-sorted structures is that a many-sorted structure consists of a family of sets (one for each sort), and the relation and function symbols are sorted (so that each argument of a function/relation symbol comes from a prescribe sort). For formulas, in addition, each variable is sorted in the obvious sense. The definition of satisfaction is natural. This has nothing to do with second-order logic (which is more about what syntax you allow, rather than the structures themselves - in particular, it can also be multi-sorted) in general. $\endgroup$
    – tomasz
    Apr 3, 2022 at 22:51
  • 1
    $\begingroup$ A natural example of a multi-sorted structure is a field together with a vector space over it. Then you have addition on each sort, multiplication on the field sort and multiplication with mixed arguments (going into the vector space sort). At least one of the books I mentioned does include multi-sorted structures in one of the introductory chapters. $\endgroup$
    – tomasz
    Apr 3, 2022 at 22:54

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .