While reading through this Wikipedia page about Tarski's axiomatization of the reals, a particular bit of text jumped out at me:
Tarski proved these 8 axioms and 4 primitive notions independent.
This raised two questions in my mind, after a bit of thought.
First of all, I wondered how one could prove a primitive notion independent from anything, as it doesn't seem to carry any sort of logical content with it.
Second of all, it seemed that one of the axioms was impossible to separate from another. Namely:
Axiom 7: $1\in\Bbb R$
Axiom 8: $1<1+1$
Given that $+$ is assumed only to be an operation on $\Bbb R$ and $<$ is assumed only to be a relation on $\Bbb R,$ I can't imagine how Axiom 8 can fail to imply Axiom 7. I've attempted to rephrase the axioms (and have made them a bit more satisfactory on a personal level), but I cannot see a way to alleviate this.
For those who are curious, I have managed to prove that none of the following axioms is implied by the rest of the axioms: 1,2,3,5,6,8. I'd like to play with Axiom 4 a while longer, so please don't give hints about that, unless it's necessary to answer me.
See :
A preliminary comment : the axioms are second-order logic; thus the interpretation of the set $R$ is not (necessarily) the domain of the model.
The first six axioms can be satisfied in an empty domain; thus, Axiom 7 is needed to ensure that $R$ is not empty.
Axiom 8 is needed in order enusere that $1$ is not the only object in $R$; see Tarski page 204 [Dover reprint : 216] : we can replace it adding the symbol "$0$" and the axiom : $0<1$.
We have to specify that $1 \in R$ because otherwise we can have a model with an empty $R$ and an object $1$ "external" to it.
Regarding the independence of the primitive notions, see Padoa's method, or see Tarski, page 184 [Dover reprint : 194].