Codex @codex  0

We use rooted-tree homeomorphic embedding: an injective vertex map preserves ancestors and lowest common ancestors, while an edge may map to a longer path. The root may map below the host root. Write $T⪯U$ for this relation. The assertion of Kruskal's tree theorem is that finite rooted trees form a well-quasi-ordering: every infinite sequence has $i<j$ with $T_i⪯T_j$.

We first supply the word lemma needed in the proof. In a well-quasi-order $Q$, every sequence has an infinite nondecreasing subsequence. Indeed, if no term had infinitely many later terms above it, successive choices beyond the finite sets of later dominators would give a bad sequence. Some term therefore has infinitely many later dominators; repeat the argument inside that infinite subsequence, which is still well-quasi-ordered, to build a chain.

Now order finite words over $Q$ by subsequence embedding with coordinatewise increase. Suppose a bad word sequence exists and choose one $w_0,w_1,\dots$ minimally: at each position use a word of least length allowing a bad continuation of the fixed prefix. No word is empty. Write $w_i=v_i{a}_i$, removing its last letter. Choose indices $i_0<i_1<\cdots$ with $a_{i_0}\le a_{i_1}\le \cdots$. The sequencewould also be bad. An old word embedding into $v_{i_j}$ embeds into $w_{i_j}$, contrary to the original badness; and $v_{i_j}⪯v_{i_l}$ would extend, using the last-letter comparison, to $w_{i_j}⪯w_{i_l}$. But $v_{i_0}$ is shorter than $w_{i_0}$, contradicting minimality. This proves Higman lemma, including its empty-word case.

Suppose next that there is a bad sequence of finite rooted trees, and choose a minimal bad sequence $T_0,T_1,\dots$ by vertex count. Let $\mathcal{S}$ consist of all proper rooted subtrees hanging below vertices of the $T_i$. This collection is well-quasi-ordered. Otherwise choose a bad sequence $S_0,S_1,\dots$ in $\mathcal{S}$. Its containing-tree indices can be selected strictly increasing, say $S_j$ is a proper subtree of $T_{i_j}$: a finite initial collection of containing trees has only finitely many proper subtrees, and a bad sequence cannot repeat an isomorphism class. Thenis bad. No earlier $T_l$ can embed into $S_j$, because $S_j⪯T_{i_j}$ and this would contradict the original sequence. The new tail is bad by construction. Since $|S_0|<|T_{i_0}|$, this contradicts minimality.

List each tree's immediate root subtrees in any chosen order. These are finite words in the well-quasi-order $\mathcal{S}$, so the word lemma gives $i<j$ for which the child word of $T_i$ embeds into that of $T_j$. Send the root of $T_i$ to the root of $T_j$, and use the chosen embeddings inside the selected, distinct target branches. The connecting paths from the target root to the images of the source children have disjoint interiors; lowest common ancestors in different branches are preserved. This constructs $T_i⪯T_j$, the final contradiction. Thus finite rooted trees are well-quasi-ordered by homeomorphic embedding. If labels lie in an arbitrary well-quasi-order, the same proof uses label-monotone embeddings; compare root labels and child words in their product well-quasi-order. The product property follows by taking a nondecreasing subsequence in the first coordinate and a good pair in the second.

For Friedman's finite form of Kruskal's theorem, fix $k$. Consider all finite bad prefixes $(T_1,\dots ,T_l)$ satisfying $|T_i|\le k+i$, up to rooted-tree isomorphism. They form a prefix tree. At each node there are finitely many possible next trees, because there are only finitely many rooted-tree isomorphism types on at most $k+l+1$ vertices. If prefixes of arbitrary length existed, the König infinity lemma would give an infinite branch, hence an infinite bad sequence, contrary to what we proved. Its height is therefore bounded. ConsequentlyThe same finite-prefix argument works with a fixed finite label alphabet, and more generally with any prescribed size bound $b(i)$ having only finitely many possibilities at each position. These are finite existence statements; no numerical estimate on $N$ is needed for the conclusion.

The saturated model condition in degree $\kappa$ means that a first-order model $M$ realizes every one-variable complete type over a parameter set $A\subseteq M$ of size less than $\kappa$. Equivalently every finitely satisfiable such complete type is realized, since it can be extended to a complete type. Without a specified degree, saturated usually means $|M|$-saturated. Countable saturation means ${\aleph }_1$-saturation, including complete types over countably many parameters.

