A well-quasi-ordering is a reflexive transitive relation for which every infinite sequence has with . A bad sequence has no such pair. The labelled version of Kruskal's tree theorem says that finite rooted trees labelled in any well-quasi-ordering are themselves well-quasi-ordered by label-monotone tree embedding.
More explicitly, an embedding is an injective map of vertices preserving lowest common ancestors, and satisfying at every vertex. The root need not map to the host root. This is a homeomorphic embedding of a rooted tree: an edge can map to a longer path, but distinct branches must separate at the image of their common ancestor. We shall prove the stronger version in which every vertex's children are linearly ordered and embeddings respect that ordering. Forgetting the child order gives the stated result for unordered rooted trees.
We first establish the two well-quasi-ordering facts used in the proof. Every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence. Indeed, color an index pair according to whether . The infinite two-color Ramsey theorem gives a homogeneous infinite set; the negative color would be a bad sequence, so the positive color gives the required subsequence. It follows that the componentwise product of two well-quasi-orderings is a well-quasi-ordering: first extract a nondecreasing subsequence in one coordinate, then find a good pair in the other.
Next prove Higman lemma: finite words over a well-quasi-ordering , ordered by subsequence embedding with coordinatewise increase of letters, are a well-quasi-ordering. Suppose not, and choose a minimal bad sequence by making the length of minimal among all choices admitting an infinite bad continuation of the already fixed prefix. No word is the empty word, since that embeds in every later word. Write with . Extract indices for which . Consider
It cannot be a bad sequence, since its first replacement is shorter than the minimal choice . But a good pair within the original prefix is impossible. A prefix word embedding into would embed into , contradicting the original bad sequence. And embedding into would, after appending the ordered last letters, embed into , also impossible. This contradiction proves Higman lemma, including words of arbitrary finite length.
Now suppose there is a bad sequence of finite ordered labelled rooted trees. Choose a minimal bad sequence by minimizing the number of vertices of , subject to the fixed prefix having an infinite bad continuation. Existence of a least possible size uses ordinary well-ordering of the natural numbers; after selecting such a tree retain a bad continuation to make the next choice.
Let be the collection of all proper rooted subtrees of all , with inherited labels and child ordering. These are the subtrees rooted at vertices other than the root, and each embeds into its containing tree. We claim is a well-quasi-ordering under the same label-monotone tree embedding.
Otherwise choose a bad sequence from , and choose for each a containing tree . The indices are unbounded in every tail: finitely many containing trees have only finitely many rooted subtrees, and an infinite bad sequence cannot repeatedly use one of these, since it embeds into itself. Passing to a subsequence, arrange . The spliced sequence
is bad. A good pair within either piece is already excluded. A comparison , where , would compose with to give , contradicting the original bad sequence. But is smaller than , contradicting the minimal choice at that position. This proves the claim about .
Describe by its root label and its finite ordered list of child subtrees. Every entry of lies in . By Higman lemma, is a well-quasi-ordering; hence so is . There exist with and an increasing injection matching the child subtrees in to child subtrees in , each by an embedding. Map root to root and combine these child embeddings. Different matched children lie in different target branches, so their paths meet exactly at the target root; within each branch the chosen embedding already preserves lowest common ancestors. The resulting map is a label-monotone tree embedding , a contradiction. Therefore
The empty labelled tree, if included by convention, embeds into every tree and causes no exception. A common stronger formulation requires the source root to map to the target root. It also follows: the theorem just proved makes all labelled child subtrees a well-quasi-ordering, and the product then provides a good pair with roots explicitly matched, by the same final assembly. Internal child roots may map further down their matched branches. This must not be confused with edge-to-edge embedding, for which the theorem is false in general.
One form of the Ehrenfeucht-Mostowski theorem says that, for every infinite first-order structure and every total order , an elementary extension contains distinct elements forming an order-indiscernible sequence. After a suitable Skolem expansion, their Skolem hull is a first-order model of , and every order automorphism of extends to a structure automorphism of that hull. If has a definable infinite linearly ordered subset , the generators may lie in and their order may agree with that definable order. Uniqueness of the extended structure automorphism is asserted in the chosen Skolem expansion, rather than for every structure automorphism of its reduct.
Here is an ultraproduct proof of the Ehrenfeucht-Mostowski theorem. First expand to with Skolem functions for all existential first-order formulas, iterating through the enlarged languages if necessary. This is done in the ordinary classical metatheory; the choice restriction in question 1 is not a restriction on this question. Fix a nonprincipal ultrafilter on .
We can obtain an infinite sequence of distinct elements in an elementary extension of by one preliminary ultrapower. For each choose a finite list of distinct elements of . Represent by the function taking the th entry when , with an arbitrary default otherwise. Distinctness holds on a cofinite set, so follows from Łoś theorem. In the definably ordered variant, first name any parameters defining , and choose each finite list increasingly inside instead; then and for . Infinitude of an ordered set supplies every finite increasing chain. This preparatory step uses no Ramsey theorem.
For a finite subset of , define the ultrafilter on by nested membership, in this order:
where means . This is the ordered Fubini product of ultrafilters. Closure under intersections and the decision between a set and its complement hold at each nested level, proving it is an ultrafilter. For take the principal ultrafilter on the one-point product. Put
If , pull a function back along the projection . A test independent of an omitted coordinate is unchanged by its ultrafilter quantifier, so projection pushes to . The induced map is therefore an elementary embedding by Łoś theorem. These maps are coherent, giving a directed system indexed by finite subsets of .
Take its directed limit of elementary embeddings . One can verify elementarity directly: representatives of a finite tuple occur at a common stage; functions and atomic relations are interpreted there. In the existential step, a witness in the limit occurs with the parameters at some later common stage, and elementarity pulls the existence statement back. Thus every embeds elementarily into , which contains an elementary copy of .
For , let be the class of the coordinate function . Projection coherence makes this independent of . If , then for each fixed the set is cofinite. The nested test therefore gives . In the ordered variant, the same argument with gives and .
For every first-order formula of the expanded language and every increasing tuple , Łoś theorem gives
The right-hand side depends on the first-order formula and tuple length, not on the indices. This proves order indiscernibility in the expanded language. Let be the Skolem hull of the generators in . The Tarski-Vaught test gives , and its reduct is a first-order model of .
An order automorphism of acts by
Indiscernibility makes this well defined: combine the finite supports of two term expressions into one increasing tuple, and apply indiscernibility to their logical equality. Applying it to relation first-order formulas proves preservation of all relations; the inverse is induced by . Every element of the hull is such a term, so the extension is unique among structure automorphisms preserving the Skolem expansion. Moreover
This proves the theorem, including its ordered version and structure automorphism conclusion, using ultrapowers and a directed limit throughout.
The Canonical Ramsey theorem says that for every map , with no restriction on the colour set , there are an infinite set and such that, for increasing tuples from ,
To prove it, define an equivalence relation on by equality of colours. Two ordered pairs of -sets have one of finitely many intersection-order types. Successively apply the infinite Ramsey theorem to obtain an infinite on which, for each type, equivalence has a constant truth value. Let consist of those coordinates whose replacement, with all other coordinates fixed and order preserved, changes the equivalence class. Homogeneity of the pair types shows first that this does not depend on the chosen tuple. Changing coordinates one at a time then shows that agreement on implies equivalence; reversing the same chain shows that disagreement at a coordinate in implies inequivalence. This gives the displayed canonical form.
For , the four choices of give exactly the constant, minimum, maximum, and injective colourings. Suppose the asserted finite result failed for some . For every choose an equivalence relation on having no canonical -set. These finite bad relations form a finitely branching tree under restriction. König infinity lemma gives an infinite branch, hence a colouring-equivalence relation on with no canonical -set. The canonical theorem supplies an infinite canonical set, whose first vertices give a contradiction. Therefore a suitable finite exists.
Restrict the given finite edge-colouring to the positive integers inside . The infinite Ramsey theorem gives an infinite monochromatic subset; listing it in increasing order produces
Apply the same theorem separately to the negative integers. If the selected indices satisfy , then
forms a monochromatic set with . The two monochromatic colours need not agree.
Let be the vertex set of a regular polygon and let the cyclic rotation group act transitively on it. The finite invariant-colouring lemma says that for every number of colours there are positive weights with such that every colouring of the weighted Cartesian power
contains a monochromatic set
For completeness, prove the lemma along a cyclic composition series for . For a prime cyclic quotient, refine each colour to the finite vector of colours obtained by applying the quotient elements in every active coordinate. The Hales-Jewett theorem supplies a variable block on which this vector is constant. Assign that block squared weights summing to the squared weight of the coordinate it replaces. This makes the quotient orbit monochromatic without changing any orbit distance. Iterating through the cyclic factors proves the lemma for the finite cyclic group .
Because rotations commute, for each coordinate satisfies
for a fixed vertex . Hence the squared distance between the two corresponding product points is
The monochromatic orbit is therefore isometric to . This proves that every regular polygon is a Euclidean Ramsey set.
Now consider the edge-colouring definition. If all pairwise distances in are equal, then is a regular simplex. Take a sufficiently large regular simplex of the same side length. The ordinary finite Ramsey theorem gives a monochromatic -vertex complete subgraph, and every such vertex set is isometric to . Thus is an edge Ramsey set.
Conversely, if has two distances, let and be its least and greatest distances. Colour every Euclidean edge by whether its length equals . Every isometric copy of contains both an edge of length and one of length , so no copy is monochromatic. Hence the edge Ramsey sets are exactly the equidistant finite sets.
Allowing similar copies does not change the answer. If , colour an edge of length by the parity of
In every similar copy, the images of a shortest and a longest edge have lengths and , whose displayed integers differ by one. They receive opposite colours. Thus no non-equidistant is edge Ramsey even up to similarity, while the regular-simplex argument already supplies an isometric copy.
Ramsey theorem follows from : at a vertex, either at least neighbours or at least non-neighbours produce the desired clique or independent set. Induction with gives , hence .