Put , the power object, with acting by inverse image of predicates. Transposing a predicate on gives natural bijections
Thus is left adjoint to . Its unit sends to evaluation at , namely the predicate . This unit is monic: two generalized elements having the same evaluation on all predicates agree by testing the singleton predicate of the first, or equivalently its graph in the relevant parameter product.
We verify a sufficient form of Beck's monadicity theorem: a right adjoint is monadic if it reflects isomorphisms and its domain has, and it preserves, coequalizers of reflexive pairs. Suppose is invertible. Then is invertible, and naturality of the monic unit shows that is monic. Regard it as the subobject . Its characteristic predicate and the constantly true predicate have the same restriction to , so injectivity of makes them equal. Thus this subobject is all of , and is invertible. Hence reflects isomorphisms.
A reflexive pair in is a coreflexive pair in , with a common retraction such that . Its equalizer exists. We show that is the coequalizer of . Direct image of subobjects along the mono defines , and similarly . At every parameter object the identities are
For the middle identity, an equality forces after applying ; their common point must therefore lie in the equalizer. This proves the identity for parameterized predicates, not merely for global elements. If satisfies , composing with gives . Thus it factors through , and the last displayed identity gives uniqueness. This proves that power objects turn coreflexive equalizers into coequalizers. All hypotheses of the monadicity criterion have now been checked, so is monadic, with
A logical functor preserves finite limits, exponentials and the classifier, hence gives compatible natural isomorphisms and . They respect units and multiplications, because these are defined by evaluation and transposition. Under the displayed equivalences, is therefore the induced functor on double-power Eilenberg-Moore categories. Their forgetful functors create finite limits, and the underlying preserves them. Consequently the induced functor preserves finite limits, so does too. Reversing arrows proves every logical functor preserves finite colimits.
For the first counterexample, the constant-terminal functor has the constant-empty functor as left adjoint: both sets of maps in the adjunction are singletons. It preserves exponentials, since with the canonical comparison. It does not preserve the initial object, because . Thus preservation of exponentials alone is insufficient.
For the second, take the fixed-point functor for . Its left adjoint gives a set the trivial action. The classifier of -sets is the two-element set with trivial action, so preserves it and its truth map. Let be the free two-element -set. The coequalizer of its identity and its swapping automorphism is the singleton -set. Applying gives two maps followed by , whereas their coequalizer in sets is . Thus preserves the classifier but not all finite colimits. These examples also explain why both requirements in logicalness matter.
For a small category , write . Its objects are categorical presheaves and its arrows natural transformations. The terminal presheaf is the constant singleton, and products and equalizers are computed objectwise. Their restriction maps are induced by the corresponding set operations, so the objectwise universal properties are natural and give finite limits in .
For presheaves , define the exponential object by
For , restriction precomposes with . Evaluation sends at to . Given , its transpose sends to the transformation whose component at is
Naturality of proves this is a natural transformation and that the assignment is natural in . Conversely evaluation reconstructs . These constructions are inverse, proving the exponential universal property explicitly.
For the subobject classifier, let be the set of sieves on a category on and let take inverse image of sieves on a category. The truth map selects the maximal sieve on a category at every stage. A monomorphism of presheaves is objectwise injective, so identify it with . Define
This is a sieve on a category, and restriction gives precisely inverse image, so is natural. Its value is maximal exactly when , by testing the identity arrow. Thus is its pullback of truth. Uniqueness follows since membership of is detected by whether the restriction to is true. Smallness of makes all the displayed components and natural-transformation sets genuine sets. Hence is an elementary topos.
The same constructions work componentwise under the weaker slice hypothesis. Indeed,
A component on is simply a map , with the naturality conditions for triangles in . Restricting to a small skeleton of an essentially small slice therefore makes this a set; the result determines the maps on all isomorphic slice objects. Likewise a sieve on a category on is a full downward-closed collection of objects of , determined by its intersection with that small skeleton, so the collection of sieves on a category is a set. The restriction, evaluation and classifier proofs above are unchanged. This establishes the slice-small presheaf construction.
For an example, take a discrete category with one object for every ordinal and no arrows other than identities. Each slice is the terminal category, but there is a proper class of pairwise nonisomorphic objects, so it is not equivalent to a small category.
The large-category assertion needs a universe convention. The constructions give all elementary-topos axioms in a larger universe in which those diagrams and their transformations are admitted. They do not imply local smallness in the original universe: for the discrete example, transformations from the constant singleton to the constant two-element presheaf are arbitrary ordinal-indexed binary families and do not form a set there. If “topos” is required to be locally small relative to that original universe, the unrestricted large-category assertion is false. With the usual larger-universe interpretation, the explicit component constructions prove the intended result; no assumption that the original category itself is essentially small is needed.
A regular category has finite limits, factorizations of every arrow as a regular epimorphism followed by a monomorphism, and pullback-stable regular epimorphisms. Equivalently one may require coequalizers of kernel pairs and pullback stability of the resulting quotients. A regular epimorphism is a coequalizer of some parallel pair; an extremal epimorphism is an epimorphism such that , with monic, forces to be invertible.
First, every regular epimorphism is extremal without assuming regularity of the whole category. Suppose coequalizes and . Since is monic, , so the universal property gives with . Then ; cancellation of the epimorphism gives . Monicity of now gives , so is an isomorphism. Conversely, in a regular category, factor an extremal as with regular epic and monic. Extremality makes invertible, so is regular epic. Thus covers and regular epimorphisms coincide.
For a counterexample, work in the category of small categories, which has finite limits constructed on objects and arrows. Let be two disjoint walking arrows and . Let be the walking isomorphism, with two objects and inverse arrows , . Define by , , , . These images generate all of , so two functors agreeing after agree everywhere; thus is epic.
A monic functor is injective on objects and faithful, as tested by functors from the terminal category and from the walking arrow. If factors through such a functor , its image contains both objects and both arrows . Faithfulness forces their lifted composites to be the identities, so the image contains every arrow of and is an isomorphism. Hence is extremal.
It is not regular. Its kernel pair identifies the endpoint pairs and but has no relation forcing the composites of the images of to be identities. Concretely, send all four objects to the one-object category with endomorphism monoid , , and send both to . This functor equalizes the kernel pair: corresponding identities agree, and the only nonidentity arrow pairs in the kernel pair are an arrow paired with itself. It cannot factor through , because images of would have to be inverse, whereas . In a category with kernel pairs, every regular epimorphism is the coequalizer of its kernel pair: its original coequalized pair factors through that kernel pair, giving the universal property. Therefore is an extremal but nonregular epimorphism, the promised nonregular extremal epimorphism in the category of categories.
The saturated model condition in degree means that a first-order model realizes every one-variable complete type over a parameter set of size less than . Equivalently every finitely satisfiable such complete type is realized, since it can be extended to a complete type. Without a specified degree, saturated usually means -saturated. Countable saturation means -saturation, including complete types over countably many parameters.
Here is a general saturated elementary extension theorem, with proof: for every infinite regular cardinal , every first-order structure has a -saturated elementary extension. At a stage , list all complete types over its subsets of size less than . There is a set of them, since their formulas lie in a set-sized language. Add a witness constant for each complete type to the elementary diagram of , together with every formula in that complete type evaluated at its witness constant. A finite part mentions finitely many complete types and finitely many formulas from each; each finite conjunction is realizable in , and the witnesses for different complete types are unconstrained relative to each other. Thus the finite part is satisfiable. The compactness theorem produces an elementary extension realizing all those complete types. At limits take elementary unions, justified by the elementary chain theorem.
Iterate for stages and put . If has size below , regularity bounds the stages at which its elements enter, so for some . A complete type over consistent with is finitely satisfiable in : each finite conjunction is an existential formula with parameters from , and elementarity transfers its truth from . The complete type is therefore realized in . This proves
For a singular desired degree, apply the theorem at a larger regular cardinal. If is infinite and an uncountable regular satisfies , with and , the construction can keep every stage of size . There are then at most parameter sets and complete types, and downward Löwenheim-Skolem gives that size after each extension; adding distinct elements initially ensures final size exactly . The resulting model is saturated in the unqualified sense. The cardinal-arithmetic hypothesis belongs to this size refinement, not to the general existence theorem.
An explicit ultraproduct version is useful too. In a countable language let be a nonprincipal ultrafilter on and , where each factor is nonempty. Enumerate a countable finitely satisfiable complete type, including its chosen parameter representatives, as . By the Łoś theorem, the set of coordinates where the first formulas have a simultaneous witness belongs to . Put
These are decreasing members of . At coordinate , let be the greatest with , if there is one. Choose a witness to the first formulas there, and an arbitrary element when there is none. For fixed , every coordinate in has , so the chosen function satisfies on a -large set. Its ultraproduct class realizes the whole complete type. A countable language over a countable parameter set has only countably many formulas, so this proves countable saturation of a nonprincipal ultraproduct over omega.
For NFU, we give the rank-indiscernible construction of an NFU model explicitly. NFU has a unary predicate for sets, atoms have no members, extensionality applies to sets, and comprehension applies to every stratified formula. A stratification assigns integer types to variables so that equality uses equal types and requires . A unary set predicate adds no type difference.
Start with the actual set structure . This structure satisfies extensionality and every pure-membership separation instance: the subset defined in a set of rank below still has rank below . We do not assert that satisfies replacement or all of ZFC. Expand it by Skolem functions. In it use the sequence of rank objects , . For two such objects in sequence order, we have
with quantifiers in . The second statement holds because every subset of belongs to , and the later rank is at least .
Introduce constants , , and require them to be order indiscernibles in the Skolem language, satisfying these two assertions whenever . Also require for every ; this fixed rank object is first-order definable in . Every finite part of these requirements together with is satisfiable: color finite increasing tuples of the original rank sequence by the truth values of the finitely many formulas mentioned, and use Ramsey's theorem to get a homogeneous subsequence. The rank assertions hold for every increasing tuple there. The compactness theorem gives a model of the full theory. In its Skolem hull generated by the , the integer shift extends to an automorphism with , by the term-transport proof of the Ehrenfeucht-Mostowski theorem. Thus still satisfies extensionality and all pure-membership separation instances, and
This is a set-sized first-order model; no satisfaction predicate for a proper-class universe is being assumed.
Externally let . The automorphism bijects onto . Interpret a typed structure with sort equal to . At sort , declare a set exactly when ; otherwise it is an atom. Define adjacent-sort membership by
The guard is necessary: a typed atom might have some ordinary -members in , and those must not become its typed members. Set-extensionality follows from extensionality in , because the ordinary members of a typed set all lie in . For any typed formula on sort , its quantifiers can be restricted to the corresponding , its set predicates replaced by subset assertions, and its memberships replaced by the guarded relation. This is an ordinary pure-membership formula of with finitely many parameters. Separation gives its extension , and the displayed closure assertion gives . It is therefore a typed set witnessing comprehension. The automorphism shifts these sorted domains and preserves the set flags and guarded memberships.
Collapse the types onto . Define
Objects not satisfying have no -members. If two sets have the same -members, their images under are subsets of with the same ordinary members, so are equal by extensionality of ; injectivity of gives equality of the original objects.
To verify every stratified comprehension instance, assign a variable its stratification type and translate its value to . Equality is preserved. An atomic translates to the guarded adjacent-sort membership because ; the unary predicate translates to . Induction on formulas, using the domain bijections for quantifiers, preserves truth. If the free variable has type , typed comprehension produces its extension , with . Put . Then holds, and for every ,
This is exactly the required NFU set. No formula containing the external automorphism has been used in a separation or comprehension scheme; only transports values after the pure formula is formed.
The construction also permits the usual infinity requirement. The ordinary and its successor graph are definable in , hence fixed by , and lie below , so belong to all the required domains. Under , the members of are still its ordinary -members. The new Kuratowski pair satisfies
Since , membership of this pair in under is equivalent to . Thus is an internal injection of into itself omitting zero, giving a Dedekind-infinite set.
We have built a model of NFU, with infinity if it is included in the formulation, in ordinary ZFC metatheory:
In particular . This proof does not assume as an additional internal axiom: its starting structure is the set , not a model of ZFC.
For the effective counterexample, let be the diagonal halting set and let be the finite approximation obtained by running the first programs for steps. For , define the recursive triple colouring with no computable infinite homogeneous set by
This is a total recursive two-coloring: only bounded computations are involved. An infinite homogeneous set cannot have color one. Fix and take sufficiently large that every halting computation with index at most that ever halts has already halted by stage ; then the color is zero. If has color zero, it computes : given , find in with and inspect . Agreement with every later stage , and the unboundedness of , give . Hence this is the correct answer. The set is not recursive: a purported halting decider would produce a program that halts exactly when the decider says it does not halt on its own index. Thus there is no recursive infinite homogeneous set. Here infinite is essential: every finite subset is recursive, and sets with fewer than three elements are vacuously homogeneous.
A precise finite-arity Erdős-Rado theorem for finite arities is
where and . We prove the closed elementary-submodel construction of an end-homogeneous sequence and then induct. We work with AC, as in the usual cardinal partition calculus.
Put , where is infinite, and let with and . Choose a regular cardinal large enough that this coloring and its domain belong to , the sets of hereditary size below . There is of size containing , every ordinal below , and closed under externally given sequences of length at most . Here is the closure construction: start with a Skolem hull of the named parameters and the ordinals below ; iterate hulls after adjoining all at-most--sequences of the preceding hull for stages. Every stage and the union have size , since and . The elementary chain theorem gives elementarity. Any sequence of at most members of the final union lies in a bounded stage, because is regular, and is added at the next stage. This proves the required closure.
Let . Regularity of gives , and : otherwise would also belong to . Recursively choose increasing for so that, for every -subset of the earlier points,
To justify the recursion, the earlier sequence has length at most , hence belongs to . There are at most constraints. All their points and color values are in , so their coded table belongs to by closure, even though itself is external to . The supremum of the earlier points, plus one, also belongs to and is below . Thus witnesses in that a point above that bound satisfying the table exists. Elementarity supplies such a point in . This completes the recursion.
The sequence is end-homogeneous: on any increasing -tuple from it, the color depends only on its first entries. Define the induced -tuple coloring by . For the induction, the arity-one assertion is the infinite pigeonhole principle: a union of sets each of size at most has size at most . At step , take , so . The constructed sequence has size . The induction hypothesis makes constant on a subset of size ; end-homogeneity makes constant on its -subsets. This proves the theorem. In particular gives an uncountable homogeneous set for every finite-arity coloring with countably many colors, on a sufficiently large cardinal.
There is no unrestricted infinite-exponent analogue under AC. For any infinite cardinal , choose one representative from each equivalence class of modulo finite symmetric difference. Color by the parity of . Removing one element of leaves it in the same class and reverses the parity. Every infinite proposed homogeneous set contains both a countably infinite and , so cannot be homogeneous. Thus the finite-symmetric-difference colouring of infinite subsets proves
The contrast is between arbitrary colorings at countably infinite arity and the finite arities of the theorem; restrictions on the definability of an infinite-arity coloring can change the problem.

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