Can we prove the existence of $A\cup B$ without the union axiom?

If $A$ and $B$ are sets, then $A\cup B$ is defined as follows: $$A\cup B:=\{x: x\in A \, \, \,\text{ or } \, \, \, x\in B\}.$$

In ZFC, $A\cup B$ exists because $\bigcup\{A, B\}$ exists by union axiom, and it is known that axiom of union is independent of rest of ZFC.

If there is a set such that $A\subseteq C$ and $B\subseteq C$, then we can define $A\cup B$ using the $C$ and separation axiom. But can I prove the existence of $C$ in ZF-Union? Thanks for any help.

Nice question!

It turns out that in $T=\mathsf{ZFC}-\mathrm{Union}$, we can prove that unions of finite sets exist. There is a (remarkably recent) paper devoted to this issue. What follows is a (very) brief account of my reading of (section 3 of) the paper:

Greg Oman. On the axiom of union, Arch. Math. Logic, 49 (3), (2010), 283–289. MR2609983 (2011g:03122).

(Unfortunately the paper is behind a paywall, and the author does not have a version in their page or in the arXiv. Contact me if you find difficulties accessing it.)

Of note is that the argument uses choice in essential ways, so the question remains whether unions of finite sets can be proved to exist in $\mathsf{ZF}-\mathrm{Union}$. (Similarly, but perhaps less surprisingly, replacement also plays a key role.)

First, note that $T$ proves that if $x,y$ are sets, then $x\cup\{y\}$ exists: Map each singleton $\{z\}$ in $\mathcal P(x)$ to $z$, and every other subset to $y$. Call this Lemma 1.

The basic theory of ordinals can be carried out in $T$ (e.g., any two distinct ordinals are comparable by $\subset$ and by $\in$), and (crucially) $T$ proves that every set is in bijection with an ordinal. Call this Theorem 1.

This argument requires some care for two reasons: First, the usual approach uses transfinite recursion, which uses the union axiom. Second, arguing about the existence of functions requires some care, since at this stage it is not even clear that Cartesian products exist. However, we have a way of circumventing the second issue, since some functions do exist, since we have the axiom of choice (stated in the form: Choice functions exist).

Oman's argument (which is really a careful reworking of Zermelo's original approach) goes as follows: Given $X$, begin with a choice function $G$ on the nonempty subsets of $X$. Call $f$ an approximation iff its domain is an ordinal, its range is contained in $X$, and for each $\alpha\in\mathrm{dom}(f)$, $$ f(\alpha)=G(X\setminus\{f(\beta)\mid \beta<\alpha\}). $$ Now check that approximations are compatible, and that every element of $X$ is in the range of some approximation. For the latter, letting $Y$ be the subset of $X$ consisting of those elements of $X$ that appear in the range of some approximation, note that for each $y\in Y$ there is a unique $\alpha_y$ such that there is some approximation $f$ with $\alpha_y\in\mathrm{dom}(f)$ and $f(\alpha_y)=y$. It follows that $F=\{(\alpha_y,y)\mid y\in Y\}$ exists, and one readily verifies that it is itself an approximation.

One completes the argument by checking that the range of $F$ is $X$. But if it is not, then letting $\gamma=\mathrm{dom}(F)$, we have that $F\cup\{(\gamma,G(X\setminus Y))\}$ is also an approximation (thanks to Lemma 1!). This is a contradiction, since the definition of $Y$ then implies that $G(X\setminus Y)\in Y$, which is absurd as $G$ is a choice function. This completes the proof of Theorem 1.

By the way, if you are not familiar with this argument, you may want to read the nice survey by Kanamori and Pincus,

Akihiro Kanamori, and David Pincus. Does $\mathsf{GCH}$ imply $\mathsf{AC}$ locally?. In Paul Erdős and his mathematics, II (Budapest, 1999), pp. 413–426, Bolyai Soc. Math. Stud., 11, János Bolyai Math. Soc., Budapest, 2002. MR1954736 (2003m:03076).

