12
$\begingroup$

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?

$\endgroup$
9
  • $\begingroup$ What is the definition of well-foundedness if not "infinite descending sequences don't exist?" $\endgroup$ Jan 6, 2015 at 17:34
  • 4
    $\begingroup$ @NoahS I gave a link. $\endgroup$ Jan 6, 2015 at 18:07
  • 4
    $\begingroup$ This looks suspiciously like a version of the hydra game. I have no experience with constructive mathematics, but maybe it is possible to adapt the usual proof via ordinal numbers to prove well-foundedness here. Does this work? Can one even constructively prove that ordinals are well-founded? $\endgroup$ Jan 6, 2015 at 21:20
  • 1
    $\begingroup$ @ToddTrimble I thought of that too, but I don't think it can be, because the lexicographic order is not well-founded: AB > AAB > AAAB > AAAAB > ... $\endgroup$ Jan 6, 2015 at 22:43
  • 1
    $\begingroup$ @darijgrinberg I only used $A=\mathbb{N}$ to illustrate the definition of $\prec$. I definitely do not want to assume that finite lists in $A$ have upper bounds (and it's not true for a general well-founded relation). $\endgroup$ Jan 10, 2015 at 8:46

4 Answers 4

3
$\begingroup$

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}$.

$\endgroup$
4
  • $\begingroup$ What is $\#$ in this definition? I presume it's ordinal multiplication or something like that. $\endgroup$ Jan 9, 2015 at 19:13
  • 1
    $\begingroup$ @JohannesHahn: The natural (Hessenberg) sum; see e.g. en.wikipedia.org/wiki/Ordinal_arithmetic#Natural_operations . $\endgroup$ Jan 9, 2015 at 19:24
  • 1
    $\begingroup$ A constructive proof means a proof that's valid in constructive mathematics, in particular no excluded middle or choice. But this argument might work, for an appropriate constructive definition of "ordinal". $\endgroup$ Jan 10, 2015 at 8:51
  • 1
    $\begingroup$ The textbook theory of ordinals uses excluded middle at every level. I strongly suspect that the "appropriate" theory of constructive ordinals that is needed for this problem is the "directed" kind. A key part of this theory is exactly the proof in my answer to the question. $\endgroup$ Mar 11, 2015 at 10:52
3
$\begingroup$

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.

$\endgroup$
2
  • 1
    $\begingroup$ Thanks for posting the proof. It has now been formalized in Lean: github.com/leanprover-community/mathlib/pull/14190/…. Notice that acc (<) x in Lean means that the non-strict slice $X/x$ is well-founded. $\endgroup$
    – Junyan Xu
    May 17, 2022 at 17:21
  • 1
    $\begingroup$ @JunyanXu : Thanks for the pingback — very happy to hear this turned out useful, and nice to see it formalised! $\endgroup$ May 24, 2022 at 14:44
2
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ Thanks! But I can't quite see how all of that helps at the moment: even the constructive version seems to be about a notion of "well-quasi-order" involving comparing elements of infinite sequences, and I don't see how to get from there to the constructive notion of well-foundedness. $\endgroup$ Jan 19, 2015 at 6:10
2
$\begingroup$

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)).

$\endgroup$
2
  • 1
    $\begingroup$ I don't see why the map $L A \to K A$ preserves $\prec$. For instance, if $A=\mathbb{N}$ with its usual ordering, then in $L A$ we have $(3,0) \prec (3,1)$, but I don't think we have $\{3,0\} \prec \{3,1\}$ in $K A$: for $u=3\in \{3,0\}$ there is no $v\in \{3,1\}$ such that $3\prec v$. $\endgroup$ Mar 11, 2015 at 23:27
  • $\begingroup$ OK I'll think about that, but I am pretty confident that the result in my paper has to be the core of the solution. $\endgroup$ Mar 12, 2015 at 8:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.