Here an ultralimit in the model-theoretic sense is a model-theoretic ultralimit: start with a first-order structure, take successive ultrapowers along their diagonal elementary embeddings, and take the directed limit of elementary embeddings of that chain. The elementary chain theorem, proved by induction on formulas after identifying the embeddings with inclusions, makes every stage elementary in the limit. This definition concerns structures, rather than the topological ultrafilter limit.
We first prove the needed Frayne embedding lemma. If , every finite subset of the elementary diagram of a structure can be realized in : existentially quantify its finitely many named elements, and use elementary equivalence. Index by finite diagram fragments, choose such realizations, and extend the filter of cones requiring each diagram formula to an ultrafilter. For each , let give its chosen coordinate realizations, filling unspecified coordinates arbitrarily. The Łoś theorem shows that is an elementary embedding of into an ultrapower of . The formulas ensure injectivity.
There is a relative version: if , keep all named elements from constant in every coordinate. Each finite diagram fragment is realizable in over those parameters by elementarity, so the resulting embedding extends the diagonal embedding of into its ultrapower.
Now use alternating ultrapowers give isomorphic ultralimits. First embed into an ultrapower of . Apply the relative lemma to , embedding into an ultrapower of over its diagonal copy. Next embed into an ultrapower of over , and continue. After coherent identifications this givesEach is an ultrapower of along its diagonal embedding, and each is an ultrapower of likewise. The two subsequences are cofinal in the same chain of elementary substructures, so their limits are the same union. Hence . No isomorphism theorem for single ultrapowers has been assumed.
Order the collection of all chains in a partial order, including the empty chain, by inclusion. Suppose that were an order-preserving injection. The chain-poset nonembedding lemma follows by a transfinite recursion of length the Hartogs ordinal :Inductively, the previously constructed points form a strictly increasing chain. If , then , since belongs to the latter but not the former. Monotonicity gives , and injectivity makes this inequality strict. Thus the recursion continues at every and gives an injection , contradicting the defining property of the Hartogs ordinal. Therefore The empty chain is part of the convention: excluding it would make a one-point poset a counterexample.
Suppose a nonempty set had no minimal member for the intersection-power-set predecessor relation. Put , which is a set by separation. For every there is an with . Since , this gives . Intersecting over every yields .
Now form the diagonal subset . It belongs to , hence to , so its defining condition implies , a contradiction. Thus This is a Cantor diagonal argument; it uses neither the Axiom of foundation nor the axiom of choice. In particular, no selection of an infinite descending sequence is needed.
Use the embedding characterization of a supercompact cardinal: for every cardinal there is an elementary embedding into a transitive class with critical point , and . In the Lévy hierarchy, a sentence can be put into the form with bounded matrix . The same argument allows parameters , which the embedding fixes.
Suppose and choose a witness . Pick an ordinal with , and a cardinal large enough that and . Take the corresponding supercompact embedding. Its closure implies : induct on rank, enumerate each set in this rank segment by at most elements already in , and use followed by taking the range. Thus and .
Bounded formulas are absolute between transitive classes. Since holds in , it holds in and then in the transitive rank segment . This segment contains , soApply elementarity to the first-order assertion that this sentence holds in the indicated cumulative hierarchy level, and use . We obtain the supercompact Sigma-two downward reflection conclusionThe closure requirement is used to put the original witness into the target; elementarity alone would not do that.
In an infinite game of perfect information, the players alternately choose elements of a nonempty set , producing . Player I wins when belongs to the payoff set . A strategy in an infinite game chooses a move at each position where its player moves, and a winning strategy in an infinite game wins against every possible opposing play. The Gale-Stewart theorem states that such a game is determined when is open in the product topology of discrete . The same holds for closed payoff sets and, more strongly, for every payoff set.
For open determinacy, let be the positions and the prefixes certifying a win for I, where is the extension cylinder set. Form the winning-position attractor in an infinite game by transfinite recursion: start at , at a successor stage add I-positions with some successor already in and II-positions with all successors in , and take unions at limits. This increasing sequence stabilizes, since its positions form a set. Call the stable set .
Each position in has a least entry ordinal, necessarily a successor. I chooses a successor with smaller entry ordinal; every II successor has smaller entry ordinal. An infinite strictly decreasing sequence of ordinals is impossible, so play reaches in finitely many moves. This gives I a winning strategy in an infinite game from every position in . Outside , all I moves stay outside, while II can choose a move outside. The axiom of choice selects those moves simultaneously. Such a play never reaches , so it is outside the open payoff set. Thus II wins from the complement of , proving determinacy. Interchanging the players and complementing the payoff gives closed determinacy.
We prove the strengthening via Buchi games, including their determinacy argument. On a set of positions with nonempty successor sets, putFor a specified set of marked positions, I's objective is to visit infinitely often. For each , let be the least fixed point obtained by starting and iteratingwith unions at limits. Its inner entry ranks let I force a visit to . The operation is monotone. Starting at , iterate with intersections at limits. This descending sequence stabilizes at .
From , the inner ranks force a marked position with a next move still in . I chooses such a move, and the construction repeats. At II-positions all necessary moves stay in the indicated inner attractor, or in at a marked position. Every round takes finitely many moves by decreasing inner ranks. I therefore forces infinitely many marked visits.
For , let be its removal rank: . Since , at I's turn all successors lie outside , and at II's turn there is a successor outside it. II chooses such successors. If also , then ; II can choose outside , or every I move lies outside . Along this strategy removal ranks never increase and strictly decrease after each marked visit. Infinitely many visits would give an infinite ordinal descent, so II wins. This proves Buchi game determinacy on a set-sized arena without any countability restriction.
Now write the original payoff as , with each open. Add a deterministic monitor to the finite position, initially . At each new prefix, if its cylinder is contained in , increment the monitor and mark that step. For a play , the monitor increments infinitely often exactly when . In one direction every increment certifies the next required open set. In the other, after the monitor reaches , openness of supplies a later certifying prefix, so it eventually reaches . The expanded game is a Buchi game; its monitor is determined by the observed finite play, so its winning strategy transfers directly to the original game. ConsequentlyComplementing and interchanging players also gives determinacy for payoff sets. These arguments work on pruned game subtrees as well, and assigned terminal winners can be incorporated by replacing each terminal position by an absorbing position with the corresponding outcome.
Let be nonempty first-order structures in one language and let be an ultrafilter on . In the ultraproduct , identify functions when , interpret functions coordinatewise and relations by their coordinate truth sets. The Łoś theorem states that for every first-order formula ,All interpretations are independent of representatives: changing finitely many arguments on -small sets changes truth only on their finite union, also -small.
Prove the theorem by structural induction on formulas. Terms evaluate coordinatewise by induction on terms. This proves the atomic cases of logical equality and relation symbols. For conjunction, intersect the two truth sets and use the filter laws. For negation, the truth set is complemented, and an ultrafilter contains exactly one of a set and its complement. These cases supply the other Boolean connectives too.
For the existential step, a witness in the ultraproduct makes the coordinate truth set for belong to by the induction hypothesis. That set is contained in the coordinate truth set of , so the latter is in . Conversely, if that existential truth set belongs to , choose a witness in for each , and any element of elsewhere. The axiom of choice supplies this function. The induction hypothesis makes a witness in the ultraproduct. Universal quantification follows by negation. This completes the proof.
For the compactness theorem, take to be the set of finite subsets of the given theory . For each , choose . For , the cone is nonempty, and any finite intersection of such cones contains their union as an index. Extend the filter they generate to an ultrafilter . By the proved Łoś theorem, the ultraproduct satisfies every , because its coordinate truth set contains . Thus . This proves compactness without assuming it in the ultraproduct construction.
The Ehrenfeucht-Mostowski theorem asserts that an infinite first-order structure has, for any prescribed total order , an elementary extension containing distinct order-indiscernibles . After a Skolem expansion, the Skolem hull of those generators is a model of the original complete theory. Every order automorphism of extends to a unique automorphism of this specified Skolem hull in the expanded language.
Choose a Skolem expansion of the original infinite structure: for each existential formula, select a witness function, including nullary functions when needed. Add constants for and the elementary diagram of a structure of , using separate names for its elements. Require for distinct indices, and for each formula in the Skolem language requirewhenever both index tuples are strictly increasing. These are the order-indiscernible sequence requirements.
Every finite fragment is satisfiable in . Choose a countably infinite sequence of distinct elements of . The fragment mentions only finitely many formulas and arities. Color increasing -tuples of that sequence by the finite vector of truth values of its relevant -ary formulas. The Ramsey theorem supplies an infinite homogeneous subsequence; repeat for the finitely many arities. Assign the finitely many named to distinct elements of the final homogeneous subsequence in increasing index order. The fixed finite part of the elementary diagram of a structure already holds in . By the compactness theorem proved in Question 5, the full set of requirements has a model , giving the required elementary extension and order-indiscernible sequence.
Let comprise all values of Skolem-language terms in finitely many . It is closed under the witness functions. If for parameters in , the specified witness function supplies a witness in . Induction on formulas therefore gives ; its reduct is a model of . For infinite , its cardinality is at most and at least .
For an order automorphism , defineRewrite any finite list of indices in increasing order, allowing a term to repeat or omit variables. The order-indiscernible sequence property transfers every equality between terms and every relation among their values, making this definition well defined and elementary. Applying gives its inverse. All of is generated by the and the named Skolem functions, so an automorphism extending must have precisely this action. Thus , with uniqueness in the Skolem expansion. This uniqueness need not hold in the unexpanded reduct.
A measurable cardinal is an uncountable cardinal carrying a nonprincipal ultrafilter on that is -complete: intersections of fewer than members of remain in . An elementary embedding preserves truth of every first-order formula, with its parameters carried along by .
The identity is always an elementary embedding of the universe into itself. The substantive question concerns a nonidentity embedding. In ZFC, the Kunen inconsistency theorem givesHere, as usual for class embeddings, restrictions to sets and the recursively defined critical sequence are available. We give the stationary-set proof, including its partition ingredient.
Suppose such a existed. It has a least moved ordinal , its critical point of an elementary embedding. To see why some ordinal must move, if all ordinals were fixed, induction on rank would fix every set: membership of in is equivalent to membership of in once every lower-rank is fixed. A rank segment containing a moved set would then be fixed pointwise, a contradiction. The critical point is an uncountable cardinal. All finite ordinals and are definable and fixed. If had cardinality , a bijection would be carried to a surjection whose range still consists exactly of the fixed ordinals below , impossible since .
Put , and . Applying to this Kunen critical sequence shifts it by one, so . Elementarity also gives ; write .
We need a stationary partition at a successor cardinal. If is stationary, choose bijections for . For each , on the stationary tail the function is regressive. The Fodor lemma supplies a stationary fiber with constant value . Some value occurs for many , since a union of sets each of size at most cannot have size . For distinct such , their fibers are disjoint: cannot equal two different ordinals. These fibers yield disjoint stationary subsets; include any leftover points in one cell. Grouping cells also gives a partition into any nonzero number at most .
For completeness, the Fodor lemma used here follows from diagonal intersections of clubs. If a regressive function had no stationary fiber, choose a club set disjoint from each fiber. The diagonal intersection is club by regularity and closure. A point in its intersection with would belong to , contradicting the choice of that club.
The set is stationary: inside any club choose a strictly increasing countable sequence, whose supremum still lies below the regular uncountable and belongs to the club. Partition it as . Its image is another stationary partition of the same .
The set is club. Closure is immediate. To get a member above any given ordinal, repeatedly bound the images of all earlier ordinals and take a countable supremum; regularity of keeps each bound below . Choose . Since , a countable cofinal sequence in and give : the image sequence remains below by closure under , and .
But for some . Applying and using gives , contradicting its membership in the disjoint cell . This proves the assertion. The use of axiom of choice in the cardinal and stationary-partition arguments matters; the conclusion here is explicitly in ZFC.
Write for ZF with the Axiom of foundation omitted. Independence is a relative-consistency assertion: from a model of ZFC we construct models of , both with and without axiom of choice. A model of ZFC itself supplies the positive cases.
First use a Rieger-Bernays permutation model. Inside the starting model choose a definable class bijection and put exactly when . The new extension of is the old set , so any prescribed set of new members has representative . We verify the axioms rather than treating the change of membership as automatically harmless.
The axiom of extensionality follows from injectivity of . The new empty set is and a pair with members is . The union of a new set is represented byA new subset of means . Hence the new power set of is represented byThese are sets by the original power-set and replacement axioms. Translate each formula by replacing membership with . The original separation axiom extracts the required subset of , and replacement collects the range of a definable functional relation on ; applying gives their new representatives. Thus the full Axiom schema of replacement and separation schemes survive.
For axiom of infinity, start at , iterate the new successor along the old , and take a new set representing this range. It contains the new empty set and is closed under the new successor. Finally, the old axiom of choice well-orders each old extension . Encode that relation using new ordered pairs and its new set representative. All subsets of the extension are represented in the new model, so this is genuinely a new well-order. Thus choice survives the full membership permutation.
Now transpose the old and and fix every other object. The old empty set satisfies , so its sole new member is itself: it is a Quine atom. The nonempty new set has no member disjoint from it, violating foundation. This gives . Together with the starting model, this proves independence of foundation.
For failure of choice, a membership permutation alone is insufficient, as the verification above shows. Add a symmetry restriction. Choose distinct old objects for and let simultaneously swap with , fixing all other objects. The two families are disjoint, so this is a class bijection. Each is now a Quine atom. Write for the new set having precisely these atoms as members.
Every permutation of the atoms extends to an automorphism of the new universe, fixing its pure well-founded part. To construct it, send the atoms according to the prescribed permutation and, for any other object , take the unique object whose new members are the images of its new members. This recursion is well founded away from the atomic self-loops: every other membership step decreases old rank, including the steps from the transposed singletons to their old extensions. Thus all the required automorphisms exist.
An object is supported by a finite set if every atom permutation fixing pointwise fixes it. Let consist of objects that have finite support in a permutation action and all of whose new membership descendants also have finite support in a permutation action. This is the hereditarily finite-supported Quine-atom model. The atoms belong to , as does itself. We check that restricting to preserves .
Extensionality is inherited because every member of an object of is again in . Empty sets, pairs and unions have supports obtained by taking finite unions of the supports of their parameters, and their descendants are already supported. The pure natural numbers and their set are fixed by every atom permutation, giving infinity. For separation, permutations fixing the domain and formula parameters preserve the defined subset, which therefore has their common finite support in a permutation action. For replacement, translate the relativized formula into the original universe and use original replacement to collect its unique values. Every value lies in , and the range is invariant under the same finite support in a permutation action. Finally, the collection of all -subsets of an object is a subcollection of its full new power set, hence is a set in the original universe. Every permutation fixing a support of permutes these supported subsets, so this collection is supported; its members and their descendants lie in . This verifies the internal power-set axiom. These arguments handle the full schemes with arbitrary finite tuples of parameters.
There is no choice function on the two-element subsets of in . Suppose were one and had finite support in a permutation action . Choose distinct atoms . The transposition exchanging them fixes and the unordered pair , but exchanges its two possible selected values. Thusis impossible. The family of all such pairs belongs to : it is invariant under every atom permutation and each pair has finite support in a permutation action. Therefore ; it still contains the self-membered atoms, so it also fails foundation. We have provedThe positive-choice permutation model and this negative-choice symmetry model establish independence of choice from . These constructions can be carried out internally in any starting model; no assumption of a transitive set model is needed.
Use rooted-tree homeomorphic embedding: an injective map of vertices preserves ancestor order and lowest common ancestors, so edges may be stretched into paths and distinct branches remain distinct. The source root may map below the target root. Kruskal's tree theorem asserts that finite rooted trees are well-quasi-ordered by this embedding: every infinite sequence has with . More generally, labels from any well-quasi-ordering may be required to increase under the embedding. This labelled result implies the unlabelled one by using a one-point label set, and also implies the version for unrooted trees by choosing roots arbitrarily.
We first prove the word lemma needed for the tree argument. In a well-quasi-ordering , every infinite sequence has an infinite nondecreasing subsequence. Indeed, some term must be below infinitely many later terms: if no term were, recursively avoiding the finitely many successors dominated by each previously chosen term would produce a bad sequence. Repeat this observation inside the infinite set of later terms dominating the chosen one.
The Higman lemma says that finite words over are well-quasi-ordered by subsequence embedding with letterwise comparison. Suppose otherwise, and choose a minimal bad sequence of words, minimizing length at each position among words admitting a bad continuation of the chosen prefix. No word is empty. Write , separating its last letter. Choose indices on which is nondecreasing. Thenis bad. A comparison from a prefix word into some would give a comparison into in the old bad sequence. A comparison , , together with would give . Both are impossible. But the new continuation uses a shorter word at position , contradicting minimality. This proves the Higman lemma.
Now suppose there were a bad sequence of labelled finite rooted trees. Choose it minimally by number of vertices at each position. Let be the collection of all proper rooted subtrees occurring at vertices other than the roots in these trees. We claim that is well-quasi-ordered. Otherwise take a bad sequence of such subtrees , with a proper subtree of . The indices cannot remain bounded, because finitely many finite trees have only finitely many rooted subtrees, and repetition is a comparison. Pass to a subsequence with strictly increasing . The sequenceis bad: a comparison from an earlier into would compose with the subtree embedding to contradict the original badness. Its other comparisons were excluded already. Since has fewer vertices than , this contradicts minimality, proving the claim.
List each tree's immediate root subtrees in any chosen order. These are finite words over , hence form a well-quasi-ordering by the word lemma. Combine the lists with the root labels. A product of two well-quasi-orders is well-quasi-ordered: pass to an infinite nondecreasing subsequence in the first coordinate and find a comparable pair in the second. Thus two trees have comparable root labels and a subsequence matching of their child lists. Map the first root to the second root and use the matched subtree embeddings in distinct child branches. The resulting injective map preserves labels and lowest common ancestors, giving , the desired contradiction. This proves the full labelled form of Kruskal's tree theorem.
Friedman's finite form of Kruskal's theorem is a uniform finite consequence. For every fixed natural , there is such that any sequence of finite rooted trees satisfying has a comparable pair . It also holds with labels in any fixed finite label set. To prove it, assume no such exists. Form the finite bad-sequence tree whose nodes are bad finite tree sequences satisfying those size bounds, using one representative of each isomorphism type. Each position has finitely many extensions, since there are finitely many labelled tree types of each bounded size. By assumption this finitely branching tree has nodes at every finite height. The König infinity lemma supplies an infinite branch, which is an infinite bad sequence of trees, contradicting the theorem just proved. HenceLikewise, using fixed labels with the bound for gives the customary finite labelled tree form. Only existence of its finite bound is claimed here, not a small numerical estimate.
We prove the Borel determinacy theorem by reducing each Borel game to a clopen game while preserving winning strategies. The construction permits arbitrary set-sized alphabets; no enumeration of the move set is used. Assume . For an empty alphabet the game ends at its initial position, with its assigned terminal outcome, and is trivially determined.
Allow intermediate game trees to have terminal positions with assigned winners. Write for the space of infinite branches, with its prefix-cylinder topology; the payoff governs infinite plays, while the assigned winners govern finite plays. Question 4's attractor proof still gives open and clopen determinacy: include I-winning terminals among the initial targets and make the opposing terminals absorbing losses.
A covering of an infinite game consists of a new tree , a prefix-preserving map preserving lengths, and a strategy map for each player. Old terminal outcomes must be inherited. The strategy map is local in depth: choices before depth depend only on the given strategy before depth . Its essential lifting requirement is that each original play following has a lift following whose projection is , or whose projection is an initial segment of and which ends with a loss for the player using . Infinite projections are taken by union of prefixes. A -covering is identical to the original tree, terminal assignments and strategy choices through depth .
These conditions transfer winning strategies for every payoff. Indeed, if wins the covered game with payoff , a lift of a play following cannot be an early loss for its player. The lift therefore projects to the whole original play. Infinite membership in agrees under projection, and an original terminal loss would also be a loss in the game covering. Hence the original play is won. Call a game covering an unravelling of a game payoff when is clopen in .
We first construct a -covering unravelling any closed . Choose an even and leave the first levels unchanged. At a nonterminal position of length , I's next move will carry auxiliary information. For each legal ordinary move , let be the set of first nonterminal positions strictly beyond whose infinite continuations miss : means extends , , and no intervening strict extension of has this property. These positions are pairwise incomparable. I plays , where .
If was already terminal, inherit its outcome. Otherwise II has two types of response. On accepting, II plays with an ordinary legal move, and subsequent moves are ordinary. When a position is reached, end the covered game with a win for I if and for II if . Other old terminals retain their winners. On challenging, II plays with and an initial segment of ; subsequent play is forced along until reaching it and then proceeds ordinarily in . Original terminal outcomes remain in force. Forget the auxiliary data to define .
For an infinite accepted play, no exit in was reached. Its projection belongs to : if it did not, closedness would give a prefix cylinder disjoint from , and the first such nonterminal extension strictly beyond would have ended the play. An infinite challenged play projects through an exit and therefore misses . Thus, among infinite plays, the inverse image of is exactly the acceptance branch of this finite protocol. It is clopen, decided at depth .
Here are both strategy-transfer maps; these are necessary because continuous projection by itself does not preserve determinacy. Given a strategy for I in the covered tree, follow its ordinary moves while simulating acceptance of its announcement . If an exit is reached, continue arbitrarily: that play has an early covered loss for I as a lift. If is reached, switch to the continuation prescribed by under the challenge of . This is consistent with the already observed prefix, since the challenged game forced every intermediate move along . If no exit is reached, acceptance itself supplies the full lift. Old terminal plays lift in the same way. This defines and verifies the lifting requirement for I.
For a covered strategy for II, at the projected position defineAgainst announcement , the strategy must accept: a challenge would have to name an element of , contradicting its definition. Simulate this acceptance, including its ordinary response . If an exit is reached, it is an early covered loss for II, so continue arbitrarily. If an exit is reached, choose an announcement for which challenges , and switch to that simulation. The challenged game's forced prefix agrees with the observed prefix, including the earlier ordinary response , so it supplies a full lift following . If no exit is reached, the original acceptance simulation gives the full lift. This defines and verifies lifting for II. Choices of use the axiom of choice on a set of possibilities.
Both maps are local in depth. The sets and the chosen use only II's response function at depth ; later choices use only strategy values at the already reached depth. The switches do not query choices at later levels. On irrelevant histories assign fixed legal moves. Thus this is a genuine -covering. Complementing changes neither the game covering nor its lifting property, and complements of clopen sets are clopen. This proves the base construction for both closed and open payoff sets.
We next give the limiting construction needed for the induction. Coverings compose by composing their position and strategy maps; lifting successively verifies the same lifting condition. Supposeis a sequence of game coverings whose th map leaves depth unchanged. For each finite depth , the trees and terminal assignments through that depth eventually stop changing. Define using these stabilized levels. Its map to on a position of length is the composite from any sufficiently late stage; stabilization makes the value independent of the stage. Define strategy maps in the same way, using their locality in depth. These maps respect the tree, terminal outcomes and composition, and leave depth unchanged.
To check lifting, start with a play of consistent with the projected strategy. Lift the entire play successively through the later game coverings, using the corresponding projected strategy at each stage. If all these lifts are infinite, each projects to the preceding one and each finite prefix eventually stabilizes, giving the desired infinite lift in . If a premature own-player loss occurs, later lifts have nonincreasing finite lengths, and those lengths and their prefixes eventually stabilize. This gives a terminal own-player loss in , which is exactly the allowed exceptional lift. The same reasoning handles original finite terminal plays. Thus covers every . This argument uses level stabilization, not compactness of an infinitely branching tree.
Now induct on the countable Borel hierarchy rank, with the strengthened assertion: for every game tree on any set alphabet and every , a payoff of that rank has a -covering unravelling it. The base case of open or closed sets was proved above. Complements preserve the assertion using the same game covering. For the union step, write with constituent sets of smaller rank. Starting at , successively choose a -covering that unravels the inverse image of under the composite map to . This is legitimate because continuous inverse images preserve Borel hierarchy rank, and the induction assertion ranges over all trees and alphabets, including the enlarged ones produced by earlier game coverings.
In the stabilized inverse limit, each pulled-back is clopen, because the later projection to the stage where it was unravelled is continuous. Their union is therefore open. Apply the already proved open-set unravelling construction once more, with preservation depth , and compose with the limit game covering. The result unravels itself. This proves the strengthened assertion at every successor or limit countable Borel hierarchy rank. Every Borel set arises at some such rank: countable unions take the supremum of countably many countable ranks and then one further stage, and complements do not leave the generated hierarchy.
Apply the assertion to and . The covered payoff is clopen and hence determined by Question 4, including its assigned finite terminal outcomes. Transfer its winning strategy through the game covering. We obtainEvery auxiliary alphabet and strategy collection used above is a set. The argument uses power sets and replacement to build those collections and their iterated game coverings, and the axiom of choice for strategy selections; it does not require to be countable.
Articles by others on the same topic
There are currently no matching articles.