(Theorem 3.3.c is false, but this does not affect their exposition on Zermelo's argument.)

Using Theorem 1, Oman argues that (finite) Cartesian products exist: Given $x,y$, find ordinals $\alpha,\beta$ in bijection with them. If $\gamma=\max\{\alpha,\beta\}$, then it is easy to check that $\alpha\times\beta$ exists, since it is a subset of $\mathcal P(\mathcal P(\gamma))$. Replacement completes the proof.

It follows immediately that the collection of functions from $x$ to $y$ exists. Using this, we can now prove

Theorem 2. If $x$ is a set and $\{|y|\colon y\in x\}$ is a bounded set of ordinals, then $\bigcup x$ exists.

Note that the boundedness assumption is obviously necessary, and it is immediate in the presence of the union axiom. This could therefore be seen as the key feature that the union axiom gives us. As an immediate corollary, if $x$ is finite, then $\bigcup x$ exists, answering your question affirmatively.

Let's conclude by sketching the proof of Theorem 2: We may assume that no element of $x$ is empty. Let $\gamma$ be a bound for the cardinalities of the elements of $x$. For $y\in x$, let $S_y$ be the set of all surjections from $\{y\}\times\gamma$ onto $y$, and note that $S_y\ne\emptyset$. Now consider a choice function $G$ on $\{S_y\mid y\in x\}$, so for each $y\in x$, $G(y):\{y\}\times\gamma\to y$ is onto. Replacement now implies that $\bigcup x=\{G(y)(y,\alpha)\mid (y,\alpha)\in x\times\gamma\}$ is a set, and we are done.

As Andrés' answer points out, ZFC - Union proves the existence of finite unions, and much more. AC is in fact essential for this theorem, for ZF proves Con(ZF - Union + "there are $x,y$ such that $x \cup y$ doesn't exist").

Recall that $\aleph(x)$ is defined to be the least ordinal which does not inject into $x$ and $\aleph^*(x)$ the least ordinal which $x$ does not surject onto.

Lemma: For infinite $A,$ define $H'(A)= \{x: \forall y \in TC(\{x\}) (|y| \le |A|) \}.$ Then $H'(A) \subset V_{\aleph^*(A)^+}.$ In particular, $H'(A)$ is a transitive set.

Proof of lemma: Let $\kappa=\aleph^*(A).$ It suffices to find a surjection from $\kappa$ onto $\text{rk}``(TC(\{x\})$ for $x \in H'(A).$

We will recursively define surjections $f_{x,n}: \kappa \rightarrow \text{rk}``(\bigcup^n \{x\})$ for all $x \in H'(A).$ Suppose we have defined all such functions up through $n.$ Define a surjection $g_{x, n+1}: \kappa \times x \rightarrow \text{rk}``(\bigcup^{n+1} \{x\})$ by $(\alpha, y) \mapsto f_{y,n}(\alpha).$ For each $\alpha, \text{ot}(g_{x, n+1}``(\{\alpha\} \times x))<\kappa,$ yielding a canonical surjection $f_{x, n+1}: \kappa \simeq \kappa \times \kappa \rightarrow \text{rk}``(\bigcup^{n+1} \{x\}).$ This completes the recursion, and now we define a surjection $f_x: \kappa \simeq \kappa \times \omega \rightarrow \text{rk}``(TC(\{x\}))$ by $(\alpha, n) \mapsto f_{x, n}(\alpha).$

Now, to prove the main result, we work in the Bristol model, a certain submodel of $L[c]$ ($c$ a Cohen real over $L$) which, among many interesting properties, satisfies ZF + existence of a set $A$ such that $A$ does not inject into $\mathcal{P}^n(\alpha)$ for any ordinal $\alpha$ and $n<\omega.$ (See https://arxiv.org/pdf/1704.06939.pdf) Fix such an $A.$ Let $\kappa = \aleph(\mathcal{P}^{\omega}(A)).$

Let $M=\{x: \forall y \in TC(\{x\}) \exists n<\omega(|y| \le |\mathcal{P}^n(A)| \vee |y| \le |\mathcal{P}^n(\kappa)|)\}.$ Applying the lemma to $\mathcal{P}^{\omega}(A \cup \kappa),$ we see that $M$ is a transitive set. We check that $M \models \text{ ZF - Union + there are $x,y$ such that $x \cup y$ doesn't exist}).$

We get extensionality and foundation from $M$ being transitive. Pairing, infinity, and power set are clear. We get separation and replacement from $M$ being closed under subset and surjection (noting that if $x$ injects into $y,$ any surjective image of $x$ injects into $\mathcal{P}(y)$). Finally, $A, \kappa \in M,$ yet $A \cup \kappa \not \in M.$