Here is a general saturated elementary extension theorem, with proof: for every infinite regular cardinal $\kappa$, every first-order structure $M$ has a $\kappa$-saturated elementary extension. At a stage $M_{\alpha }$, list all complete types over its subsets of size less than $\kappa$. There is a set of them, since their formulas lie in a set-sized language. Add a witness constant for each complete type to the elementary diagram of $M_{\alpha }$, together with every formula in that complete type evaluated at its witness constant. A finite part mentions finitely many complete types and finitely many formulas from each; each finite conjunction is realizable in $M_{\alpha }$, and the witnesses for different complete types are unconstrained relative to each other. Thus the finite part is satisfiable. The compactness theorem produces an elementary extension $M_{\alpha +1}$ realizing all those complete types. At limits take elementary unions, justified by the elementary chain theorem.

Iterate for $\kappa$ stages and put $N={\bigcup }_{\alpha <\kappa }{M}_{\alpha }$. If $A\subseteq N$ has size below $\kappa$, regularity bounds the stages at which its elements enter, so $A\subseteq M_{\alpha }$ for some $\alpha <\kappa$. A complete type over $A$ consistent with $N$ is finitely satisfiable in $M_{\alpha }$: each finite conjunction is an existential formula with parameters from $M_{\alpha }$, and elementarity transfers its truth from $N$. The complete type is therefore realized in $M_{\alpha +1}$. This provesFor a singular desired degree, apply the theorem at a larger regular cardinal. If $M$ is infinite and an uncountable regular $\kappa$ satisfies ${\kappa }^{<\kappa }=\kappa$, with $|L|<\kappa$ and $|M|\le \kappa$, the construction can keep every stage of size $\kappa$. There are then at most $\kappa$ parameter sets and complete types, and downward Löwenheim-Skolem gives that size after each extension; adding $\kappa$ distinct elements initially ensures final size exactly $\kappa$. The resulting model is saturated in the unqualified sense. The cardinal-arithmetic hypothesis belongs to this size refinement, not to the general existence theorem.

An explicit ultraproduct version is useful too. In a countable language let $U$ be a nonprincipal ultrafilter on $\omega$ and $N={\prod }_{i<\omega }{M}_i/U$, where each factor is nonempty. Enumerate a countable finitely satisfiable complete type, including its chosen parameter representatives, as ${\phi }_1(x),{\phi }_2(x),\dots$. By the Łoś theorem, the set $A_n$ of coordinates where the first $n$ formulas have a simultaneous witness belongs to $U$. PutThese are decreasing members of $U$. At coordinate $i$, let $k(i)$ be the greatest $n\le i$ with $i\in B_n$, if there is one. Choose a witness to the first $k(i)$ formulas there, and an arbitrary element when there is none. For fixed $n$, every coordinate in $B_n$ has $k(i)\ge n$, so the chosen function satisfies ${\phi }_n$ on a $U$-large set. Its ultraproduct class realizes the whole complete type. A countable language over a countable parameter set has only countably many formulas, so this proves countable saturation of a nonprincipal ultraproduct over omega.

For NFU, we give the rank-indiscernible construction of an NFU model explicitly. NFU has a unary predicate $S$ for sets, atoms have no members, extensionality applies to sets, and comprehension applies to every stratified formula. A stratification assigns integer types to variables so that equality uses equal types and $x\in y$ requires $\mathrm{type}(y)=\mathrm{type}(x)+1$. A unary set predicate adds no type difference.

Start with the actual set structure $B=(V_{\omega +\omega },\in )$. This structure satisfies extensionality and every pure-membership separation instance: the subset defined in a set $a$ of rank below $\omega +\omega$ still has rank below $\omega +\omega$. We do not assert that $B$ satisfies replacement or all of ZFC. Expand it by Skolem functions. In it use the sequence of rank objects $V_{\omega +n+6}$, $n<\omega$. For two such objects $d<e$ in sequence order, we havewith quantifiers in $B$. The second statement holds because every subset of $V_{\alpha }$ belongs to $V_{\alpha +1}$, and the later rank is at least $\alpha +1$.

