An infinite set of axioms in ZF? What does that mean? Before write this question, I looked around enough in this forum for a possible answer and although there are many similar questions, I couldn't find one answer which understand or satisfies me. I did read somewhere a long time ago that Zermelo-Frankael has an infinite set of axioms. Moreover, the same is true for Peano's system and as I perceive there are many differences among the systems with a finite set and infinite set of axioms (I don't know exactly even what the latter means in practice)
So, can you explain me please what does the sentence "Zermelo-Frankael has an infinite set of axioms" mean?
Any kind of comments and answers are welcomed, although I would prefer a sort of answer or comment which doesn't assume a deep understanding of the above-mentioned notions. 
 A: If by "what does it mean" you mean "what does it mean" I have to ask what do you mean, what does it mean? Saying that ZF has infinitely many axioms means exactly what it says. There are infinitely many primes. There are only finitely many natural numbers less than $3$. There are infinitely many axioms of ZF.
Probably you actually understand that, and you're just puzzled because you see presentations of the axioms in finitely much space, making it look as though there are only finitely many axioms. No, some of those "axioms" are, formally, not axioms but rather infinite sets of axioms. This is using the word "axiom" in a formal sense, requiring it to be a formula of first-order logic.
Consider the axiom, or rather axiom schema, of Separation. Informally this says that for any set $A$ and any property $P$ that the elements of $A$ may or may not satisfy, $$\{x\in A:P(x)\}$$ is a set. The reason this counts as infinitely many axioms is that in the formal system in question there is no way to "say" "for every property $P$", so formally we have infinitely many axioms, one for each $P$.
For example, the existence of $$\{x\in\Bbb R:x>0\}$$follows from one instance of Separation, while the existence of $$\{x\in\Bbb R:x^2>3\}$$requires another instance of the axiom scheme. Formally two different axioms, one for the predicate $x>0$ and one for the predicate $x^2>3$.
Why not just add "for every property $P$" to the formal system? Then it becomes a "second-order" system, and second-order logic is harder.
