The arrow in the original PDF permits partial functions. A partial computable function is computed by a finite program which halts with the specified value on every input in its domain and diverges on inputs outside the domain. A total computable function is the special case with full domain. Coding finite tuples by a primitive recursive pairing function identifies the different finite arities effectively, without identifying total and partial computability.
One precise machine model is a Turing machine. Its finite transition rules and configurations admit effective numerical coding. Bounded simulation is primitive recursive, and unbounded execution gives the partial result. Equivalently, start from zero, successor and projections and close under composition, primitive recursion and unbounded minimization. The Kleene normal form theorem makes the equivalence concrete:
where is a primitive recursive predicate checking a coded halting computation and reads its output. If no computation exists, the minimum and hence the value are undefined. Checking a finite history is effective because every consecutive configuration must obey one of the finitely many transition rules.
The universal partial computable function evaluates the program indexed by on an input. The S-m-n theorem says that fixing finitely many input parameters can be done by a total computable operation on program Gödel numbers: a new program stores those parameters and calls the original universal evaluator. These facts explain both universal simulation and uniform reductions. A set is computably enumerable when it is the domain of a partial computable function, equivalently the range of an effective enumeration. It is recursive when its characteristic function is total computable. A set is recursive precisely when it and its complement are computably enumerable: dovetail the two enumerations to decide each input.
The diagonal halting problem is computably enumerable but not recursive. A total decider would yield a program which, on , diverges if the decider says and halts otherwise. Applying this program to its own index gives a contradiction. There is likewise no total computable universal listing of all total computable functions: the diagonal function would be total and absent from the listing.
Here is a full proof of the Rice theorem. Let be a nonempty proper class of partial computable functions whose property depends only on the function, not its program. First suppose the everywhere-undefined function is not in , and choose a program for a function . Given an index , construct uniformly a program which on first waits for to halt and, only then, simulates . The S-m-n theorem gives a total computable index map . If , then ; if , then . Thus
A decision procedure for the property would decide , impossible. If , apply the same argument to its nontrivial complement. Every nontrivial extensional property of partial computable functions has an undecidable index set. Totality, having finite domain, and taking a particular value somewhere are examples. A syntactic property such as program length is not covered; nor does the theorem say that no individual program's behaviour can be established.
Self-reference can also be made effective. For a total computable index transformation , let be an index for the program which first computes and then runs the program with that resulting index on its own input. The S-m-n theorem makes total computable. Choose an index for the total function , and put . Then
This proves the recursion theorem: every effective transformation of programs has a fixed point at the level of the function computed, though not necessarily at the level of its numerical code.
Finally, consider the Jockusch triple coloring computing the halting set. Fix computable finite approximations with union . For , define
This is a total recursive two-coloring because both stages are finite computations. Suppose is infinite and homogeneous. Its color cannot be one: fix , wait until every enumeration below has stabilized, and choose later from beyond that stage. Their color is zero.
If has color zero, it computes . On input , use to find and in . For arbitrarily large with , homogeneity gives . Taking stages sufficiently large to reach the final finite approximation gives . Consequently membership of in is decided by the finite stage . A recursive would therefore make recursive, a contradiction. There is a recursive partition of triples with no infinite recursive homogeneous set. This is the nontrivial finite-color meaning of the partition of an infinite domain; if “infinite partition” meant infinitely many colors, the coloring by the least member would already give a trivial example. Ramsey's theorem still guarantees infinite homogeneous sets for the displayed two-coloring, but every such set is computationally nontrivial.
The Rieger-Bernays permutation model changes membership, not the underlying domain. In a model of ZF, let be a definable class bijection, with parameters allowed, and define
Every old set is the new extension of precisely the object . Translation of formulas replaces each membership assertion by this definable relation. Both images and inverse images of old sets under are sets by replacement.
Here are the axiom checks. Extensionality follows because equal new extensions mean and hence . The new empty set is and the new pair is . For an object , new union and power set have representatives
These formulas verify the actual new membership conditions. A definable subset of the new extension is an old set by separation after translation, and its representative gives new separation. Similarly, a functional new formula on that extension has an old set as range by replacement; apply to its range. For infinity, iterate the new successor operation
starting from the new empty set. Old recursion and replacement collect its finite iterates into a set , and is a new inductive set. Thus all axioms of ZF except possibly foundation hold.
Now swap the old objects and and fix everything else. The old object then satisfies , and its entire new extension is . It is a Quine atom, so foundation fails. Taking to be the identity gives the original model where foundation holds. Foundation is independent of the other ZF axioms, relative to consistency of ZF.
A full permutation of a model of choice does not destroy choice. Given a new family of nonempty new sets, old choice selects an element of each old extension ; replacement converts its graph into new ordered-pair coding. Thus simply repeating the preceding unrestricted permutation construction would not prove independence of choice. The extension needed is the hereditarily finite-supported Quine-atom model.
Start with a model of ZFC and simultaneously swap with for all . These transpositions have disjoint supports: none of these infinite ordinals is a singleton, and the ordinals and their singletons are separately distinct. Put , whose members now have new extensions . Build the universe over these Quine atoms by allowing arbitrary new sets of previously constructed objects at each successor stage, and taking unions at limit stages. More explicitly, begin with , put
and take the union over all ordinals. The singleton with sole member is already , as extensionality requires; it is not added as a different atom or set. Every other object's membership has a well-founded construction rank once these designated atomic self-loops are treated as rank-zero leaves.
Every permutation of extends to an automorphism of this universe: on atoms use , and on every non-atomic object recurse by
The inverse permutation gives its inverse, and the formula preserves . Call an object supported by a finite when every permutation fixing pointwise fixes that object. Retain only objects which are supported and all of whose members are hereditarily supported; the recursion here again stops at atoms, whose support is their singleton. Denote this class by .
We verify that is a model of ZF without foundation. It is membership-closed and hence retains extensionality. Pairing uses the union of the two parameter supports, and union uses the support of its input. For separation, use the finite union of the supports of the domain and all parameters: permutations fixing them preserve satisfaction in , so they fix the defined subset. Every member remains hereditary. For replacement, the same support fixes the image of a definable functional relation; its elements already lie in by the internal range condition, and old replacement supplies the underlying set of them. These assertions are legitimate class translations because construction ranks, supports and hereditary support are definable in the starting model.
For power set, start with the set of all new subsets of a supported set and retain exactly those lying in . The resulting collection is fixed by every permutation fixing the original set's support: the action preserves hereditary support and permutes its subsets. Every retained member is hereditary, so this is the internal power set. The empty set and the pure finite and infinite natural-number hierarchy have empty support, yielding infinity. The new pairing, union and comprehension representatives discussed above therefore remain inside . Foundation still fails because all the Quine atoms are in .
The set itself has empty support and hereditary members. So does the family of its two-element subsets, each of which has a finite support in a permutation action. If this family had a choice function , let be a finite support in a permutation action of , and choose distinct . The transposition of fixes and the unordered pair , but interchanges either possible chosen value . It cannot fix the function graph, contradicting its support. Thus choice fails in .
The unrestricted permutation model over the same initial ZFC model satisfies choice and fails foundation, whereas its hereditarily supported submodel fails both. Hence choice is independent of ZF with foundation omitted. These are relative-consistency constructions, not an assertion that ZF proves its own consistency. Starting with ZFC is harmless for the usual consistency comparison with ZF, by the constructible-universe relative-consistency theorem.
A well-quasi-ordering is a preorder in which every infinite sequence has with . A sequence without such a pair is a bad sequence. We use rooted-tree homeomorphic embedding: an injective map of vertices preserving lowest common ancestors, so edges may become paths and a source root may map below the host root. Labels, when present, must increase in their label preorder. This convention is important; adjacency-preserving embeddings do not give the same theorem.
We first prove the auxiliary Higman lemma. If is a well-quasi-order, its finite words are well-quasi-ordered by subsequence embedding with increased letters. Suppose not, and choose a minimal bad sequence of words: at each position choose one of least length among those permitting a bad continuation of the preceding prefix. No word is empty. Write by deleting its last letter. A well-quasi-order has an infinite nondecreasing subsequence of any sequence: if no member of an infinite subsequence had infinitely many later upper bounds within it, one could recursively avoid the finitely many upper bounds of earlier choices and construct a bad sequence. Choose a member with infinitely many later upper bounds, restrict to those bounds and repeat. Apply this to get .
The sequence is still bad. An earlier prefix word embedding into a would embed into , contrary to the original bad sequence. An embedding would extend by the comparable last letters to , equally impossible. But its next word at position is strictly shorter than , contradicting minimality. This proves Higman's lemma, including the possibility that a deleted word is empty, since that would make the proposed bad continuation impossible immediately.
We now prove the labelled version of Kruskal's tree theorem for labels in any well-quasi-order . Assume there is a bad sequence , and choose one minimal in vertex count at each position, subject to bad extendibility. Let be the collection of rooted subtrees obtained by deleting a root and taking one of its child branches, over all .
This collection is well-quasi-ordered. Otherwise take a bad sequence from . Only finitely many of these objects can come from any bounded initial segment of the , since that segment has only finitely many child branches and a bad sequence cannot repeat an object. Pass to a subsequence with a child branch of and . Then
is bad: a prefix tree embedding into would embed into , and the are already bad among themselves. The next object has fewer vertices than , contradicting the minimal bad choice. Notice that a child branch does embed into its full tree under the stated homeomorphic convention.
List each tree's child branches in any chosen order. The preceding result and Higman's lemma make these finite lists well-quasi-ordered. The product of two well-quasi-orders is well-quasi-ordered: first thin to an infinite nondecreasing subsequence in one coordinate and then find an increasing pair in the other. Therefore there are such that the root label of increases to that of , and the child list of embeds as a subsequence into the child list of , with each source branch homeomorphically embedding into its matched branch.
Map the root of to the root of , and use these branch embeddings below it. Different child branches map into different host branches, so their lowest common ancestor maps to the host root. Within each branch it is preserved by the chosen embedding. Thus the whole map is injective, preserves all lowest common ancestors and respects labels, contradicting badness. Finite rooted trees labelled by a well-quasi-order are well-quasi-ordered under homeomorphic embedding. Taking one label proves Kruskal's tree theorem. If one uses a root-preserving convention, mark the root by a separate label incomparable with all ordinary labels and apply the labelled theorem; the marked root then has to map to the marked root. No adjacency-preservation assertion is being made.
For Friedman's finite form of Kruskal's theorem, fix . The required finite conclusion is
Assume there were arbitrarily long bad sequences satisfying these size bounds. Form the tree of their finite prefixes, using rooted-tree isomorphism classes as objects. At position only finitely many finite rooted trees have at most vertices, so this prefix tree is finitely branching and has nodes at arbitrarily large depths. König infinity lemma supplies an infinite branch: at each step some child must still have arbitrarily deep extensions, because there are only finitely many children. The branch is an infinite bad sequence of finite rooted trees, contradicting Kruskal's theorem. Thus such an exists. The argument also works for any prescribed size-bound function, or any fixed finite label set, because each position then still has finitely many possible objects.
A useful precise form of the Ehrenfeucht-Mostowski theorem is this: for an infinite structure and any linear order , a model of can be generated as a Skolem hull by distinct order indiscernibles . Every order automorphism of extends to an automorphism of that hull in the chosen Skolem language. One may first name all elements of , giving an elementary extension containing the original structure. The generation and uniqueness assertions concern this specified expansion, not arbitrary automorphisms of its reduct.
Choose a Skolem expansion : for each existential formula add a function selecting a witness whenever one exists. Introduce constants for . Take the theory of , distinctness of these constants, and all equivalences
The formulas here are in the fixed expanded language, without the newly added as extra parameters. If naming , use its complete elementary diagram and allow those original names in the formulas.
Every finite fragment has a model by Ramsey's theorem. Only finitely many formulas and constants occur. Take a sequence of distinct elements of . For each arity appearing, color the increasing tuples from this sequence by the finite vector of truth values of all formulas of that arity. Successive Ramsey thinning gives an infinite subset homogeneous for each of these finitely many colorings. Assign the finitely many constants in increasing order to distinct elements of this subset. This satisfies every displayed equivalence in the fragment; the original theory is satisfied because the underlying structure remains . Compactness now gives a model of the full theory, with the required order-indiscernible sequence.
The substructure generated by the constants under the Skolem functions is elementary: any existential formula with parameters which are terms in the generators has its Skolem witness in that same hull. If is an order automorphism of , define
Indiscernibility makes this well-defined, by applying it to the equation between any two term representations using the increasing tuple of all their indices. The same argument preserves every relation and function; supplies the inverse. It is unique in the generated Skolem structure. This completes the Ramsey proof, rather than stopping at the existence of indiscernibles.
For simple typed set theory with atoms, use sorts and membership only from to . A set predicate distinguishes sets from atoms, extensionality compares sets of the same positive type, and comprehension produces in type every subset of defined by a well-typed formula. Atoms have no members. First-order models use Henkin semantics; they are not required to have their next domain equal to the full external power set. Typical ambiguity is the schema for each closed sentence, where every sort index in is raised by one.
We show finite satisfiability of this entire typed theory with ambiguity. Choose a list of ranks above , spaced by at least two. For a finite increasing selection of ranks , let
where is the set of objects declared to be sets at type . Membership from to is ordinary membership restricted to objects of ; all other type- objects are atoms. The spacing puts inside . Thus comprehension and set extensionality hold exactly, and atoms have no typed members. There are infinitely many objects at every visible type, so any usual typed infinity requirement also holds.
The auxiliary rank provides a uniform interpretation if a set predicate is allowed at type zero; no type-minus-one domain is used in the theory. This avoids artificially declaring all type-zero objects to be atoms, which would not be invariant under type-raising. If the language has no type-zero set predicate, simply ignore this auxiliary interpretation.
A finite set of ambiguity instances uses finitely many closed sentences of bounded highest type, say at most . Color increasing -tuples of ranks by their finite truth vector in the structure with visible domains and the auxiliary preceding rank. Ramsey's theorem gives an infinite homogeneous rank set. Choose consecutive ranks from it and build the hierarchy on all these ranks. The first window evaluates each original sentence; shifting the window one place evaluates its uniform type-raise. Homogeneity makes the truth vectors equal. All finite typed axioms and the selected ambiguity instances therefore hold together. Choosing large enough covers every sort needed by the finite fragment. Many-sorted compactness, equivalently ordinary first-order compactness after encoding sorts, yields
This is a model existence argument in the ambient set theory; no equality of adjacent type cardinalities is claimed. The gaps between ranks supply atoms, and the ambiguity is about truth of sentences, not a bijection between domains.
A measurable cardinal is an uncountable cardinal carrying a nonprincipal -complete ultrafilter : intersections of fewer than members of remain in . Such an ultrafilter contains no set of size less than . Indeed each singleton is absent, and intersecting fewer than singleton complements shows that every small set's complement is in . In particular every tail of is in .
Form the ultrapower of the universe by functions , identifying functions agreeing on a member of , and interpreting membership coordinatewise modulo . The Łoś theorem, applied separately to each formula, makes the map elementary. Countable completeness makes the ultrapower well-founded: an infinite descending chain would give -large sets witnessing each step, whose countable intersection is nonempty; a coordinate in that intersection would give an infinite descending membership chain in the original universe. The relation is extensional and set-like, so the Mostowski collapse theorem gives a transitive class and an elementary ultrapower embedding .
For each , every function is constant modulo . If no fibre were in , intersecting the fewer than fibre complements would give the empty set in . Induction on therefore shows that the collapsed ultrapower ordinal has precisely the elements , so
The identity function represents an ordinal below , and every constant is below it modulo , since a tail is large. Consequently
Thus the canonical collapsed embedding is not the identity; its first moved ordinal is . For a general measure the identity-function class need not collapse to exactly ; that stronger equality holds for a normal measure. The argument above needs only its lower bound.
Conversely, suppose is elementary, is transitive, its critical point is , and its derived measure is a set, as for the usual definable or amenable class embeddings. Define
Because , elementary preservation of complements and intersections makes this an ultrafilter. It is nonprincipal since for . For a sequence of large sets, fixes the index ordinal and takes the intersection to the intersection of their images; belongs to every image and hence to the intersection. Thus is -complete. The set-existence qualification excludes treating an arbitrary external class map as a set parameter without justification.
For context, measurability already implies regularity and the strong-limit property. A cofinal sequence of length below partitions into that many bounded, hence small, pieces; completeness and their absent fibres contradict covering all of . If there were distinct subsets of some , for each coordinate choose the -large side deciding its membership bit. The intersection of these large sets would still be large, but all its indices would label the same subset, so it would have at most one member. This contradiction gives . Thus the first moved ordinal is an uncountable strongly inaccessible cardinal, in addition to being measurable.
Write when every -coloring of the -element subsets of has a homogeneous subset of order type . The Erdős-Rado theorem for pairs states, for infinite ,
In particular a countable-color partition of pairs from has an uncountable homogeneous set. The standard Erdős-Rado theorem for finite arities is
We prove it, including the pair case, by constructing an end-homogeneous routing tree.
For a coloring , , route each vertex as follows. Given its previously selected increasing ancestors, choose the least greater than all those ancestors such that
The candidate always qualifies. Select it and stop if it is the minimum; otherwise add the selected to the ancestors and continue, including at limit stages. The ancestors are strictly increasing below , so the process must stop. If a selected ancestor is routed separately, its earlier path is the same: its color constraints agree with those of and the same least choices are forced. Thus the paths define a tree order on the vertices.
A node at depth is determined by the table of its colors on the -subsets of its ancestors. Given the table on , recursively take the least compatible candidate at each depth; at a limit depth use all preceding constraints. This recovers both the path and its final node. Therefore
Along any branch, once an -tuple of ancestors is fixed, the color is independent of all subsequent choices of on that branch. This is exactly end-homogeneity.
For the pair case take and . If all node depths were below , then each level would have size at most , and the union of levels would have size at most . This contradicts the number of vertices. Hence some node has at least ancestors. On that branch assign to each ancestor its constant color to all later ancestors. Regularity of implies that one of the colors occurs times, giving the desired homogeneous set. Its increasing enumeration has a subsequence of order type .
For the higher-arity induction let , so . At depths below the same bound is at most , forcing a branch of length . End-homogeneity defines a coloring of its -tuples by the common color of adjoining a later branch vertex. The previous-arity theorem gives a subset of order type homogeneous for , and every -tuple from it then has the same color under . The base case is the infinite pigeonhole principle at . This proves the full finite-arity statement.
One suitable ordinal partition-bound function is
It is nondecreasing and . It is total: choose an infinite cardinal ; the pair theorem supplies a homogeneous subset of size for every allowed color number, and its order type contains a copy of . Thus is a bound in the displayed minimum.
Let an uncountable cardinal be the supremum of a cofinal increasing sequence of iterates of , with each iterate and its successor still below . For every , monotonicity and some later iterate give . Thus the relevant consequence of being such a supremum is
If the iteration already reaches a fixed point, its constant continuation of course has that fixed point as supremum as well. A strictly increasing countable iteration instead has a countable-cofinality supremum and cannot satisfy the uncountable regular tree-property condition below; one must not assume existence of the extra condition from iteration alone.
Here closure under forces a strong-limit bound. For infinite , color distinct binary strings in by their first differing coordinate. Three strings cannot have all three first-difference coordinates equal, because there are only two bit values at that coordinate. Hence this -coloring has no homogeneous triangle, and in particular no homogeneous subset of order type . Therefore
Since and , it follows that for every .
Now impose the tree property: every tree of height , with nonempty levels of size below , has a cofinal branch. If this definition is extended to singular cardinals, it also forces regularity. For a singular , take disjoint chains of lengths cofinal in , one for each index below . Every level has at most nodes and the height is , but each branch remains in one shorter chain. A common new root may be added if rooted trees are required. Under the more usual convention the tree property is only defined at regular uncountable cardinals, so regularity is part of the convention instead.
For a coloring with , the routing tree has levels of size at most by the strong-limit property. If some node has height at least , there is already an end-homogeneous branch of that length. Otherwise the tree has height exactly : a smaller number of levels of size below could not contain its nodes, by regularity. The tree property then supplies a cofinal branch. Along it, one of the fewer than ancestor colors occurs times, again by regularity. Thus for every , giving
Moreover the closure argument gives strong limit and the tree argument gives regularity. Thus an uncountable -closed cardinal with the tree property is strongly inaccessible.
The final printed assertion requires that qualification. The ordinary tree property alone does not imply strong inaccessibility. At it is König's infinity lemma and is not uncountable. Even when the convention excludes , there are relative-consistency models in which has the tree property, although a successor cardinal is never strongly inaccessible; this result is recalled in the introduction of Friedman, Honzik and Stejskalová. No proof of the bare implication is possible under that standard definition. The preceding paragraphs prove the corrected implication in the actual -closure setting and the requested fixed-point conclusion, without silently replacing tree property by weak compactness.
We prove the Ehrenfeucht-Mostowski theorem by ordered products of ultrafilters, without using Ramsey's theorem. Choose a Skolem expansion of the infinite structure and distinct elements . Fix a nonprincipal ultrafilter on .
For a finite increasing subset of the desired index order , define the ordered Fubini product of ultrafilters on by
The notation means that the set of satisfying belongs to ; the leftmost quantifier is outermost. Upward closure and intersection follow successively at each coordinate, and applying complement at each step proves the ultrafilter dichotomy. Products are ordered; no false claim of symmetry is needed.
Put , with . If , pullback of a function by coordinate projection induces
For a cylinder condition involving only coordinates in , deleting the unused ultrafilter quantifiers makes its membership in exactly its membership in . The Łoś theorem therefore makes an elementary embedding, not merely a homomorphism. The projection identities give .
Take the directed limit of this system: elements from two stages are identified if their images agree at a common larger finite stage, and formulas are evaluated at such a stage. Elementary coherence makes this well-defined. It also makes each stage elementary in the limit: a formula uses finitely many parameters, and an existential witness at a later stage can be pulled back at the level of existential truth because the transition maps are elementary. Denote the limit by .
For each , let be the limit image of the coordinate function . These elements are distinct. For , after fixing , equality holds for at most one , a set not in ; hence equality fails in the two-coordinate ultrapower and therefore in the limit.
For any increasing , Łoś evaluates
The right-hand side depends on the formula and the number of increasing coordinates, not their particular indices. Thus is order-indiscernible for every formula of the expanded language simultaneously; no preliminary homogeneous thinning is used. If elements of were named before expanding, the same computation gives indiscernibility over those names and the initial stage embeds the original structure into the limit.
The Skolem hull of these generators is elementary by the witness property. Transporting the generators by any order automorphism of transports every term, with well-definedness and relation preservation supplied by the formula equivalence just proved. The inverse transport supplies an inverse automorphism. The ordered-ultrapower construction gives the full Ehrenfeucht–Mostowski model and its order automorphisms without Ramsey's theorem.
A model-theoretic ultralimit is the elementary direct limit of a chain of successive ultrapowers along their diagonal embeddings. We will build two such chains with isomorphic limits. This is not a topological ultrafilter limit and does not require the stronger claim that one ultrapower of each structure is already isomorphic.
First prove the Frayne embedding lemma, including the relative form needed to make the diagrams commute. If , expand the language by constants naming every element of , and let be its complete elementary diagram. Index by finite subsets of this diagram. The finitely many constants in can be interpreted in so that holds: existentially quantifying them gives a sentence true in and hence in . Choose such interpretations, and give unused constants an arbitrary fixed value in the nonempty domain of .
For each diagram sentence , its cone has the finite intersection property with the other cones. Extend the generated filter to an ultrafilter . For , let be its chosen interpretation at coordinate . The map
is elementary by Łoś: every formula true of a tuple from , or its negation, is a diagram sentence and holds on its corresponding cone. In particular distinct named elements stay distinct.
If , the construction can keep every constant naming equal to that same at every coordinate. For a finite diagram fragment, existentially quantify just the names outside ; the resulting formula with parameters in is true in , hence true in . Thus the finite realizations still exist with all those old names fixed. Consequently
This relative extension of the diagonal map is the essential strengthening.
Now let . The nonrelative lemma embeds into an ultrapower of . Identify the image with a copy of inside . Since , the relative lemma embeds into an ultrapower of extending its diagonal map. Rename this larger structure so that the displayed copy of is a literal elementary substructure. Next apply the relative lemma over to embed into an ultrapower of fixing its diagonal copy. Continue alternately. We obtain a coherent elementary chain
with as well. Each inclusion is, up to these coherent identifications, the diagonal embedding into its ultrapower; the same holds for . It is the relative clause, not merely the existence of arbitrary elementary embeddings, which guarantees this.
By the elementary chain theorem, the unions of the two subsequences are elementary limits. They are the same structure: each lies in a subsequent , and each lies in . Hence the alternating ultrapowers give isomorphic ultralimits construction proves
Conversely each ultrapower and each elementary direct limit has the same first-order theory as its starting structure. Isomorphic ultralimits therefore imply as well. Thus the conclusion exactly characterizes elementary equivalence at the level of ultralimits.

Articles by others on the same topic (0)

There are currently no matching articles.