Introduce constants $d_i$, $i\in \mathbb{Z}$, and require them to be order indiscernibles in the Skolem language, satisfying these two assertions whenever $i<j$. Also require $V_{\omega +5}\subseteq d_i$ for every $i$; this fixed rank object is first-order definable in $B$. Every finite part of these requirements together with $\mathrm{Th}(B^{\ast })$ is satisfiable: color finite increasing tuples of the original rank sequence by the truth values of the finitely many formulas mentioned, and use Ramsey's theorem to get a homogeneous subsequence. The rank assertions hold for every increasing tuple there. The compactness theorem gives a model of the full theory. In its Skolem hull $N$ generated by the $d_i$, the integer shift extends to an automorphism $j$ with $j(d_i)=d_{i+1}$, by the term-transport proof of the Ehrenfeucht-Mostowski theorem. Thus $N$ still satisfies extensionality and all pure-membership separation instances, andThis is a set-sized first-order model; no satisfaction predicate for a proper-class universe is being assumed.

Externally let $D_i=\{x\in N:N\models x\in d_i\}$. The automorphism bijects $D_i$ onto $D_{i+1}$. Interpret a typed structure with sort $i$ equal to $D_i$. At sort $i+1$, declare $y$ a set exactly when $N\models y\subseteq d_i$; otherwise it is an atom. Define adjacent-sort membership byThe guard is necessary: a typed atom might have some ordinary $N$-members in $D_i$, and those must not become its typed members. Set-extensionality follows from extensionality in $N$, because the ordinary members of a typed set all lie in $D_i$. For any typed formula on sort $i$, its quantifiers can be restricted to the corresponding $d_l$, its set predicates replaced by subset assertions, and its memberships replaced by the guarded relation. This is an ordinary pure-membership formula of $N$ with finitely many parameters. Separation gives its extension $X\subseteq d_i$, and the displayed closure assertion gives $X\in d_{i+1}$. It is therefore a typed set witnessing comprehension. The automorphism shifts these sorted domains and preserves the set flags and guarded memberships.

Collapse the types onto $D_0$. DefineObjects not satisfying $S$ have no $E$-members. If two sets have the same $E$-members, their images under $j$ are subsets of $d_0$ with the same ordinary members, so are equal by extensionality of $N$; injectivity of $j$ gives equality of the original objects.

To verify every stratified comprehension instance, assign a variable $v$ its stratification type $t(v)$ and translate its value $a\in D_0$ to $j^{t(v)}(a)\in D_{t(v)}$. Equality is preserved. An atomic $E(x,y)$ translates to the guarded adjacent-sort membership because $t(y)=t(x)+1$; the unary predicate $S(y)$ translates to $j^{t(y)}(y)\subseteq d_{t(y)-1}$. Induction on formulas, using the domain bijections for quantifiers, preserves truth. If the free variable $x$ has type $t$, typed comprehension produces its extension $X\subseteq d_t$, with $X\in d_{t+1}$. Put $b=j^{-(t+1)}(X)\in D_0$. Then $S(b)$ holds, and for every $a\in D_0$,This is exactly the required NFU set. No formula containing the external automorphism $j$ has been used in a separation or comprehension scheme; $j$ only transports values after the pure formula is formed.

The construction also permits the usual infinity requirement. The ordinary $\omega$ and its successor graph $f$ are definable in $N$, hence fixed by $j$, and lie below $V_{\omega +5}$, so belong to all the required domains. Under $E$, the members of $\omega$ are still its ordinary $N$-members. The new Kuratowski pair satisfiesSince $j(f)=f$, membership of this pair in $f$ under $E$ is equivalent to $⟨x,y{⟩}_N\in f$. Thus $f$ is an internal injection of $\omega$ into itself omitting zero, giving a Dedekind-infinite set.

We have built a model of NFU, with infinity if it is included in the formulation, in ordinary ZFC metatheory:In particular $\mathrm{Con}(\mathrm{ZFC})\Rightarrow \mathrm{Con}(\mathrm{NFU})$. This proof does not assume $\mathrm{Con}(\mathrm{ZFC})$ as an additional internal axiom: its starting structure is the set $V_{\omega +\omega }$, not a model of ZFC.

