A well-founded relation on lists

Question

Let $A$ be a set equipped with a well-founded relation $<$, let $LA$ be the set of finite lists of elements of $A$, and define a relation $\prec$ on $LA$ such that $\ell \prec m$ if $\ell$ is obtained from $m$ by replacing some element $x\in A$ occurring in $m$ with some finite list (perhaps empty) whose elements are all $<x$. For example, if $A=\mathbb{N}$ with its usual ordering, then in $LA$ we would have

$ (1,3,4,2,0) \prec (1,5,0) $

and also

$ (1,0) \prec (1,5,0) .$

In classical mathematics, I can prove that $(LA,\prec)$ is also well-founded, as follows. Suppose we had an infinite sequence $\cdots \ell_3 \prec \ell_2 \prec \ell_1$, and define a tree $T$ whose vertices are pairs $(n, x\in \ell_n)$ and whose edges are induced by the definition of $\prec$. That is, if we had $ \ell_2 = (1,3,4,2,0) \prec (1,5,0) = \ell_1 $ then there would be edges $(1,0) \to (2,0)$ and $(1,1) \to (2,1)$ and $(1,5) \to (2,3)$ and $(1,5) \to (2,4)$ and $(1,5) \to (2,2)$. Now exclude from $T$ all the trivial infinite branches (those whose second component is constant). By Konig's lemma, the resulting subtree $T'$ still has an infinite branch. This yields an infinite descending sequence in $A$, a contradiction.

This argument is nonconstructive in two ways: it uses the equivalence of well-foundedness with the nonexistence of infinite descending sequences, and it uses Konig's lemma. Is there a constructive proof that $(LA,\prec)$ is well-founded?

Answer 1

I don't know what counts as a constructive proof for you, but perhaps an explicit assignment of ordinals will help. Let's assume we have an assignment $\pi:A\rightarrow\alpha$ of ordinals below $\alpha$ to elements of $A$ such that $a<b$ implies $o(a)<o(b)$.

The operation on orderings you're dealing with is similar to the one in Higman's Lemma, so this is loosely based on the argument from "Ordinal Numbers and the Hilbert Basis Theorem".

Define $o((x_1,\ldots,x_n))=\#_{i\leq n}\omega^{o(x_i)}$. If $(y_1,\ldots,y_m)\prec(x_1,\ldots,x_n)$ then we may assume $$(y_1,\ldots,y_m)=(x_1,\ldots,x_{i-1},z_1,\ldots,z_k,x_{i+1},\ldots,y_m)$$ where each $z_j<x_i$, so $o(z_j)<o(x_i)$. Therefore $$\#_{i\leq m}\omega^{o(y_i)}=\#_{j\neq i}\omega^{o(x_j)}+\#_{j\leq k}\omega^{o(z_j)}$$ and since $\#_{j\leq k}\omega^{o(z_j)}<\omega^{o(x_i)}$, this ordinal really is smaller.

In particular, the height of LA is at most $\omega^{\alpha}$.

Answer 2

You may well have resolved this question offline by now, but in any case, here’s a direct constructive argument that it’s well-founded. I’ll use a few background lemmas; all are straightforward, and iirc several are in Paul Taylor’s papers on constructive ordinals.

Lemma 0. If $<_1$ is a subrelation of $<_2$ on the same set, and $<_2$ is a well-order, then so is $<_1$.

Lemma 1. A finite lex product of well-orders is a well-order.

Def 2. A fibration of sets-with-binary-relations is a map $f:X \to Y$, not necessary relation-preserving, such that whenever $y_1 < f(x_2)$, there's some $x_1<x_2$ with $f(x_1)=y_1$.

Lemma 3. If $f:X\to Y$ is a surjective fibration and $X$ is a well-order, then so is $Y$.

Def 4. Given a set-with-binary-relation $(X,<)$, and $x \in X$, write $X//x$ for the strict slice $\{ y\ |\ y < x\}$, and $X/x$ for the non-strict slice $\{ y\ |\ y \leq x \}$ (where “≤” is defined as “< or =”).

Lemma 5. Suppose a relation is transitive, and every non-strict slice is well-founded. Then the whole relation is well-founded.

Now: back to $LA$. Instead of your relation, work directly with its transitive closure, though all we really need to note is that this contains your relation (for invoking Lemma 0), and is transitive (to use Lemma 5 later). So we define: $l_1 < l_2$ if, writing $l_2$ as $[a_1,\ldots,a_n]$, there’s a decomposition $l_1 = m_1 ; \cdots ; m_n$ (where “;” is concatenation), such that for each $i ≤ n$, either $l_i = [a_i]$ or all entries of $l_i$ are $< a_i$, and such that for some $i$, it’s the latter.

Lemma 6. For any list $l = [a_1,…,a_n]$, the concatenation map $\prod_i LA/[a_i] \to LA/l$ is a surjective fibration (with the lex ordering on the product).

Main Lemma. For each $a \in A$, $LA/[a]$ is well-founded.

Proof. Work by induction on $a$. Suppose it holds for all $b<a$. Then the strict slice $LA//[a]$ is w-f by combining all the lemmas above: each non-strict slice $LA/l$ of $LA//[a]$ is by Lemma 6 a surjective fibrant image of a lex product of slices $LA//[b]$, with $b < a$; by IH, these are each w-f, so by Lemma 1 their lex product is, so by Lemma 3, the slice $LA/l$ is, so putting this together for all $l < [a]$, the strict slice $LA//[a]$ is w-f by Lemma 5. It follows directly that so is the non-strict slice $LA/[a]$, as required.

Theorem. $(LA,<)$ is well-founded.

Proof. By Lemma 5, it’s enough to show that each slice $LA/[a_1,\ldots,a_n]$ is well-founded. For this, essentially repeat the inductive step of the main lemma: it’s a surjective fibrant image of a finite lex product of slices $LA/[a_i]$, which are each well-founded by the main lemma.

Answer 3

There is a substantial literature on this. I do not have to time to look at the precise theorem you want, but I think you want to start from the constructive Kruskal theorem by Veldman, inductive minimal bad sequence arguments and the localic treatment of them. This paper connects to other computer science topics and is formalized in Coq.

Answer 4

Let $(A,\prec)$ be a set with a well founded relation. Then let

• $(L A,\prec)$ be the set of (finite) lists from $A$ together with the relation that Mike defines above and

• $(K A,\prec)$ be the set of Kuratowski-finite subsets of $A$ together with the relation

$$ U\prec V \quad\equiv\quad (\exists v\in V.\top) \ \land\ (\forall u\in U. \exists v\in V. u\prec v). $$

My definition explicitly requires $V$ to be inhabited; the same is also implicit in the wording of Mike's definition. This excludes $\emptyset\prec\emptyset$.

Then the obvious map $L A\to K A$ preserves $\prec$: it takes Mike's relation to mine.

The constructive proof that $(K A,\prec)$ is well founded is given in Prop 8.6 of my paper Intuitionistic Sets and Ordinals, JSL 61 (1996) 705-744. It is the "box" proof displayed on page 737 in the journal.

It follows (easily) that $(L A,\prec)$ is well founded too (Prop 1.7(a)).