Use the order on locale maps in which means for every open . A Hausdorff locale has a closed diagonal in its localic square. A totally unordered locale, or locale, has discretely ordered hom-sets: every comparable pair of maps with any common domain is equal.
In the localic square of , let
This is the largest open disjoint from the diagonal: inverse image along the diagonal sends the rectangle to . Hence is the complement of its closure. If , then
for every summand of . Thus factors through the closure of the diagonal. For a Hausdorff locale that closure is the diagonal itself, so . This proof of Hausdorff implies does not require classical logic.
Here is an explicit classical counterexample to the converse implication from spatial Hausdorffness. Give the topology generated by the usual opens and by . Every open has the form , where are usual open sets and we may arrange . The topology is finer than the usual one, so the space is Hausdorff. Put , the complete Boolean algebra of ordinary regular open elements, and write . Restriction from this space to its rational and irrational subspaces, followed by Booleanization, gives frame homomorphisms
To justify these formulas, each subspace has its ordinary subspace topology and is dense in the ordinary real line. Regular-open algebras of a space and a dense subspace are isomorphic: restrict a regular open and take its interior-closure, with inverse obtained by taking interior-closure in the ambient space. Restriction is a frame homomorphism, and double negation is a frame homomorphism into its fixed-element frame. These observations also show independence of the chosen representation of . Since , we have , but and . Thus this Hausdorff space fails as a locale.
For the remaining arguments about connected locales, use the classical-logic option: positive opens of a locale are exactly the nonzero opens. There is a necessary positivity qualification. The empty locale has no positive opens, so the printed condition on those opens holds vacuously, although no point exists. The point assertions therefore require to be positive. This qualification is automatic if “totally connected” includes nonemptiness; otherwise it must be added explicitly.
Let be positive and satisfy the condition on its positive opens of a locale. Put . It contains , excludes , and is upward closed. If had , their union would be a positive open of a locale with a decomposition into two disjoint nonzero opens, contradicting its being a connected locale. Thus . If , not all can be zero; classical logic supplies a nonzero summand. Hence is a completely prime filter, and its characteristic frame homomorphism defines a point .
The point is dense. Indeed implies by the definition of . In nucleus language the image of has nucleus ; its value at is , so the image is a dense sublocale.
Conversely suppose an open locale has a dense point . Density means only if , and classically this implies for every positive open of a locale. If a positive open split as with and both summands nonzero, then , contradicting preservation of their meet. Thus every positive open of a locale is a connected locale, proving the converse under the declared logical convention.
Let be the terminal map. For a positive totally connected locale , the point above satisfies
because the right side is when and both sides are otherwise. Hence . If and is a totally unordered locale, composition gives , so . Therefore
which is the required constant factorization. For the empty source the factorization need not exist: the unique map does not factor through . Thus the positivity qualification matters for this assertion too.
A preframe has finite meets and joins of nonempty directed sets, with finite meets distributing over these joins. A preframe homomorphism preserves both operations. Its preframe tensor product has generators and relations making a homomorphism separately in each variable. Equivalently,
In particular . The tensor unit is the free preframe on one generator: classically it is , and constructively it is the frame of truth values, with generator .
Regard a frame as a commutative monoid object in preframes, with multiplication and unit . Binary join preserves finite meets and directed joins separately. Conversely take a commutative monoid object in preframes and put
This set contains and , since preservation of the empty meet gives . If , then , and
Thus finite meets are inherited. If is nonempty and directed, separate preservation of directed joins gives
because a common upper bound gives . Directed joins are inherited too. Associativity and commutativity show that is idempotent; it is the least idempotent upper bound of . Therefore is the bottom and is binary join on . Arbitrary joins are directed joins of finite products, including the empty product . Finally
so binary distributivity, together with directed distributivity, proves that is a frame.
A homomorphism from a frame join monoid to sends every element to an idempotent above and therefore factors uniquely through . The factor preserves finite joins and directed joins, hence arbitrary joins. Conversely the inclusion preserves the preframe and monoid operations. Also a preframe monoid homomorphism between frames is automatically a frame homomorphism. This proves the full embedding and its right adjoint: is a coreflective subcategory of , with coreflector .
The coproduct of commutative monoid objects in a symmetric monoidal category is their tensor: the maps are , , and a pair induces . For two frames , the induced multiplication on pure generators is
Every pure generator is idempotent and above . Those properties are preserved by finite meets and directed joins, as just proved, so hold throughout the generated preframe. It is therefore already a frame, rather than requiring a further coreflection. Consequently
Rectangles in the localic product are instead .
For a filtered colimit in a category of frames, form the colimit in preframes, with stage maps . It can be presented by stage elements, all their finite-meet and directed-join relations, and the transition relations. Since tensoring is a left adjoint, it preserves colimits. Filteredness makes the diagonal diagram cofinal in the product index diagram, so the stage multiplications induce . The units agree. Each stage element is idempotent above the common unit; generation again implies . The resulting frame is the filtered colimit in a category in ; its binary join is induced by computing two representatives at a common later stage. Thus binary coproducts and filtered colimits of frames are computed in preframes, with the indicated induced join operation.
We now prove compactness. For a compact locale, its frame has a top test , , preserving finite meets and directed joins. For compact , tensor the tests and use the unit isomorphism to obtain a preframe map with
It reflects top on every pure generator. The property is closed under finite meets and directed joins: for a directed join, preservation of the join says that its truth value is the existential disjunction of the individual truth values, so some term has value . Since pure generators generate the preframe, reflects top everywhere. Applying to a directed cover of therefore shows that a term of that cover is . This proves compactness of the binary coproduct frame, hence of the binary product locale.
For a filtered diagram of compact frames, define on stage
These truth-valued maps preserve finite meets: witnesses can be taken to a common later stage, using filteredness. They preserve directed joins: compactness at the witnessing later stage selects a member of the directed family. They are compatible with transitions, again by filteredness, so induce a preframe map . On stage generators, implies . The same generation argument proves that reflects top throughout . Thus the filtered colimit frame is compact.
Finally the arbitrary coproduct of the frames is the filtered colimit of their finite coproducts, indexed by finite subsets of the index set; the empty finite coproduct is , itself compact. Finite coproducts are compact by the binary argument, and their filtered colimit is compact by the preceding paragraph. Opposing the categories gives
This proves the localic Tychonoff theorem through preframes, without choosing points or invoking the axiom of choice.
Work in the frame , writing for Heyting implication. A nucleus on a frame is an inflationary, idempotent map preserving finite meets. The open nucleus and closed nucleus are
Their meet in the frame of nuclei on a frame is pointwise. The distributivity of a Heyting algebra and the defining adjunction for Heyting implication give
If a nucleus on a frame bounds both, then and . Consequently , so is the top nucleus. Thus and are complements in .
For any nucleus on a frame , put . At an arbitrary ,
since . Moreover . Therefore
Indeed the join is at most , and its value at each is at least . This proves generation by the open nuclei and closed nuclei, without assuming that joins of nuclei on a frame are computed pointwise.
For the given frame homomorphism , restrict the displayed join to and denote the resulting nucleus on a frame by . The same inequalities show and . If has the same values on , its restricted formula is identical, so . Hence is the least representative of the equivalence class. We will also use the consequence
The least representatives form a subframe. For a family , let in . Restricted monotonicity gives for every , hence . For two least representatives, distribution in expresses their meet as the join, over , of
Here and . Since
each summand is below . The opposite inequality always holds, proving closure under binary meets. The top is and is a least representative. Also , because the summand at is ; and , because the summand at is . It follows from the restricted normal form that is exactly the subframe generated by and .
The map preserves finite meets by the formula above. A nucleus on a frame bounds every exactly when for every , equivalently . The least such nucleus is , so preserves arbitrary joins too, including . Evaluation at recovers , so this frame homomorphism is injective.
For the pushout, we prove the universal property explicitly. Let be a frame homomorphism for which every has a complement in . Define, for ,
To prove preservation of arbitrary joins, let be the right adjoint of and set for . This is a nucleus on a frame: inflationarity follows from the adjunction, finite-meet preservation follows from distribution and meet preservation by , and gives ; inflationarity gives the reverse inequality. Complementation and the adjunction now give
The last equivalence uses leastness of . Thus is a left adjoint, so preserves arbitrary joins. For binary meets, expand . A term indexed by is
This proves ; monotonicity proves the reverse inequality. The term at proves . Directly,
For the second identity the term at gives , while every term is disjoint from , because .
Apply this construction first with , , target , and complements . It gives a frame homomorphism satisfying and . Given any compatible pair , , take ; compatibility supplies the required complements. The constructed satisfies and , since the latter equality holds on the open and closed generators of . Uniqueness follows because and generate . Hence the square with edges is a pushout in .
The base ring must be specified in the algebraic definition. For a commutative -algebra , work in and let mean multiplication by . Set and define recursively
These are the operators of order at most . The order of a nonzero differential operator relative to a base ring is the least for which it belongs to ; the zero operator can be assigned order . An operator of order zero commutes with all multiplications and is itself multiplication by , so . The union is the ring of finite-order operators, with composition as multiplication. The identity
and induction on the sum of orders give . Sums have order at most the maximum of their orders, proving that this union is a ring.
For an arbitrary commutative ring, the absolute version uses , so the ambient endomorphisms are additive. For the polynomial ring in this question, the intended Weyl-algebra identification is the relative one with . Absolute operators would also include nonzero derivations of the coefficient field : a derivation on a rational function field in a transcendence basis over extends to its algebraic closure in characteristic zero, and hence to . Extending it coefficientwise to gives an order-one additive operator which is not complex-linear. Such an operator cannot belong to the complex Weyl algebra. This explains why the linearity convention matters.
Now take . Coordinate multiplication has order zero, and each partial derivative has order one because . They satisfy the defining Weyl algebra relations, giving an algebra homomorphism . Reordering spans by . If an ordered expression acted as zero, commutation with the coordinates according to a maximal derivative multiindex would give multiplication by ; removing the top coefficients successively proves that every coefficient is zero. Thus the homomorphism is injective, as in the ordered monomial basis of a Weyl algebra proof.
For surjectivity, let have order at most , and put . The operations commute, since the coordinate multiplications commute. A product of more than of them kills . Define polynomial coefficients
Commuting through repeatedly gives the finite identity
It follows by induction on from and Pascal's identity. Terms with vanish. Since
for , we obtain . The monomials are a complex basis of , so complex linearity yields equality of the operators on all of . Hence
For a nonzero ordered expression , its order is exactly . The upper bound follows from composition; the lower bound follows by taking that many coordinate commutators to extract a nonzero multiplication operator. This describes the order filtration of a Weyl algebra:
The associated graded ring is therefore
The symbol of is . In a product of ordered operators, moving derivatives past coefficients introduces terms of lower differential order. Thus top-order symbols multiply as ordinary polynomials, and the ordered basis proves there are no further relations. In particular , with : the top-order symbols of the two products agree and cancel. Unlike the Bernstein filtration, the order filtration's degree-zero part is the entire polynomial ring and its pieces are infinite-dimensional over .
Form the Rees ring of a filtered algebra
The central element is a non-zero-divisor. This ring is generated by , the , and , with
Its quotient modulo is the associated graded ring just computed. Explicitly the degree- component of is , so the degree- quotient is . The quotient modulo recovers .
Since is commutative, any two lifts of symbols have . Define
Division by is unique because is a non-zero-divisor. If is replaced by , the quotient changes by , which is zero modulo ; changing works the same way. Thus the bracket is well defined. Antisymmetry and bilinearity follow from the commutator. The identity proves the Leibniz rule. For the Jacobi identity, lift each inner bracket by ; the cyclic sum of the outer expressions is the commutator Jacobi identity divided by , hence zero. These verifications prove that the graded polynomial ring is a Poisson algebra. This is the Poisson bracket from a central deformation parameter construction.
The generators give and all coordinate-coordinate and symbol-symbol brackets zero. The Leibniz rule therefore determines the answer on every polynomial:
The sign here follows the chosen convention : in particular , rather than . For homogeneous symbols the bracket has order degree , and can equivalently be written .
A precise version of the Hilbert-Serre theorem is as follows. Let be a commutative graded ring, generated over an Artinian degree-zero ring by homogeneous elements of positive degrees . Let be a finitely generated graded module, bounded below. Each component has finite module length over . Its Poincare series of a graded module, or Hilbert series, is
When is a field, these lengths are dimensions. The theorem asserts
For a nonnegatively graded module the numerator can be taken in . The finite-generation and finite-length hypotheses specify the meaning of the series; they are part of the theorem's statement.
We prove it by induction on . Regard as a finite graded module over , with , acting through the specified generators of . This polynomial ring is Noetherian by the Hilbert basis theorem and Question 1. When , finitely many homogeneous generators over mean that only finitely many components are nonzero, so the series is a Laurent polynomial. For the induction step, put , , and . Both and are finite graded modules; annihilates them, so they are modules over . The finite generation of uses Noetherianity of .
The exact sequence of graded modules
gives, by additivity of component lengths,
Here the shift is defined so that . By induction both series on the right have denominator . Dividing by proves the result. The annihilator term cannot be omitted unless multiplication by is injective.
In the standard grading , the coefficients of are . Multiplying by the finite numerator shows that the component dimensions agree with a polynomial for sufficiently large . Cumulative dimensions have generating function and are also eventually polynomial. This consequence supplies the dimension used for Weyl algebra modules.
Use the Bernstein filtration , in which both coordinate generators and differentiation generators have degree one. The ordered monomial basis of a Weyl algebra gives
Choose a finite-dimensional generating subspace of a nonzero finitely generated left module and set . This is a good filtration of a module: the symbols of the generators generate its associated graded module over the displayed polynomial ring. The Hilbert-Serre theorem makes an eventual polynomial. Define the Bernstein growth dimension of a Weyl algebra module by
The dimension is independent of the chosen finite generating subspace. Each of two finite generating sets is contained in a fixed filtration step for the other, giving and . Such fixed shifts preserve the degree of growth. The same argument applies to any good Bernstein filtration. This dimension agrees with the Gelfand–Kirillov dimension of a module; one may set .
Let the nonconstant element have Bernstein degree . Since is a domain, the product of two nonzero symbols cannot vanish. Hence
Right multiplication by is injective, using the domain property of . Thus the quotient filtration on has cumulative dimensions
The leading terms of degree cancel, and the leading surviving term is
It is nonzero, because . Therefore
Equivalently the Hilbert series of the associated graded quotient is . Here is Bernstein degree, not differential order: multiplication by has differential order zero but Bernstein degree one. Using the order filtration in this dimension argument would lose the finite-dimensional filtration pieces.
A regular element of a ring is an element for which both multiplication maps are injective:
It is thus neither a left nor a right zero divisor; it need not be a unit. Here “ideals” means two-sided ideals. Put , and let denote the specified upper triangular ring.
We first establish the additional facts about the Weyl algebra needed below. Its generators satisfy
Reordering gives a spanning set . These monomials are independent. Indeed, represent the generators by multiplication and differentiation on . In a putative zero operator , choose of maximal total derivative degree. Iterated commutation with multiplication by the coordinates, times in coordinate , gives multiplication by . All other derivative terms of that total degree disappear unless they have exactly the same multiindex, and lower-degree terms disappear. Thus , and descending induction eliminates all coefficients. This proves the ordered monomial basis of a Weyl algebra and faithfulness of its polynomial action.
The Weyl algebra is a simple ring. In a nonzero two-sided ideal choose a nonzero element of least Bernstein filtration degree, where both and have degree one. Commuting it with any generator stays in the ideal and lowers that degree. Minimality therefore makes all these commutators zero. Commutation with every forces all derivative coefficients with to vanish; commutation with every then forces all partial derivatives of the remaining polynomial to vanish. In characteristic zero the element is a nonzero scalar. The ideal consequently contains . This proves simplicity of a Weyl algebra in characteristic zero. Its Jacobson radical is zero, since the radical is a proper two-sided ideal of a nonzero unital simple ring.
Use the two diagonal idempotents to isolate the entries of any ideal of . It must have the form
where all three entries are two-sided ideals of and . Conversely this condition makes the indicated set an ideal. Simplicity says that each is or , and either nonzero diagonal entry forces . Hence the five ideals of are
For a two-sided ideal of , multiplication on both sides by elementary matrices isolates any entry and moves it to any matrix position. The entries obtained form one two-sided ideal of , and the original ideal is . Thus the only ideals of are and .
Since , lies in the Jacobson radical of : for and , and has inverse . On the other hand, has zero radical, so the image of the radical in this quotient is zero. The elementary unit criterion for the Jacobson radical justifies both assertions. Therefore
The second equality follows from simplicity of .
We now construct the denominators used to describe regular matrices. A left Noetherian noncommutative domain satisfies the left Ore condition. For if for two nonzero elements, the left ideals have direct sum: in a relation the first summand lies in , all the others in , so it vanishes; cancellation of the final repeats the argument. Their finite partial sums form a strictly ascending chain, contradicting left Noetherianity. Thus , giving common nonzero left multiples and the required Ore equations. The analogous argument with right ideals gives the right Ore condition under right Noetherianity. Both hypotheses for are allowed in the question.
The Ore localization therefore embeds in a division ring . Briefly, its elements are left fractions , with nonzero , and two fractions are identified after passing to a common left denominator. Common multiples supply addition and multiplication, while cancellation in the domain makes the embedding injective. A nonzero fraction has an inverse, obtained by interchanging its numerator and denominator in the appropriate Ore fraction calculation. The right fraction construction gives the same division ring, so finite lists have common left and common right denominators.
A triangular matrix with is invertible over , with inverse
It is consequently regular over . If , then ; if , then . Hence
A full matrix is regular exactly when it is invertible over :
One implication follows immediately from invertibility. Conversely, a singular matrix over a division ring has a nonzero right kernel column and a nonzero left kernel row, by row reduction. A common right denominator turns the column into a nonzero column over , providing a right annihilator matrix over . A common left denominator does the same for the row and gives a left annihilator. Thus a singular matrix is not regular. Explicitly, for with , row elimination says that regularity is equivalent to in . If , it is equivalent to both and . A commutative determinant formula must not be substituted here.
Finally both classical left rings of quotients exist, and
To prove this directly, clear a common left denominator from all the finitely many entries of a matrix over . It becomes with in the original triangular or full ring and regular. Every original regular element becomes a unit in the corresponding ring over , by the descriptions above. For regular and in the original ring, write in this way; then , the left Ore condition. Since the denominators are regular, the additional annihilator condition for localization is automatic. This proves the matrix and triangular localization over an Ore domain assertions. In particular, the nonzero nilpotent radical of the triangular ring does not prevent its classical localization; that localization retains the triangular radical.
Put , and let be any ideal of this formal power series ring. For define an ideal of by
Multiplication by shows . Since is Noetherian, this chain stabilizes at some , and each is finitely generated. For every , choose finitely many series whose degree- coefficients generate .
Given , cancel its degree-zero coefficient using the , then its degree-one coefficient using the , and so on. At a degree , use . Each residual remains in and has zero coefficients below the next cancellation degree. For each of the finitely many chosen , accumulate its multiplier into a formal power series . The higher-degree increments of these multipliers converge coefficientwise. At every degree the cancellation procedure gives the exact coefficient identity, so
Thus the finitely many lifts generate as an actual ideal. No assumption that is closed has been used. This proves Noetherianity of formal power series rings:
Iterating the argument proves the assertion for , which is naturally the iterated formal power series ring.
For a surjective module map , define the adic completion of a module by
Take and choose representatives for its components. Compatibility says . Choose with . If , surjectivity gives , so choose with and put . The classes of modulo are compatible and map to the chosen components of . Hence
This surjectivity on adic completions does not require finite generation of or . The compatibility of the lifts is the point; independent lifts of the finite-level classes would not suffice.
Since is Noetherian, write . Define a ring homomorphism
Modulo , evaluating a series requires only its finitely many terms of total degree below . These evaluations commute with the reduction maps, and define without needing the original ring to be complete or separated.
To prove surjectivity, begin with . Choose matching its component modulo . After terms of total degree below have been chosen, their evaluation differs from at level by a class in . This class is an -linear combination of the monomials with . Choose the corresponding homogeneous degree- polynomial as the next term. Then the series evaluates to at every level. This proves the power-series presentation of an adic completion, and therefore
A quotient of a Noetherian ring is Noetherian, since its ideals correspond to ideals containing the kernel. The cases and give and , respectively, and satisfy the conclusion as well.
Let be a commutative Artinian ring. We prove finite composition length first, without assuming the conclusion that is Noetherian.
Every prime ideal is maximal. Indeed, an Artinian integral domain is a field: for , stabilization of gives , and cancellation gives . There are only finitely many maximal ideals. To see this, choose a minimal finite intersection using the descending chain condition. Minimality gives for any other maximal ideal . Since , primeness forces one , and maximality makes them equal. Thus the Jacobson radical is this finite intersection, and the Chinese remainder theorem gives
We also need nilpotence of . Its powers stabilize; put at a stabilization stage, so . If , choose an ideal minimal subject to . Since , minimality gives . Choose with . Minimality applied to the subideal gives . The equality then yields for some . But is a unit by the unit criterion for the Jacobson radical; hence , a contradiction. Therefore .
Each layer is an Artinian module over the finite product of fields . Its components over those fields are finite-dimensional: an infinite-dimensional vector space has a strictly descending chain of subspaces. Each layer consequently has finite composition length. The finite filtration
proves that itself has finite composition length, and therefore satisfies the ascending chain condition on ideals. Every commutative Artinian ring is Noetherian. The zero ring satisfies the conclusion trivially.
The relevant Artin–Wedderburn theorem says that a semisimple ring which is a right Artinian ring has the form
where the are division rings and the positive integers and division rings are unique up to permutation and isomorphism. The division rings need not be commutative or finite-dimensional over a field. Conversely every such finite product is semisimple and a right Artinian ring.
Here is a proof which also works if semisimplicity is initially expressed as . A nonzero right ideal contains a minimal nonzero right ideal by the descending chain condition; is a simple module. If , then for every and , , so has inverse . The unit criterion for the Jacobson radical would give , a contradiction. Thus some induces a nonzero map by left multiplication. This map is an isomorphism, since is simple. Choose with . Then and injectivity on gives . We obtain and the splitting
For a right ideal containing , the same argument splits . Repeatedly split a minimal right ideal out of the remaining summand. The remaining summands form a strictly descending chain of right ideals, so the process terminates. Thus
for pairwise nonisomorphic simple modules .
A nonzero map between simple modules is an isomorphism: its kernel and image leave no alternatives. Thus is a division ring, and for . This is the needed Schur lemma. Taking endomorphisms of the direct sum gives . Finally, left multiplication identifies with : a right-module endomorphism sends to , and composition corresponds to multiplication in , not its opposite. This proves the displayed ring isomorphism.
For the converse, the right regular module of is the direct sum of its row modules. Each row module is simple, since elementary matrices and nonzero scalar inverses send any nonzero row to any prescribed row. A finite product therefore has a finite semisimple regular module and is a right Artinian ring. The simple-module multiplicities and their endomorphism division rings recover the factors, establishing uniqueness.
For Fodor's theorem, let be regular uncountable, stationary, and regressive: for every nonzero . A club set is unbounded in and closed under limits below ; a stationary set meets every club. Removing preserves stationarity. We prove that some fibre of is stationary, not merely that one fibre is large.
We first check the club facts used in the argument. An intersection of fewer than club subsets of is club. Closure is immediate. For unboundedness, given and clubs with , choose an increasing sequence starting above , such that is above a point of every beyond . Regularity bounds the supremum of the fewer-than- points at each step. Then , and the chosen points in each are cofinal in ; closure puts in their intersection.
For a sequence of clubs its diagonal intersection
is also club. To obtain a point above , recursively choose in , possible by the preceding result, and take the supremum of the sequence. For each , every sufficiently late belongs to , so . For closure, if diagonal-intersection points are cofinal in , then for each their sufficiently late points lie in , and closure again puts there.
Suppose every fibre were nonstationary. Choose a club disjoint from each fibre. Stationarity supplies , with . Put . By diagonal membership , but by its definition , a contradiction. Thus
This is precisely the pressing-down assertion. Regularity and uncountability were used to keep the club-building suprema below .
For the Cantor normal form theorem, every nonzero ordinal has a unique expression
All operations are ordinal operations, so the order of the terms matters. The ordinal zero has the empty expression. We give the greedy existence proof and then prove uniqueness.
The powers are strictly increasing and continuous at limit exponents, and satisfy . Hence the set of exponents with is nonempty and bounded, and its supremum belongs to it by continuity (or is already its last successor member). Thus there is a largest such exponent and
Since the last product is the supremum of the finite multiples, there is a unique positive finite satisfying
The initial segment of of length leaves a tail of unique order type , so
The bound follows from strict increase of ordinal addition in its right argument: a tail at least would contradict the preceding interval. This is the relevant instance of the ordinal division algorithm.
If , apply the same construction to it. Its leading exponent must be below . Continue with the remainder. An infinite continuation would produce an infinite strictly descending sequence of ordinals, impossible by well-foundedness. Thus the process terminates after finitely many steps and gives the required form.
To prove uniqueness, first observe that a finite decreasing-exponent suffix with leading exponent is smaller than . This follows by induction on its number of terms: the later tail is below , so adding it to a finite multiple of stays below the next finite multiple and hence below . Consequently the tail after a term with exponent is below .
Any proposed normal form therefore places in exactly the interval
Its first exponent is recoverable as the largest exponent whose power does not exceed , and its first coefficient is recoverable as the largest finite multiple not exceeding . The right remainder is unique because ordinal addition is strictly increasing in its right argument. Apply the same reasoning to the remainder, successively fixing every exponent and coefficient. This proves uniqueness without treating ordinal addition as commutative or cancelling arbitrary left summands.
A complete type over is a maximal consistent set of first-order formulas in a fixed finite tuple of variables with parameters from , consistent with the theory of that parameter expansion. A first-order model is a saturated model of degree if every such type with is realized in . It suffices to require this for one-variable types and realize a finite tuple successively. Without a subscript, saturated commonly means -saturated; some contexts specify only finite-parameter saturation. We state the degree explicitly.
The saturated elementary extension theorem says that every first-order structure has a -saturated elementary extension for any specified infinite . It suffices to prove this for regular , since a larger regular degree implies the requested degree. At a single stage , list all complete one-variable types over all subsets of of size below . This collection is a set. Adjoin a witness constant for each type to the elementary diagram of and require that constant to satisfy its type. Every finite subset is satisfiable in : each type's finite conjunction has a witness there, and the finitely many new constants have no cross-constraints. The compactness theorem gives an elementary extension realizing all these types simultaneously.
Repeat this step along an elementary chain , taking unions at limit stages, and let be its union. The elementary chain theorem follows here by induction on first-order formulas: an existential statement true in the union has a witness in a later stage; elementarity brings an existential witness back to the earlier stage containing its parameters. Thus each stage is elementary in .
If has size below regular , all its elements lie in a single , by taking the supremum of their fewer-than- stage indices. Any complete type over consistent with is already consistent over , since these structures have the same parameter theory. It was therefore realized in . This proves -saturation of .
A corresponding theorem about full saturation is available with a stated cardinal-size hypothesis: if is uncountable regular, , and , then every infinite first-order model of size at most has an elementary extension of size which is -saturated. First adjoin pairwise distinct constants to the elementary diagram; every finite fragment is satisfiable because the original first-order model is infinite. A Skolem hull of their realizations and the original domain has size . There are at most small parameter sets and at most types over each of them. Compactness and the downward elementary-submodel construction keep each realization stage of size . Taking a Skolem hull of the preceding stage and the chosen witnesses closes under at most finite terms and proves this size bound and elementarity. The same length- chain is consequently a fully saturated model of size . The cardinal hypothesis is not silently asserted to hold for every cardinal.
We now prove consistency of NFU by the permitted alternative method of indiscernibles and a domain-shifting structure automorphism. This can start from an explicit set structure available in ZFC, so we need not assume that there is a first-order model of all ZFC. Let
and give the value off the natural numbers. Regard as a first-order structure, with a named object . The graph of is an external set in the metatheory; it need not be a member of . This structure is extensional and satisfies every separation instance in the pure membership language: any subset of has rank below and belongs to . It also satisfies, for natural ,
since a subset of has rank at most and hence belongs to .
Apply the indiscernible construction proved in question 7(i) to a Skolem expansion of this set structure, requiring to be increasing members of its named natural-number object. For every finite fragment use an increasing sequence of ordinary natural numbers in the initial structure in the Ramsey argument. The resulting generated elementary hull has an external structure automorphism with , preserving and the named . Put and . Then , and satisfies the displayed subset-containment assertion between successive domains. No claim that satisfies replacement is required.
All membership and subset statements about these objects are interpreted inside . The hull is necessarily externally nonstandard: the natural-number objects give an external descending chain. The external structure automorphism is not an object that must be definable within that first-order model.
On the external domain define
This is the rank-shifting NFU model with explicit set predicate. The guard is essential: an object not contained in could still have some ordinary members in , and must not thereby become a nonempty atom. The objects failing have no -members. If two objects satisfying have the same -members, their images under are subsets of with the same members, so extensionality in and injectivity of make the original objects equal. Thus set-extensionality and the atom condition hold.
It remains to prove every comprehension instance. Use the domains just constructed, equivalently , for integer sorts. The map is a bijection from the objects of to the objects of , and every subset of that exists in is an element of . In sort define the set predicate by ; from sort to define membership by ordinary membership guarded by .
For a stratified formula, assign integer types to its variables with equal types for equality and adjacent types for membership. Shift all types uniformly if necessary so the finitely many used types are nonnegative. Replace a variable of type by of its untyped value, quantify it over , and use the typed relations just described. Applying to the untyped definition shows that each atomic first-order formula has the same truth value under this translation; induction on connectives and quantifiers proves the same for the whole first-order formula. Importantly the translated first-order formula is an ordinary first-order formula of with finitely many domain and transformed-parameter constants, not a first-order formula containing the external structure automorphism as a predicate.
If the comprehension variable has type , separation in produces its extension . The subset-containment assertion gives . Put . Then , hence , and for every ,
This verifies stratified comprehension with arbitrary parameters. The empty extension gives a distinguished empty set; the always-true first-order formula gives a universal set. The unstratified Russell predicate is not an allowed comprehension instance. Thus
Starting from the actual set structure and applying compactness constructs a set first-order model, so this is a consistency proof in ZFC, not merely an assumption of Con(ZFC). It proves the requested consistency with an explicit interpretation; it does not depend on treating the much stronger full extensionality of NF as already consistent. The external is a tool of the construction, not an extra symbol permitted in NFU's comprehension scheme.
Here a monochromatic set must mean an infinite homogeneous set for a colouring: every singleton is a finite monochromatic set. The requested phenomenon holds for every finite . For it is impossible, since the colour classes of a finite computable colouring are computable and at least one is infinite. We treat this necessary qualification explicitly.
We construct a finite-injury computable colouring of pairs with no infinite computably enumerable homogeneous set, which is stronger than the requested absence of a recursive one. Enumerate the computably enumerable sets as , with computable finite approximations . Requirement seeks distinct markers . At stage , consider indices not currently assigned markers. Choose the least one, if any, for which has two elements outside all markers of higher-priority indices . Assign two such elements as its markers, using a fixed least-element rule, and cancel all markers at lower-priority indices. Do nothing if no such index exists. The active markers are therefore pairwise distinct at every stage.
For , simulate this finite construction through stage and define
In particular every active first marker has colour zero against larger points. This is a total computable function: no question about eventual enumeration or eventual stabilization is used in computing a given pair.
Induction on proves finite injury. Once the finitely many higher requirements have stabilized, requirement is never cancelled again. If it has markers they stay fixed. If is infinite, it eventually supplies two points outside the finite collection of higher markers, so it becomes eligible and is assigned markers; only finitely many higher indices could delay its assignment. Thus an infinite eventually has permanent distinct markers . Choose beyond both markers and beyond their stabilization stage. Then
So is not homogeneous. Every infinite recursive set is computably enumerable, proving the desired obstruction. For , colour an increasing -tuple by the pair formed by its first two elements. Every pair from an infinite homogeneous candidate can be completed by larger members of that candidate, so it would give an infinite pair-homogeneous set, already ruled out.
The uncountable positive theorem is the Erdős-Rado theorem for finite arities. For every infinite cardinal and finite , define and . Then
The partition relation means that every colouring of -element subsets of the left-hand cardinal by at most colours has a homogeneous subset of size . In particular, taking gives an uncountable homogeneous set for every finite arity, once the domain is sufficiently large.
We prove the end-homogeneity lemma needed for induction. Let be infinite, , finite, and with . In a sufficiently large choose an elementary substructure of size containing and all ordinals below , and closed under externally given sequences of length at most . Here consists of sets whose transitive closures have size below .
To justify that closure, begin with a hull containing the indicated parameters and ordinals. At each successor stage add every sequence of length at most from the preceding stage, then take a Skolem hull. There are at most such sequences. Iterate for stages and take elementary unions at limits. The union still has size , and every sequence of at most of its elements is contained in one earlier stage by regularity of , so appears at the next. This proves the claimed closed first-order model rather than assuming its existence.
Let . The inequality uses regularity of and ; has no largest element, since it is closed under successor. Recursively choose increasing for , imposing, for every -tuple of earlier points,
At any stage there are at most earlier points and constraints. Each constraint consists of a tuple of elements of and a colour below , also in . The entire constraint code therefore belongs to by closure. The bound above the previous points belongs to as well. Although itself need not belong to , it witnesses in the existence of a point above that bound satisfying the coded constraints. Elementarity supplies such a point inside . This proves the recursion.
On the resulting sequence of length , the colour of an -tuple depends only on its first entries: its last entry has the same colour contribution as . This is the required closed elementary-submodel construction of an end-homogeneous sequence.
Now prove the theorem by induction on . The case is the infinite pigeonhole principle: partitioning into at most classes of size at most cannot cover it. For , set and apply the lemma to the colouring on . Define a colouring of -tuples from its end-homogeneous sequence of length by their colour when completed with . The induction hypothesis supplies a subset of size on which this derived colouring is constant. Every original -tuple from that subset has the derived colour of its first entries, and is therefore monochromatic. This completes the proof.
The unrestricted infinite-exponent situation is very different under AC. On , choose one representative of each equivalence class modulo finite symmetric difference, and colour by
If is infinite and , deleting remains in the same equivalence class and flips the colour. Every infinite candidate homogeneous set contains such an and as subsets, so
More generally the same argument works for subsets of any fixed infinite cardinality: deleting one element preserves that cardinality, so there is no unrestricted analogue with a homogeneous set large enough to contain such subsets. For the order-type- convention, choose in increasing order type and delete its first element; both sets still have that order type. Thus the distinction from the finite-arity theorem is genuine, not merely a notational ambiguity. This argument uses choice of representatives and is not a claim about every definability-restricted infinite-arity colouring.
An inner model of a universe of ZF is a transitive class containing every ordinal and satisfying the required set-theoretic axioms with the inherited membership relation. Transitivity means that every member of a member of belongs to . Requiring all ordinals distinguishes an inner model from a transitive set first-order model such as : a set first-order model has bounded ordinal height. One may specify an inner model of ZF, ZFC or a stronger theory; choice is not built into the term unless specified.
The fundamental example is the constructible universe. Form the constructible hierarchy
Here definable power set means subsets definable over the set structure by first-order formulas with finitely many parameters from that level. Each level is transitive, the levels increase, and , by induction. Thus is transitive and contains all ordinals.
The construction supplies a definable well-order: order objects first by their earliest construction stage, then by a least first-order formula code and a finite tuple of parameters in the already constructed level's well-order. Recursively extend the earlier well-order at each successor stage and unite compatible orders at limits. First-order formula codes and finite tuples of well-ordered parameters are well-orderable. This yields a canonical global ordering definable within ; its restrictions to sets will give choice once the ZF axioms are checked.
For that check, a useful reflection argument is explicit. Given finitely many first-order formulas and a starting level, pass to a higher level containing witnesses for their existential subformulas on all parameter tuples from the current level, choosing least witnesses in the canonical order. There are set-many tuples, so ambient replacement bounds their witness stages. Repeat for steps and take the union level . Every relevant witness with parameters in that level appears at a later step. Induction on first-order formulas, with this witness property for the existential case, proves that reflects the chosen finite list of first-order formulas of .
Separation on a constructible set is then definability over a sufficiently large reflecting level, so its subset appears at the next level. For replacement, reflect the first-order formula specifying a functional image and its required existence statements. All inputs belong to a level containing the domain as a set; all their unique outputs then lie in one reflecting level. The image is definable there and hence is constructible. For power set, the ambient set of constructible subsets of has bounded construction stages by replacement in the ambient universe. At a level containing them all, this internal collection is definable by the bounded condition , and therefore is itself in . Pairing, union and axiom of infinity follow directly from definability over sufficiently large levels, while extensionality and foundation follow from transitivity. Thus , and its canonical ordering gives .
This proves the important relative-consistency application
One does not conclude that choice is true in the original universe. Instead the inner model supplies a possibly smaller universe in which choice holds.
Constructibility also supplies GCH. Here is the cardinal-counting argument, making clear the role of the condensation lemma for the constructible universe. Work inside . If is constructible, take a large limit containing and an elementary hull of of size . Its transitive collapse is by condensation. The collapse fixes every ordinal below , and hence fixes and . Since the hull has size , . Therefore every constructible subset of appears below .
The condensation fact expresses the rigidity of this definability construction: first-order formula codes, finite parameter tuples and satisfaction in set-sized lower levels are preserved by the collapse. Inducting over the hull's ordinal indices identifies each collapsed lower level with the corresponding -level; elementarity supplies every definable subset coded by parameters in that collapsed lower level. Taking unions identifies the entire collapsed hull with a level .
Induction on construction stages gives : each successor has only countably many first-order formula schemes with finite parameter tuples, and limits take unions. Hence for infinite . The preceding containment gives in , and Cantor's theorem gives the reverse inequality. Consequently
All these cardinal computations are internal to ; they need not equal the ambient cardinal computations.
Inner models are also useful for analyzing stronger axioms. If is inaccessible in , it remains an uncountable regular cardinal in , because a shorter cofinal sequence in would already be one in . For each ordinal , its constructible subsets are fewer than even in the internal cardinal comparison: in , has size below , so its constructible part cannot have an -well-order of length at least . Thus it remains strong limit. Accordingly supplies relative-consistency information compatible with inaccessibles and GCH. Stronger embedding or measure properties require extra analysis, since the witnessing objects may disappear upon passing to an inner model.
There is a useful limitation: no uniform inner-model construction can refute choice from every starting ZF universe. Every inner model of ZF contains the ambient . Indeed, induction gives : the same set-sized level has the same satisfaction relation for definitions, and limit stages take the same unions. If the starting universe already satisfies , any inner model containing all ordinals must therefore be the whole universe, where choice holds. To obtain a choice-failing first-order model uniformly one needs a different method, such as the symmetry restriction in the preceding solution. Inner-model arguments establish consistency and preservation through carefully controlled smaller universes; they do not freely manufacture arbitrary desired axiom failures.
All independence assertions here are relative consistency results. Begin with a first-order model of ZF; for the choice-preserving side use ZFC. The original first-order model already gives the side where foundation holds. We construct the opposite side while checking the other axioms, then add a symmetry restriction to make choice fail.
Let , and let interchange the old objects and , fixing everything else. They are distinct. On the same domain define the Rieger-Bernays permutation model by
Write ; the -members of are exactly the old members of . In particular , and has no other -member. Thus is a Quine atom, and the nonempty -set has no member disjoint from itself. Foundation fails.
Here are the other axioms explicitly. Equal -extensions imply by old extensionality, hence . An -pair of is . An -union of is
Its elements are precisely objects with an -membership chain of length two into . The -power set of is
since means . These are old sets by power set and replacement.
Translate any first-order formula by replacing its membership symbol with , a definable relation with parameter . Separation on produces the representative of the old set . For replacement, functionality in the new structure is exactly functionality of the translated first-order formula on the old set ; old replacement gives its range, and represents that range as an -set. Thus the full schemas, not merely their quantifier-free instances, survive. The old finite ordinals and are fixed by , so their empty-set and successor relations are unchanged; the old witnesses axiom of infinity.
If the original first-order model satisfies AC, the new one does too. For an -family of nonempty -sets, old choice selects for each . The -ordered-pair construction is definable, so old replacement forms the graph of this selection in -pair codes; applying makes it an -function. It chooses an -member from each member of the family. Therefore a full membership permutation alone does not refute choice. We have proved
with choice preserved if it was initially present. Together with the unchanged well-founded first-order model, this proves foundation's independence from the remaining axioms.
For the choice-failing extension, work in an ambient first-order model of ZFC and build the extensional cumulative universe over Quine atoms. Let be a countably infinite collection of distinct tagged objects. Give each the membership extension . Adjoin sets in successive construction ranks, representing a set-sized collection by a unique new tagged object with extension , except that the representative of is the already existing . Denote this representative by again. Thus ; adjoining a second, distinct ordinary singleton would incorrectly violate extensionality.
More formally take atom tags of kind zero, put , and define
The extension of is , and the extension of an atom is . Tags of the two kinds are disjoint. Any set-sized collection of objects has bounded construction ranks and hence a representative at a later stage. This proves pairing, union, power set, separation and replacement by representing their extensions, just as above. For axiom of infinity, recursively construct the pure finite ordinals, collect these representatives in an ambient set by replacement, and apply to that collection. The resulting inductive set is fixed by every atom permutation. Every object has a unique extension, so full extensionality holds, although foundation fails at the atoms.
Let be the full symmetric group of . Extend by , recursively on the non-atomic construction ranks. This preserves membership, including the atomic self-loops. An object is supported by a finite if every permutation fixing pointwise fixes it. Retain the hereditarily finite-supported Quine-atom model : every object reachable from a retained object by finitely many membership steps has finite support. In particular all members of a retained object are retained, every atom is supported by itself, and is supported by the empty set.
We verify the schemas in , rather than assuming that an arbitrary invariant class is a first-order model. For separation, a subset of a retained set definable in from parameters is fixed by permutations fixing the union of their finite supports. Its members are already in , so its representative belongs to . For replacement, a definable functional image of is a set in the ambient universe. Uniqueness makes it invariant under every permutation fixing and the parameters, although the individual outputs can have different supports. Those outputs are in by the relativized first-order formula, so the range representative is hereditarily supported. This proves replacement without falsely requiring one finite support for every individual value.
The internal power set is the representative of
It is an ambient set and is fixed by the support of , because a permutation carries retained subsets of to retained subsets of . Every member is retained by its definition. This proves the internal power-set axiom. Finite unions of supports handle pairing and union; the pure natural numbers have empty support; extensionality is inherited because is membership-transitive. Hence satisfies all ZF axioms except foundation, which still fails.
In form the family of all two-element subsets of , a family with empty support. Suppose it had a choice function , with finite support . Choose distinct . Their transposition fixes and the argument , but interchanges its two possible chosen values. Equivariance gives a contradiction. Thus
The full construction over , before restricting to , has choice by ambient choice and the representability of choice graphs. Alternatively an ordinary ZFC first-order model gives the positive choice side. This proves the independence of AC from ZF minus foundation. The required metatheoretic consistency can be expressed using Con(ZF), since the constructible universe of a ZF first-order model supplies ZFC, as explained in the next solution. No assumption of a transitive model follows from mere consistency or is needed for these interpreted first-order model constructions.
A large cardinal axiom says that there is an uncountable cardinal with a strong closure, reflection, combinatorial or embedding property. Its interest is not merely the magnitude of the cardinal: it packages a universe-like portion of set theory, or a coherent way of comparing the universe with a proper inner model. Such axioms form a hierarchy extending ordinary ZFC, compared through relative consistency implications. The consistency qualifications are essential; an existence axiom is not a theorem of ZFC simply because its consequences are attractive.
The basic example is a strongly inaccessible cardinal: an uncountable regular cardinal which is a strong limit cardinal, so
These conditions imply for every . Prove this by induction along the cumulative hierarchy: the successor step uses the strong-limit property, and a limit step uses regularity to bound a union of fewer than smaller sets. Thus every member of has cardinality below .
Consequently is a transitive model of ZFC. Pairing, union, power set, separation, axiom of infinity and foundation stay within the hierarchy. For replacement, a definable function on has fewer than values; regularity bounds their ranks below , putting the range in . Ambient choice supplies a choice function for a family in , and its graph also has bounded rank. This verifies the substantial closure axiom rather than only saying that the rank is large. It also shows why inaccessible existence cannot be proved in a consistent ZFC: it would yield a set first-order model of ZFC and hence its consistency, contrary to the Gödel second incompleteness theorem.
An uncountable regular limit cardinal is a weakly inaccessible cardinal; requiring the strong-limit inequality is stronger without additional hypotheses. Under GCH, every smaller infinite cardinal satisfies , so the two notions coincide. This distinction separates cardinal-arithmetic assumptions from the regularity requirement.
A Mahlo cardinal is an inaccessible whose inaccessible cardinals below it form a stationary set. Thus every club set meets those inaccessibles, which strengthens mere unboundedness. There are inaccessible ; is a first-order model of ZFC containing an inaccessible . Mahloness therefore supplies a consistency statement stronger than the bare existence of one inaccessible. Iterating the demand that smaller cardinals have the same reflection property leads to further levels of the hierarchy.
A weakly compact cardinal is a logical and combinatorial strengthening of inaccessibility. One standard characterization is an inaccessible with
every two-colouring of pairs has a homogeneous subset of size . Equivalently one can use compactness for theories of size at most , or the tree property at an inaccessible. These viewpoints explain the terminology: a local collection of compatible requirements has a global realization, and tall narrow trees cannot avoid cofinal branches. They are characterization statements; the elementary closure and measure arguments below are separate proofs of the consequences used here.
A measurable cardinal carries a nonprincipal kappa-complete ultrafilter on . Every set of size less than is -null, since it is a union of fewer than null singletons. Such a cardinal is regular: a cofinal sequence of length would partition into bounded, hence null, pieces; completeness would make their union null, an impossibility.
It is also strong limit. If and there were distinct sets for , choose for each the -large side of the partition according to whether . The intersection of these fewer than large sides belongs to , but all its indices designate the same subset of , so it has at most one member. This contradicts nonprincipality. Hence , proving that every measurable cardinal is inaccessible.
The measure gives an ultrapower embedding. Form equivalence classes of functions under equality on a -large set, with membership defined coordinatewise modulo . Induction on first-order formulas proves elementarity: Boolean operations use the ultrafilter laws, and the existential step chooses coordinate witnesses on a large set. Countable completeness makes the ultrapower well-founded. An infinite descending membership chain would give countably many large coordinate conditions; their intersection would produce an actual infinite membership descent in . Collapse the ultrapower to a transitive class , obtaining .
For , every function into is constant on a large set by completeness; induction shows . The class of the identity function is larger than every such constant ordinal and lies below , so . Thus the critical point of an elementary embedding is . The measure viewpoint has become a precise self-similarity principle for the universe.
A supercompact cardinal imposes arbitrarily strong closure on these embeddings: for every there is with critical point , , and . It implies measurability by the derived ultrafilter
Elementarity makes this an ultrafilter; fixed ordinals below show that singletons are null. For , fixes the indexing length, so it carries an intersection of sets to the intersection of their images. If all these images contain , so does their intersection, proving -completeness.
These examples illustrate three connected uses of large cardinals: obtaining set first-order models and stronger consistency statements, extending finite or countable compactness and partition phenomena to uncountable domains, and constructing elementary embeddings with controlled closure. They also interact with inner models: an inaccessible remains inaccessible in the constructible universe, since it cannot acquire a new short cofinal sequence there and there are fewer subsets of smaller ordinals. A measurable cardinal's measure need not belong to that inner model, so preservation of the stronger property is a different issue. Large cardinal axioms are thus structured additional hypotheses, with carefully distinguishable consequences and relative-consistency claims, rather than a single claim that sufficiently big cardinals exist.

There are unlisted articles, also show them or only show them.