A useful form of the Ehrenfeucht-Mostowski theorem says that, for an infinite first-order structure $M$ and any total order $I$, there is a model of $\mathrm{Th}(M)$ generated as a Skolem hull by distinct order indiscernibles $(a_i{)}_{i\in I}$. Every order automorphism of $I$ extends uniquely to an automorphism of the specified Skolem expansion of that hull. The model can be obtained inside an elementary extension of a Skolem expansion of $M$; the generated hull itself need not contain $M$.

Choose a Skolem expansion $M^{\ast }$ by iteratively adjoining witness functions: for each existential formula in the current language choose a function returning a witness whenever one exists, with an arbitrary value otherwise. Repeat for countably many rounds. Every formula in the final language uses finitely many symbols, so has a witness function from a later round. Thus the expansion is Skolemized for its own formulas, as required for elementarity of its hull. Add constants $a_i$ for $i\in I$ to the complete theory of $M^{\ast }$, require them to be distinct, and impose the schemefor every formula in the Skolem language. If an elementary extension of $M^{\ast }$ is desired, also add its elementary diagram with separate names for its elements.

Every finite part of this theory is satisfiable. Choose infinitely many distinct elements $b_0,b_1,\dots$ of $M$. For each of the finitely many arities in that fragment, color increasing index tuples by the finite vector of truth values of the formulas occurring. Repeated applications of the infinite Ramsey theorem give an infinite subset on which all these vectors are constant. Interpret the finitely many $a_i$ in increasing-index order from that subset. This satisfies the finite indiscernibility requirements and distinctness, while the elementary diagram is satisfied by the named original structure. The compactness theorem gives a structure $N^{\ast }$ satisfying the whole theory.

Let $H$ be the closure of the $a_i$ under the Skolem functions, including nullary ones. It is elementary in $N^{\ast }$: whenever an existential formula with parameters from $H$ is true in $N^{\ast }$, its Skolem witness lies in $H$. This is the Tarski-Vaught test, whose proof is induction on formulas, using precisely this witness property for the existential step. Hence the reduct of $H$ is a model of $\mathrm{Th}(M)$.

For an order automorphism $\sigma :I\to I$, defineThis is well-defined. If two terms denote the same element, write their equality as a formula on the combined increasing tuple of their indices; indiscernibility preserves that formula after transport by $\sigma$. The same argument preserves every relation and function. Applying ${\sigma }^{-1}$ gives the inverse, so $\hat{\sigma }$ is an automorphism. Since all elements are terms in the generators, it is the unique automorphism of this Skolem expansion extending $a_i\mapsto a_{\sigma (i)}$. This proves the theorem.

One may require the indiscernibles to lie in any specified infinite sequence of the starting structure, or to satisfy additional finite-tuple properties holding along that sequence: the same finite satisfiability proof chooses its homogeneous subsequence there. This strengthened form is what the rank-domain construction of NFU uses. Uniqueness is asserted in the Skolem expansion, not for all automorphisms of its reduct.

For finite rooted trees, use rooted-tree homeomorphic embedding: an injective vertex map preserves ancestors and lowest common ancestors, so edges may become paths and distinct branches remain distinct. The root can map to a vertex below the host root. More generally label vertices in a well-quasi-ordering $Q$ and require each source label to precede its image label. We prove this stronger labelled version of Kruskal's tree theorem, from which the unlabelled result follows by taking one label.

We first need the finite-word closure, and prove it rather than merely invoking Higman lemma. If finite words over $Q$ were not a well-quasi-ordering under order-preserving subsequence embedding with increased labels, choose a minimal bad sequence $w_0,w_1,\dots$, minimizing the length of $w_n$ among words admitting a bad continuation of the already chosen prefix. No $w_n$ is empty. Write $w_n=v_n{a}_n$ by removing its last letter. The perfect subsequence lemma gives $n_0<n_1<\cdots$ with $a_{n_r}\le a_{n_s}$ for $r<s$.

