Axiomatization of the real numbers in first order logic

Question

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.

Answer 1

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.

Answer 2

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).