Edit: This question has been rewritten, check the edit history for the original post.
Suppose that I want a completely formal first-order proof of some theorem in topology (doesn't matter which). Presumably, I would start by stating the [non-logical] axioms (those first order statements which do not require a proof) of topology, since any theorem will ultimately follow from these.
In analogy with abstract algebra, it is my impression that [general] topology may be regarded as the study of a particular class of structures, namely topological spaces.$^1$ And just as the basic properties of groups (the group axioms) form the basis of group theory, the basic properties of topological spaces serve, at least initially, as the axioms of topology.
The usual informal statement of the open-set definition of a topology goes something like this:
Let $X$ be a set and $\tau$ a family of subsets of $X$, then the pair $\langle X,\tau\rangle$ is a topological space iff:
$\tau$ contains the empty set and $X$,
$\tau$ is closed under [arbitrary] union,
$\tau$ is closed under [finite] intersection.
Which can be formally stated as
- $\emptyset,X\in \tau$
$\forall S\subseteq\tau.\bigcup S\in\tau$
3a. $\forall x,y\in\tau.x\cap y\in\tau$
3b. $\forall S\subseteq\tau.|S|<\aleph_0\implies\bigcap S\in\tau$
(the choice between 3a and 3b is a discussion for another time)
A somewhat natural question to ask is whether or not these represent the minimal axioms for topology and what, if anything, we might change without affecting existing results in topology. This brings me to my question. Suppose that $\langle X,\tau\rangle$ is a topological space. Is it necessary that $X$ be the maximal element of $\tau$?
Note: the following statements are equivalent$^2$
$X$ is the maximal element of $\tau$ (i.e. $\bigcup\tau=X$)
$\tau$ is a subset of the power set of $X$
(Proof in footnotes.)
At first, it might seem that the answer is an obvious "yes," but consider that a pair of sets $\langle X,\tau\rangle$ may satisfy each of the four listed requirements independently of whether or not $\bigcup\tau=X$.
In particular, it seems that if $\tau$ is a topology on $X$ and $X\subset Y$, then $\tau\cup \left\{Y\right\}$ is also a topology on $X$ - inasmuch as it preserves all topological properties of the space $\langle X,\tau\rangle$. That the underlying set of a space might then be any one of several elements of the topology would also justify the definition of a topological space being a pair, since the underlying set might differ from the maximal element of the topology.
If, however, it is required for any topological space $\langle X,\tau\rangle$ that $\bigcup\tau=X$ then the statement of the underlying set is redundant. With only cosmetic changes to existing terminology and conventions, it becomes possible to disregard the notion of topological space entirely in favor of considering only the topology itself.
More significantly, if it is necessary that $\bigcup\tau=X$ for any topological space $\langle X,\tau\rangle$, then the axioms of topology can be stated as follows:
$\tau$ is a topology iff:
$\forall S\subseteq\tau.\bigcup S\in\tau$
$\forall S\subseteq\tau.|S|<\aleph_0\implies\bigcap S\in\tau$
From this, the underlying set of a topology $\tau$ is simply defined as the maximal element. Furthermore, we may prove that $\bigcup\tau\in\tau$ (a topology contains its underlying set as an element), $\emptyset\in\tau$, and the closed-set definition of a topology, with minimal effort.
In fact, it might even be possible to formalize all of topology with a single axiom.
$^1$ A topological space may be defined as a set with no additional structure, a pair of sets with no additional structure, a relational structure, or an algebraic structure.
$^2$ Theorem:
$X$ is the maximal element of $\tau$ if and only if $\tau$ is a subset of the powerset of $X$.
Proof:
The existence of a maximal element is guaranteed by closure under arbitrary union.
subproof 1:
Suppose that $\tau$ is a subset of the powerset of $X$ satisfying the listed axioms. By definition, every set $U\in\tau$ must then be a subset of $X$.
Suppose that $X$ is not the maximal element of $\tau$. Then there exists some set $U\in\tau$ such that $U$ is not a subset of $X$. Therefore, by contradiction, if $\tau\subseteq\mathcal{P}(X)$ and all axioms hold, then $X$ is the maximal element of $\tau$
subproof 2:
Suppose that $\tau$ is a set containing $X$ as its maximal element and satisfying all listed axioms. By definition, every set $U\in\tau$ must then be a subset of $X$.
Suppose that $\tau$ is not a subset of the powerset of $X$. Then there exists some set $U\in\tau$ such that $U$ is not a subset of $X$. Therefore, by contradiction, if $X$ is the maximal element of $\tau$, then $\tau\subseteq\mathcal{P}(X)$.
Therefore $\tau$ is a subset of the powerset of $X$ if and only if $X$ is the maximal element of $\tau$.
If you really want to be precise, you have to define a topological space explicitly as a pair: $(X, \mathcal{T})$ where $X$ is a set (I assume we're in ZFC so we know what that is) and $\mathcal{T} \subseteq \mathscr{P}(X)$. These two facts could be called axiom (0), as it were.
The usual axioms then further state (there are at least two flavours possible for the finite intersection one):
I seem to recall Bourbaki also preferring the pair-definition (as part of their general "set with a structure" paradigm.
The fact that $\mathcal{T} \subseteq \mathscr{P}(X)$ is understood, often explicitly, by almost all texts that I have. Whether or not you call it an axiom or not doesn't matter, really; fact is that it holds. The 4 axioms I mentioned distinguish a topology from many other "set plus set of subsets" structure definitions, just like the specifics of a group or a ring distinguish those structures among others of the "set with operations and constants" type. The distinguishing features are the axioms, the others (set with a set of subsets) is part of the "type declaration", if you want to use a programming metaphor. The latter struture types are purely first order, the former second order in nature, so in logic formalism there is a difference.