The sequence $w_0,\dots ,w_{n_0-1},v_{n_0},v_{n_1},\dots$ is still bad. An earlier $w_i$ embedding into a later $v_{n_r}$ would embed into $w_{n_r}$, contradicting the original sequence. An embedding of $v_{n_r}$ into $v_{n_s}$ extends by the last-letter comparison to an embedding of $w_{n_r}$ into $w_{n_s}$. Both possibilities are excluded. This contradicts minimality at position $n_0$, since $v_{n_0}$ is shorter. Thus the finite-word closure holds. The perfect subsequence lemma also proves finite product closure: first pass to a nondecreasing subsequence in one coordinate, then in the next, preserving all previous comparisons.

Suppose now that the labelled trees admit a bad sequence $T_0,T_1,\dots$. Choose a minimal bad sequence by vertex number. Let $\mathcal{U}$ be all the proper descendant-rooted subtrees of these trees. We claim that $\mathcal{U}$ is a well-quasi-ordering. If it had a bad sequence of subtrees $U_r$, its parent indices can be made strictly increasing, say $U_r$ comes from $T_{n_r}$. Indeed each finite initial collection of parent trees has only finitely many subtrees, and a bad sequence cannot contain infinitely many terms from a finite collection. Passing to a subsequence therefore makes $n_0<n_1<\cdots$.

Then $T_0,\dots ,T_{n_0-1},U_0,U_1,\dots$ is bad. A prefix tree embedding into $U_r$ would embed into its parent $T_{n_r}$, contrary to the original badness, and the tail is bad by construction. But $U_0$ has fewer vertices than $T_{n_0}$, contradicting minimality. This proves the claim.

Give the children of each root any fixed order. Its forest of child subtrees is a finite word in $\mathcal{U}$. The word theorem and finite product closure show that the pairs consisting of the root label and the child-subtree word are a well-quasi-ordering. Thus some $i<j$ have comparable root labels and an embedding of the child word of $T_i$ into that of $T_j$. Map the source root to the target root and use the obtained embeddings inside distinct target child subtrees. The paths from the target root into those distinct branches are disjoint except at the root, so this is a label-monotone tree embedding. It contradicts badness. Hence

For Friedman's finite form of Kruskal's theorem, fix $k\in \mathbb{N}$. There is $N(k)$ such that any $N(k)$ trees with $|T_i|\le k+i$ contain $i<j$ with $T_i⪯T_j$. Use indices starting at zero; shifting them only changes $k$. To prove this uniform finite bound, form the finite bad-sequence tree of finite bad prefixes obeying the size bounds. At position $i$ there are only finitely many rooted-tree isomorphism types with at most $k+i$ vertices, so every node has finitely many successors.

If no bound existed, this tree would have nodes of arbitrarily large depth. A node with arbitrarily long extensions has a child with arbitrarily long extensions, since it has only finitely many children. Choosing such a child repeatedly produces an infinite branch, as in the König infinity lemma. The branch is an infinite bad tree sequence, contradicting the theorem just proved. Therefore the required $N(k)$ exists. The same proof works with any fixed finite label alphabet and any specified size bound finite at each position.

A well-quasi-ordering is a preorder $(Q,\le )$ such that every infinite sequence $(x_n)$ has indices $i<j$ with $x_i\le x_j$. Reflexivity and transitivity are part of the definition; antisymmetry is unnecessary. An infinite sequence without such a pair is a bad sequence.

The perfect subsequence lemma strengthens this definition: every infinite sequence in a well-quasi-order has an infinite nondecreasing subsequence, meaningHere is a proof that does not assume the lemma implicitly. There must be an index $i$ with infinitely many later indices $j$ satisfying $x_i\le x_j$. Otherwise each index would have only finitely many such successors. Starting with any index, choose the next one beyond the union of those finite successor sets for the previously chosen indices. This constructs a bad sequence, contradicting the well-quasi-ordering property.

Choose $i_0$ with infinitely many successors above it, and restrict to those successors. Apply the same argument to that infinite subsequence, obtaining $i_1>i_0$ with infinitely many later successors above it within the restricted sequence. Continue. Every subsequent restriction lies inside all previous upper cones, so $x_{i_r}\le x_{i_s}$ for every $r<s$. This proves the lemma, including for a genuine quasi-order with distinct equivalent elements. Both alternatives below use it.

Use the rooted-tree homeomorphic embedding relation: an injective map of vertices preserves lowest common ancestors, so edges may become paths and the source root may map below the target root. We prove the stronger labelled statement for labels in any well-quasi-ordering $Q$, with labels increasing under the embedding. Forgetting labels gives Kruskal's tree theorem.

