Context:
I am taking an introductory real analysis class (because I need the credit), and the professor has provided me with their notes on the subject. In the notes, the professor defines the real numbers as the unique structure (up to isomorphism) characterized by the following axioms:
$$ \begin{align*} [(1.1)] & \qquad \forall x\forall y\forall z((x+y)+z=x+(y+z))\\ [(1.2)] & \qquad \forall x\forall y \forall z ((x\cdot y)\cdot z=x\cdot (y\cdot z))\\ [(2.1)] & \qquad \forall x\forall y(x+y=y+x)\\ [(2.2)] & \qquad \forall x\forall y(x\cdot y=y\cdot x)\\ [(3)] & \qquad \forall x\forall y\forall z(x\cdot(y+z)=(x\cdot y)+(x\cdot z))\\ [(4)] & \qquad \forall x(0+x=x)\\ [(5)] & \qquad \forall x \exists y(x+y=0\land \forall z(x+z=0\iff y=z))\\ [(6)] & \qquad \forall x(1\cdot x=x)\\ [(6.1)] & \qquad 0\ne 1\\ [(7)] & \qquad \forall x((x\ne0)\implies\exists y (x\cdot y=1\land\forall z(x\cdot z=1\iff y=z)))\\ [(8)] & \qquad \forall x\forall y\forall z(x<y\implies x+z<y+z)\\ [(9)] & \qquad \forall x\forall y\forall z((x<y\land y<z)\implies x<z)\\ [(10)] & \qquad \forall x\forall y(x<y\lor y<x\lor x=y)\\ [(11)] & \qquad \forall x\forall y\forall z((x<y\land z>0)\implies x\cdot z<y\cdot z)\\ [(12)] & \qquad \forall P^1((\exists xP^1x\land\exists y\forall x(P^1x\implies x<y))\implies\exists y\forall x((Px\implies x\le y)\land\forall z(z<y\implies\exists x_1(Px_1\land x_1>z))) \end{align*} $$
Now according to my professor, "all of real analysis can be derived from these axioms" (this isn't true, of course, on account of the concepts from topology which are included in most real analysis courses, but I understand what they were trying to say.)
However, I'm skeptical about this claim. Specifically, I don't see any way to prove the Archimedean property from these axioms.
Prove the Archimedean property from second-order Dedekind completeness:
When I brought this up to the professor, they said that the Archimedean property was provided in the form of a theorem which states:
For every real number $x$, there exists an integer such that $n<x<n+1$.
However, in the proof of this theorem they assumed that the integers are exactly the elements of $\Bbb R$ obtained by finitely many additions and subtractions of $1$ - a property which I pointed out was not proven in the notes, and cannot be proven by first-order means. Based on a heuristic argument I would guess that for any limit ordinal $\lambda\in\omega_1$, there should be a model whose "integers" are order-isomorphic to $\lambda^*+\lambda$. The professor agreed that this at least seems reasonable, citing that restricting the integers as desired without using second-order logic or adding a new predicate to the language would require the infinite disjunction:
$$x=0\lor x=0+1\lor x=0+(-1)\lor x=0+1+1\lor\cdots$$
I then asked if there is a second-order proof of the desired property somewhere else, to which my professor responded that they "don't work with second order logic," and suggested that I look at Dedekind's Essays on the Theory of Numbers.
This completely failed to answer my question.
It seems to me that my professor, whose primary area of research is set theory, takes for granted the standard set-theoretic implementation of the naturals, integers, rationals, and reals (specifically using Dedekind cuts). Their reasoning seems to fall along the lines of "ZFC with the particular encoding of numbers that I am used to proves it, so we needn't worry about the details." But this isn't what I was promised. I was told that all of real analysis could be derived from the axioms listed above, not that all of real analysis can be represented in ZFC!
I know that Dedekind completeness of the real numbers implies the Archimedean property given the set-theoretic definition of the naturals as the smallest infinite well-order, but any set theory capable of talking about a "smallest" anything is already much stronger than the second-order theory of the reals. If I say "I can run from New York to Los Angeles in a day," I can't prove it by taking a commercial flight, so if we're going to make the claim that "these axioms uniquely characterize the real numbers," then we ought to prove it using these axioms.
With that in mind, I would like to know how, if at all, the Archimedeam property can be derived from these axioms.
(Once more: without assuming set theory)
OR prove the existence of the integers:
The proof of the Archimedean property in the notes essentially consists of "the integers are the subset of $\Bbb R$ containing all elements obtained by finitely many additions and subtractions of $1$," "the integers are unbounded" and "for every real number $x$, there exists an integer $n$ such that $n<x<n+1$." In order to prove this, we first need to define the integers. To this end, let
$$\sigma_\Bbb Z:=\forall x(P^1x\iff (x=0\lor \exists y (P^1y\land (y+1=x\lor y=x+1))))$$
Then $\exists !P^1\sigma_\Bbb Z$ is the formula asserting the existence and uniqueness of the set of integers (uniqueness is required so that the extension obtained by adding the predicate symbol $Z(x)\equiv`\text{$x$ is an integer'}$ is conservative). This is where I get lost. I don't really know anything about second-order logic, so I have no idea how to prove $\exists!P^1\sigma_\Bbb Z$.
Once this is done, however, the proof that the integers are unbounded is straightforward. Following that, we may state the Archimedean property as
$$\exists!P^1(\sigma_\Bbb Z\land\forall x\exists y(P^1y\land y<x<y+1))$$
Once we have proven the existence of the integers, the original proof that "for every real number $x$, there is an integer such that $n<x<n+1$" should be sufficient for this purpose.
Aside: Is this a set theory/model theory question? I mean, I'm trying to avoid thinking in terms of set theory, but at the same time the potential for unintended models is the whole reason for the problem.