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.