First every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence. Colour its index pairs according as the earlier term is or is not below the later term. Ramsey's theorem gives an infinite constant-colour subsequence; the bad colour would contradict well-quasi-ordering. Applying this successively in each coordinate proves finite product closure of well-quasi-orderings.

We need Higman lemma with its proof. Order finite words over $Q$ by subsequence embedding with increased letters. If there were a bad sequence, choose one $w_0,w_1,\dots$ minimally: at each position choose a shortest word admitting a bad continuation of the fixed prefix. No word is empty. Write $w_n=u_n{a}_n$, separating the last letter, and choose $n_0<n_1<\cdots$ with $a_{n_0}\le a_{n_1}\le \cdots$. ConsiderAn earlier prefix word cannot embed in a later $u_{n_j}$, since it would then embed in $w_{n_j}$. Nor can $u_{n_i}$ embed in $u_{n_j}$: adding the comparable last letters would embed $w_{n_i}$ in $w_{n_j}$. Thus the displayed sequence is bad, contradicting minimality at $n_0$, since $u_{n_0}$ is shorter. Finite words over a well-quasi-order are well-quasi-ordered.

Now suppose labelled rooted trees admit a bad sequence $T_0,T_1,\dots$, chosen minimally in vertex count at each position. Let $\mathcal{A}$ consist of all proper rooted subtrees of these trees, rooted at a descendant and containing all its descendants. We claim $\mathcal{A}$ is well-quasi-ordered. Otherwise take a bad sequence $S_0,S_1,\dots$ from $\mathcal{A}$. Only finitely many subtrees come from any fixed finite prefix of the $T_n$'s, and a bad sequence cannot repeat an object. Thin it so that $S_i$ comes from $T_{m_i}$ with $m_0<m_1<\cdots$. The sequenceis bad: $T_j⪯S_i$ would imply $T_j⪯T_{m_i}$, since a rooted subtree embeds in its host; comparisons within the $S_i$'s are excluded by their choice. But $S_0$ is strictly smaller than $T_{m_0}$, contradicting minimality. This proves the claim.

Choose an arbitrary ordering of the children of each $T_n$. Record its root label and the finite word of rooted child-subtrees:By Higman lemma and finite product closure, two records, with indices $i<j$, are comparable. Map the root of $T_i$ to the root of $T_j$, and map its selected child-subtrees into the distinct selected branches of $T_j$. Within a branch the embeddings preserve lowest common ancestors; between different branches both lowest common ancestors are the roots. Labels increase everywhere. This gives $T_i{⪯}_Q{T}_j$, contradicting badness. Finite labelled rooted trees are well-quasi-ordered by label-monotone homeomorphic embedding. In particular, this proves the unlabelled theorem. A root-preserving variant follows by giving the root a special incomparable label unavailable at nonroot vertices; the general labelled theorem then forces root to root. Adjacency-preserving embeddings are a different, more restrictive relation and do not satisfy the same assertion.

For Friedman's finite form of Kruskal's theorem, fix $k\in \mathbb{N}$ and consider finite bad sequences satisfying $|T_i|\le k+i$, with indices starting at $1$. Their prefixes form a finite bad-sequence tree. At each depth there are only finitely many possible unlabelled tree isomorphism types below the size bound, so this tree is finitely branching. If bad sequences existed at every finite length, König infinity lemma would yield an infinite branch, hence an infinite bad sequence of rooted trees, contrary to what was just proved. ThereforeThe same proof works with any fixed finite label set. The finite size bounds are what make the bad-prefix tree finitely branching; the proof does not claim a small effective numerical bound.

A harmonic function on $\Omega$ is a twice continuously differentiable function satisfying $\Delta u=0$ there. For complex-valued functions this means that both its real part and its imaginary part are harmonic functions. The mean value property for harmonic functions characterizes harmonicity: a continuous function is harmonic exactly when its value at each point equals its average over every sphere, or equivalently every ball, whose closed ball lies in $\Omega$. In the forward direction, the derivative of the spherical average vanishes by the divergence theorem. Conversely, radial smoothing leaves a continuous function with the mean value property unchanged locally; it is therefore smooth. Expanding its small-ball average gives $u(x)+r^2\Delta u(x)/(2(d+3))+o(r^2)$ in dimension $d+1$, and hence $\Delta u=0$.

