1 Wellfounded part

Given a binary relation < on a set S, the subset W of S called the wellfounded part of S w.r.t. < is defined inductively as follows:

\frac{∀y < x. y ∈ W}{x ∈ W}

The corresponding induction principle easily yields the principle of wellfounded part induction:

\frac{∀x ∈ W. (∀y < x. P (y)) ⇒ P (x)}{∀x ∈ W. P (x)}

It also follows that < is wellfounded iff W = S.

2 The proof

Let < be a wellfounded relation on a set A, and let M(A) be the set of all finite multisets over A. We use set-notation for multisets. The letters a and b range over A; K, M and N range over M(A). We define the following abbreviations:

M < a ⇔ ∀b ∈ M. b < a
N <_{mult} M ⇔ ∃M_{0}, a, K. M = M_{0} ∪ {a} ∧ N = M_{0} ∪ K ∧ K < a
W = the wellfounded part of M(A) w.r.t. <_{mult}

Lemma 2.1 If ∀b < a. ∀M ∈ W. M ∪ {b} ∈ W and M_{0} ∈ W and ∀M <_{mult} M_{0}. M ∪ {a} ∈ W then M_{0} ∪ {a} ∈ W.

Proof by definition of W. Let N <_{mult} M_{0} ∪ {a}. We need to prove N ∈ W. There are two possibilities why N <_{mult} M_{0} ∪ {a} holds:

• If N = M ∪{a} for some M <_{mult} M_{0} then N ∈ W follows from the third assumption.

• If N = M_{0} ∪ K for some K < a then N ∈ W follows from the first two assumptions by induction on the size of K.

□

Lemma 2.2 If ∀b < a. ∀M ∈ W. M ∪ {b} ∈ W then ∀M ∈ W. M ∪ {a} ∈ W.

Proof From Lemma 2.1 by wellfounded part induction. □

Lemma 2.3 ∀M ∈ W. M ∪ {a} ∈ W.

Proof From Lemma 2.2 by wellfounded induction on a. □

Theorem 2.4 M ∈ W.

Proof by induction on the size of M. The base case ∅ ∈ W holds because there is no N <_{mult} ∅. Lemma 2.3 covers the induction step. □

Thus we know that <_{mult} is wellfounded on all of M(A).