Why 'There exists a non empty set' is an axiom in some axiomatic set theories.

Question

Some axiomatic set theories formulates the system by taking an axiom 'There exists a non empty set'. I am not clear how the statement become an axiom since after all the definition of a 'set', we have lot of examples like 'the set of all students in the class having more than 50% marks in a particular exam', etc. What exactly mean by the 'existence' of such a set (example)? Why it can't make the statement 'There exists a non empty set' as a proposition?

Answer 1

In Mathematical Induction, we Prove some $P(0)$ ; then Prove $P(n) \implies P(n+1)$ , then we claim $P(n)$ is always true.
This whole thing will collapse if we do not Prove $P(0)$.

Similarly in Set Theory, we should start by claiming that there is a set with 1 element, else we maybe talking about nothing.

Here is one such "unreal" theory :

Let M be the set of humans born on Mars.
Let N be the set of humans born on Neptune.
<< More Axioms here >>

Theorem: Every human in M is also in N. [[ Proof left as Exercise ! ]]
Theorem: Humans can be born in 2 Planets. [[ Proof : Every human in M (was born on Mars) is also in N (was born on Neptune) thus was born on 2 Planets ! ]]

Obviously, these are meaningless.

The Core Issue is when we made the Axioms, we did not claim that M & N have atleast 1 element.

Likewise, we can make Axioms about Natural Numbers, but to ensure that we are talking about something (rather than nothing), we have to make the Axiom that 1 is a Natural Number.

In Axiomatic Set Theory, we have to make the Axiom about non-empty set, otherwise, we make be talking about nothing (rather than something) and make all sorts of meaningless theorems.

Some Demonstrative Material :

[A] Empty domains

The definition above requires that the domain of discourse of any interpretation must be nonempty. There are settings, such as inclusive logic, where empty domains are permitted.
https://en.wikipedia.org/wiki/First-order_logic

[B] Empty domain

In first-order logic the empty domain is the empty set having no members. In traditional and classical logic domains are restrictedly non-empty in order that certain theorems be valid.
https://en.wikipedia.org/wiki/Empty_domain

[C] Free logic

A free logic is a logic with fewer existential presuppositions than classical logic. Free logics may allow for terms that do not denote any object. Free logics may also allow models that have an empty domain. A free logic with the latter property is an inclusive logic.
https://en.wikipedia.org/wiki/Free_logic

[[ The last reference has one Example similar to my "Mars+Neptune" Example, where "Something is Pegasus" is Proved ! ]]

Answer 2

Based on discussion in the comments, I think its worth writing this out as an answer. I should clarify, I interpret OP's question as about standard ZF(C). Since the only ZF axiom of the form OP describes is the axiom of infinity, I will focus on that. I won't worry about ZF formulated in a non classical logic.

In short, You do not need an axiom as you describe to derive the existence of some non-empty set (in standard ZF). We add the axiom of infinity so that we ensure the existence of an infinite set.

First, to clarify your confusion. Axiomatic set theories do not have sets like "the set of all students...". In ZF, the only objects are sets. So every set, except the empty one, is a set of sets. Some axiomatic theories have "urelements", which are not sets but are atom-like. Even so, you will not get a "set of all students..." as you described.

Most approaches to model theory of FOL (first order logic) stipulate that the domain of discourse is non-empty, by definition. See definition 1.1.2 of Marker's "Model Theory: An Introduction" (a standard text on the subject). Notice that FOL is independent of ZF(C). So this happens before we worry about axiomatizing ZF(C). This is not adding an axiom to ZF(C). This has to do with the definition of a model of FOL

Since ZFC lives on top of FOL, the same is true of models of ZF. Thus, empty models of ZFC are ruled out, by definition. For more, see this answer, or this Wikipedia entry at this section or this section. So it is a theorem in ZF-inf (ZF without axiom of infinity) that $\exists x(x = x)$. Applying axiom of specification with the formula $\phi :\equiv x \not= x$, we can derive $\exists x \forall z (z\not\in x)$. Applying the axiom of pairing with this newly derived set lends a set with exactly one element.

All this aside, we could tweak the definition of a model of FOL to allow for an empty domain. In this case, we would need to assert the existence of a set by hand, but it need not be a non-empty set. Asserting the existence of the empty set would allow us to derive to the existence of a non-empty one using pairing. So an axiom as OP describes simply is not necessary to establish the existence of a non-empty set.

So then why does ZF have the axiom of infinity? We add the axiom of infinity so that we ensure the existence of an infinite set. An infinite set cannot be derived with a finite application of axioms in ZF-inf. Since FOL only allows finite deductions, and thus only finite applications of the axioms of ZF-inf, we cannot derive an infinite set in ZF-inf. Since we want ZF to have infinite sets, we need to add at least one in manually. Cue axiom of infinity.

As for the other set theories you allude to, lack of a reference, I cannot speak to why they include an axiom as you describe. But, ZF(C) is the standard approach to set theory.