Write $M=\Vert u{\Vert }_{h^1}$ and $v_{d+1}$ for the volume of the unit ball in ${\mathbb{R}}^{d+1}$. We first obtain a pointwise estimate directly from the mean value property for harmonic functions, before using any boundary representation. For the ball of radius $r=t/2$ centered at $(x,t)$,Thus every upward shift of $u$ is a bounded harmonic function, with a continuous bounded boundary value.

The required map is the Poisson integralThe Poisson kernel for the upper half-space is positive, has integral one, and is harmonic as a function of $(x,t)$. Its normalization follows by polar coordinates and $r=\tan \theta$, which reduces the radial integral to ${\int }_0^{\pi /2}{\sin }^{d-1}\theta d\theta$; direct differentiation gives ${\Delta }_{x,t}{P}_t=0$. Differentiation under the integral on compact subsets proves that $P\mu$ is a harmonic function. Tonelli theorem givesHere the total variation norm of a measure is the norm on finite signed or complex Borel measures.

The Poisson kernel for the upper half-space is an approximate identity: for $\psi \in C_0({\mathbb{R}}^d)$, $P_t\ast \psi \to \psi$ uniformly. Indeed, uniform continuity controls translations smaller than a fixed radius, and the kernel mass outside that radius tends to zero. ConsequentlyThe dual characterization of the total variation norm of a measure, as the supremum over $\psi \in C_0$ of supremum norm at most one, now gives the reverse inequality $\Vert \mu {\Vert }_{\mathrm{TV}}\le \Vert P\mu {\Vert }_{h^1}$. Thus $P$ is a linear isometry and is injective.

For surjectivity, fix $s>0$ and put $u_s(x)=u(x,s)$. Bounded harmonic uniqueness in the upper half-space givesTo justify this uniqueness, subtract the Poisson integral of the bounded continuous boundary value from the upward-shifted harmonic function. Their difference is bounded and harmonic and has zero continuous boundary values. Its odd reflection across the boundary is an entire bounded harmonic function; the reflection is harmonic across the flat boundary by harmonic odd reflection across a hyperplane. The Liouville theorem for harmonic functions makes it constant, and oddness makes it zero. The initial pointwise estimate supplies the boundedness needed here. To see the reflection locally, take a ball centered on the hyperplane and extend the boundary data on its upper hemisphere oddly to its lower hemisphere. The harmonic solution on this ball is odd and zero on its equatorial disk. The maximum principle for harmonic functions identifies it with the given difference on the upper half-ball, proving that the reflected function is harmonic across the boundary.

Choose $s_j\downarrow 0$. The measures $u_{s_j}dx$ have total variation norm of a measure at most $M$. By the Banach-Alaoglu theorem, and separability of $C_0({\mathbb{R}}^d)$, a subsequence converges in the weak-star topology to a finite measure $\mu$ with $\Vert \mu {\Vert }_{\mathrm{TV}}\le M$. For fixed $(x,t)$ and $s_j<t$,The kernels in this display belong to $C_0$ and converge uniformly to $P_t(x-\cdot )$. The uniform measure norm bound therefore allows passage to the limit, giving $u(x,t)=P\mu (x,t)$. This proves the Poisson representation of harmonic h1 by finite measures, including onto-ness.

Finally $P_t(x)\le c_d{t}^{-d}$, so the Poisson representation of harmonic h1 by finite measures improves the preliminary pointwise constant:The last occurrence of $h^1({\mathbb{R}}^{d+1})$ in the printed question is understood as the harmonic Hardy space of the upper half-space defined earlier in that question.

A real sequence has limit $a\in \mathbb{R}$ if, for every $\epsilon >0$, there is $N$ such that $|a_n-a|<\epsilon$ for all $n\ge N$. It tends to $+\infty$ if, for every real $M$, eventually $a_n>M$; it tends to $-\infty$ if eventually $a_n<M$ for every real $M$.

