Proof of additive counting principle? In my "Discrete Structures" textbook, the Additive Counting Principle is defined as:

If $\{S1, S2, . . . , Sm\}$ is a partition of a finite set S, then
$|S| = |S1| + |S2| + · · · + |Sm|$.

However, it goes on to say that

A formal proof would require diving into the foundations of mathematics (defining what we mean by cardinality, addition, etc)

and mentions that some of this sort of stuff was covered in an Introduction to Analysis class I already took.
Out of curiosity, what would this sort of proof look like?
 A: Here is a sketch of how I think it would go.
$1.$ First we define the natural numbers using the Peano axioms. The most useful being the principle of mathematical induction. I first came across the Peano axioms and arithmetic within the Peano axioms in the book Analysis $1$ by Terence Tao. If you would like a to read up on these axioms, maybe read the second chapter of this book. It's a short chapter.
$2.$ Define addition for the natural numbers and prove some basic results regarding addition. Such as the commutativity and associativity of addition of natural numbers.
$3.$ State all the relevant axioms for basic set theory. This allows us to define the set of natural numbers $N$.
$4.$ Define functions between sets. Also define the relevant notions of Injections, surjections and bijections.
$5.$ Use bijections to define the cardinality of sets. That is, a set $A$ is said to have cardinality $n$, if there exists a bijection $f : A \to \{1,\dots, n\}$. Where the set $\{1,\dots, n\}$ is a subset of the natural numbers and $n$ is a natural number.
$6.$ Define what a “finite set” is. Namely, a set $A$ is said to be finite if there exist a bijection from $A$ to $\{1,\dots,n\}$. Define what unions, intersections and disjoint sets are. These would be needed to prove the principle.
Now I believe that we have a good enough setup to prove the following theorem.
Theorem: Let $S_1,\dots,S_n$ be finite and pairwise disjoint sets. Then $$|S_1\cup \dots \cup S_n| = |S_1| + \dots + |S_n|.$$
Proof: We will use induction. For $n=1$, the result is true. So, suppose that for some natural number $n$, we have that $$|S_1\cup \dots \cup S_n| = |S_1| + \dots + |S_n|$$
We need to prove that $$|S_1\cup \dots \cup S_n\cup S_{n+1}| = |S_1| + \dots + |S_n| + |S_{n+1}|$$ Where $S_{n+1}$ is also pairwise disjoint to the other sets.
Let $A = S_1 \cup \dots \cup S_n=\{a_1,\dots,a_k\}$. Where $k=|A|$. Let $S_{n+1}=\{s_1,\dots,s_m\}$. Because all the sets are disjoint, we have that $A\cup S_{n+1}=\{a_1,\dots,a_k,s_1,\dots,s_m\}$(this is easy to prove from the definitions). Define a function $f : A\to \{1,\dots,k+m\}$ by $f(a_i)=i$ and $f(s_i)=k+i$. This does indeed define a bijection from $A$ to $\{1,\dots,k+m\}$. Thus, $|A\cup S_{n+1}|=k+m$. From our induction hypothesis, we know that $$|S_1\cup \dots \cup S_{n}|=|S_1|+\dots+|S_n|$$ Thus, we have that $$|S_1\cup \dots \cup S_n\cup S_{n+1}|=k+m=|S_1|+\dots+|S_n|+|S_{n+1}|$$
Hope you find this somewhat helpful! I might have missed a few points here and there. But if you would like to construct your own proof, I would suggest that you read the first three chapters of Analysis $1$ by Terence Tao. That should give you enough background to come up with a proof by yourself.
