Claim. Given two sets $A$ and $B$ are finite. Then $A \cup B$ is finite.
I've already read [1], [2], and [3]. But I'm not convinced it has to be as complicated as that.
Following is a list of definitions I depend on:
- A set is finite iff its cardinality is a natural number.
- A set has cardinality $n$ iff it has same cardinality than $\{i \in \mathbb{N}:1 \le i \le n\}$
- Two sets have equal cardinality iff there is a bijection between them
Proof. Consider the following one-to-one function $g: A \cup B \rightarrow \{i \in \mathbb{N} : 1 \le i \le n_{A \cup B}\}$
$$ g(x) = \begin{cases} f_A(x) & \text{if $x \in A$} \\ n_A + h \circ f_B(x) & \text{if $x \notin A$, } \end{cases} $$
where $n_A$ is the cardinality of $A$, $n_B$ is the cardinality of $B$, $f_A$ is the bijection between $A$ and $\{i \in \mathbb{N} : 1 \le i \le n_A \}$, and $f_B$ is the bijection between $B$ and $\{i \in \mathbb{N} : 1 \le i \le n_B \}$.
If I were able to give a bijection
$$h : B \setminus A \rightarrow \{ i \in \mathbb{N} : 1 \le i \le n_{B \setminus A} \},$$
I could consider the case closed.
But how could I possibly define such a function $h$?
Best Answer
The key point here, which you implicitly assume in your notation, is that $B\setminus A$ is a finite set, and therefore $n_{B\setminus A}$ is a natural number.
Of course, this requires proof, but if you already can use this fact, then the existence of a bijection is given by the fact that it is a finite set.
Now, in order to prove this fact you need to show that if $f\colon B\to\{i\in\Bbb N\mid i<n_B\}$ is a bijection, then you can find one where $B\setminus A$ are mapped to the first $n_{B\setminus A}$ numbers. This is proved by induction.
But now this ends up being "as complicated" as any other more-direct proof that the union of two finite sets is finite via induction.
The main point to take from this is that being formal is not simple, and it is important to understand that sometimes even simple arguments take a lot of writing to formalize. And that when you want to prove something complicated enough which is ultimately about natural numbers, then you cannot really avoid induction.