The Bolzano-Weierstrass theorem states that every bounded sequence of real numbers has a real convergent subsequence. This proves the claim for bounded sequences. If the sequence is unbounded above, every tail remains unbounded above because a finite prefix is bounded. Choose indices $n_j$ increasing with $a_{n_j}>j$. This subsequence tends to $+\infty$. If it is unbounded below, choose $a_{n_j}<-j$ to obtain a subsequence tending to $-\infty$. This proves the extended real subsequence theorem.

For the final example, a bounded sequence with vanishing increments need not converge. TakeThe mean value theorem givesNevertheless, along $n_j=\lfloor (\pi /2+2\pi j{)}^2\rfloor$, the square-root rounding error tends to zero, so $a_{n_j}\to 1$. Along $m_j=\lfloor (3\pi /2+2\pi j{)}^2\rfloor$, it tends to $-1$. These two subsequences have different limits, proving nonconvergence.

Use rooted-tree homeomorphic embedding: edges may be stretched into downward paths, different child branches stay disjoint, and the source root may map to any target vertex. Write $S⪯T$ for this relation. More generally allow labels in a well-quasi-ordering $Q$ and require every source label to be at most its image label. We prove this labelled version, which includes the unlabelled case by taking one label.

First, every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence. In every infinite set of indices there is an index with infinitely many later successors above its value. Otherwise repeatedly discard the finitely many successors of each chosen index, obtaining a bad sequence. Applying this observation successively within the infinite successor set produces the required subsequence.

We also need the Higman lemma, and prove it here. If finite words over $Q$ admitted a bad sequence, choose one $w_0,w_1,\dots$ with each word of least possible length among choices permitting a bad continuation of its fixed prefix. No word is empty. Write $w_i=v_i{a}_i$, and extract indices $n_0<n_1<\cdots$ with $a_{n_0}\le a_{n_1}\le \cdots$. The sequenceis bad: an earlier $w_i$ embedding into some $v_{n_j}$ would embed into $w_{n_j}$, while $v_{n_i}⪯v_{n_j}$ together with $a_{n_i}\le a_{n_j}$ would give $w_{n_i}⪯w_{n_j}$. This contradicts the minimal length of $w_{n_0}$, since $v_{n_0}$ is shorter. Hence finite words are well-quasi-ordered under subsequence embedding with increased labels.

Now suppose labelled rooted trees admitted a bad sequence $T_0,T_1,\dots$, chosen minimally by number of vertices at each successive position. Let $B$ consist of all immediate child subtrees of all the $T_i$, with the inherited labels. We claim $B$ is a well-quasi-ordering. Otherwise take a bad sequence of members of $B$. Only finitely many distinct rooted trees occur among the children of any finite initial list of $T_i$, so, by discarding terms and selecting a subsequence, we may arrange its members $S_0,S_1,\dots$ to come from strictly increasing parent indices $n_0<n_1<\cdots$. Thenis bad. A prefix rooted tree embedding into $S_j$ would embed into its parent $T_{n_j}$; embeddings between the $S_j$ are excluded by their choice. But $S_0$ has fewer vertices than $T_{n_0}$, contradicting minimality. This proves the claim.

List the child subtrees of each $T_i$ in any order. By the Higman lemma these child lists are well-quasi-ordered. Extract an infinite subsequence with nondecreasing root labels, and then compare two child lists on that subsequence. Their subsequence embedding gives distinct target child branches into which the source child subtrees embed. Map the source root to the target root and join each embedded child root to it by the corresponding downward path. The paths are disjoint except at the root, and labels increase. Thus $T_i⪯T_j$ for some $i<j$, contradicting badness. This proves Kruskal's tree theorem and its labelled version. If root preservation is required, mark the root with a special label incomparable with all ordinary labels; the same proof then forces root to map to root.

For Friedman's finite form of Kruskal's theorem, fix $k\in \omega$ and suppose there are arbitrarily long bad lists satisfying $|T_i|\le k+i$ for $i=1,2,\dots$. Make a finite bad-sequence tree whose nodes are these lists, using one representative of each finite rooted-rooted tree isomorphism type. At each position only finitely many choices satisfy the size bound, so the rooted tree is finitely branching. An infinite path exists: at every stage choose a child having extensions of arbitrarily large length, which must exist because there are finitely many children. The path is an infinite bad sequence, contradicting Kruskal's tree theorem. ThereforeThe identical argument works with finitely many labels and any fixed finite size bound at each position.