The axiom of infinity fails. First prove for every finite ordinal . The base stage is empty in both hierarchies. If , that stage is a finite set. Every one of its subsets is definable over it with finitely many parameters, by a disjunction of equalities to the selected elements; the empty subset is defined by a false formula. Hence
Induction and the limit-stage definitions give
the set of all hereditarily finite sets. Every member of this set is finite externally.
If this transitive structure satisfied the axiom of infinity, it would contain an inductive set : zero belongs to , and whenever , its successor belongs to . These operations are the actual empty set and actual set successor, since they are absolute for this transitive structure and all relevant finite-rank sets lie in it. External induction would then place every finite ordinal in , contradicting the finiteness of .
Every individual finite ordinal does belong to , but the set of all finite ordinals does not. The distinction between containing each finite ordinal and containing one inductive set is precisely the issue.
Use transfinite induction. The assertion is immediate at stage zero, and at a limit stage it follows by taking the increasing union of the earlier stages.
Assume . Any ordinal is a subset of , since members of the definable power set are such subsets. Every element of is an ordinal, so
which implies . This gives the upper bound on the ordinals appearing at the successor stage.
For the reverse inclusion, the smaller ordinals are already in and hence in . The remaining ordinal itself is the definable subset . The fact used here is absoluteness of ordinalhood between a transitive set and the universe: ordinalhood has a bounded definition, and bounded formulas are absolute for transitive sets. Thus the formula asserting that a member is an ordinal, interpreted over , defines exactly . Therefore .
This proves
In particular each ordinal is a member of , so .
For a set , its definable power set consists of the subsets of definable by a first-order formula over using finitely many parameters from . The quantifiers range over ; this is generally much smaller than its full power set.
The constructible universe is defined by transfinite recursion:
The last union denotes a definable proper class, not a set-sized union over a set of all ordinals. At a successor stage, only definitions over the previously constructed stage are permitted.
To prove that power-set equality is not upward absolute, use the standard constructible universe theorem: is a transitive inner model of ZF containing every ordinal, and set rank is absolute between and . Since , some rank stage contains a nonconstructible set. Let be the least ordinal with . It is not zero; it cannot be a limit, since a union of earlier stages contained in is still contained in . Thus and .
We need not merely this inclusion, but that itself belongs to . Inside , ZF constructs its own rank stage , which is a set of . By transitivity and rank absoluteness,
Consequently . Let , the power set computed in . Then and .
By minimality there is . Externally , but , because every member of the set is in the transitive class . Hence . Taking and proves power-set equality is not upward absolute, even between transitive models of ZF.
There is no contradiction with absoluteness of : that bounded relation agrees whenever both parameters are present in the smaller class. Power-set equality quantifies over all subsets, including a new absent from the smaller class. The step proving is essential; inclusion in a class alone would not imply membership in it.
A sufficient syntactic condition is that be a sigma-one formula in set theory, written : an existential block with bounded, meaning that each of its quantifiers is of the form or . A bounded formula is also called and is absolute in both directions between transitive classes.
Prove the latter fact by structural induction. Atomic membership and equality have their actual meanings in both classes, and Boolean connectives preserve equivalence of truth. For a bounded quantifier with bound , transitivity ensures that every element of belongs to ; thus its range is exactly the same in both classes, and induction applies to its matrix. This proves the bounded case. If the smaller class satisfies a formula, take its existential witnesses in . They remain available in , and bounded absoluteness preserves the matrix. Hence formulas are upward absolute. An arbitrary unbounded universal quantifier has no such witness-preservation argument.
Let be transitive classes, both interpreted with actual membership. A formula is upward absolute from to if for every tuple of parameters from ,
For proper classes this means the usual relativization of the fixed formula's quantifiers. Full absoluteness requires the implication in both directions. The qualification on parameters matters: the smaller class must contain every object named in the comparison.
The generalized continuum hypothesis is
Equivalently, for every ordinal , . Here is the cardinality of the power set of a set of cardinality , and is the least strictly larger cardinal. The hypothesis says that no intermediate cardinal lies between an infinite set and its power set.
König's theorem for cardinal numbers states that, for a set-indexed family with at every index,
Here the sum is the cardinality of a disjoint union and the product is the cardinality of a Cartesian product. Work in ZFC. Choose disjoint sets of sizes and sets of sizes . For any function , its th coordinate values on form a subset of of cardinality at most . Choose outside that subset, using choice. Then cannot equal for any : if , its th coordinate was specifically excluded. Thus there is no surjection from the disjoint union onto the product.
Cardinal comparability under choice now implies the displayed strict inequality. Empty index set gives directly; empty individual cause no difficulty, since the corresponding coordinate excludes an empty image. This is the cardinal diagonal theorem, rather than the finitely branching tree result also bearing König's name.
To prove replacement failure at V omega plus omega, put . The set belongs to , and for every the ordinal also belongs to . The relation saying that is obtained by taking successive ordinal successors of is definable, with parameter , and is single valued in .
For clarity this does not assume Replacement inside . For each finite its finite computation sequence exists in : its entries have rank below , and the finite coding overhead still has rank below . The bounded formula verifying this finite successor chain is absolute between and the universe. The ordinary finite induction identifying its unique last entry uses the actual finite ordinals, which are the same in . This justifies the internal definable function without invoking the axiom being tested.
If Replacement held there, its range would be an element of . But ordinal rank equals the ordinal, so
Every element of has strictly smaller rank. This contradiction proves Replacement fails in . Each individual output is present; the missing object is the set collecting all outputs.
Take a nonzero limit ordinal and . Choose with . Transitivity gives . Hence every actual subset of belongs to , and the actual set belongs to . Since is a limit, , so . Thus the internal power set contains every actual subset of , and the power-set axiom holds in .
Here the absoluteness fact used is: every bounded formula is absolute between transitive sets or classes with the actual membership relation. In particular , expressed by , has the same meaning internally and externally. The argument supplies the actual power set as an internal witness. If zero is included in one's convention for limit ordinals, its empty stage has no nonempty first-order domain; the assertion is understood for nonzero limits.
If also , the preceding ordinal-membership result gives . The actual set contains the empty set and is closed under . These bounded membership and successor conditions are absolute in the transitive stage, so is an internal inductive set. Therefore Infinity holds as well. In contrast has only hereditarily finite sets and cannot use as an element.
The cumulative hierarchy is defined by transfinite recursion on the ordinals:
The recursion theorem of ZF supplies each set stage. The whole universe is , a proper-class union. Equivalently, exactly when the rank of is less than , where .

Pinned article: Introduction to the OurBigBook Project

Welcome to the OurBigBook Project! Our goal is to create the perfect publishing platform for STEM subjects, and get university-level students to write the best free STEM tutorials ever.
Everyone is welcome to create an account and play with the site: ourbigbook.com/go/register. We belive that students themselves can write amazing tutorials, but teachers are welcome too. You can write about anything you want, it doesn't have to be STEM or even educational. Silly test content is very welcome and you won't be penalized in any way. Just keep it legal!
We have two killer features:
  1. topics: topics group articles by different users with the same title, e.g. here is the topic for the "Fundamental Theorem of Calculus" ourbigbook.com/go/topic/fundamental-theorem-of-calculus
    Articles of different users are sorted by upvote within each article page. This feature is a bit like:
    • a Wikipedia where each user can have their own version of each article
    • a Q&A website like Stack Overflow, where multiple people can give their views on a given topic, and the best ones are sorted by upvote. Except you don't need to wait for someone to ask first, and any topic goes, no matter how narrow or broad
    This feature makes it possible for readers to find better explanations of any topic created by other writers. And it allows writers to create an explanation in a place that readers might actually find it.
    Figure 1.
    Screenshot of the "Derivative" topic page
    . View it live at: ourbigbook.com/go/topic/derivative
  2. local editing: you can store all your personal knowledge base content locally in a plaintext markup format that can be edited locally and published either:
    This way you can be sure that even if OurBigBook.com were to go down one day (which we have no plans to do as it is quite cheap to host!), your content will still be perfectly readable as a static site.
    Figure 5. . You can also edit articles on the Web editor without installing anything locally.
    Video 3.
    Edit locally and publish demo
    . Source. This shows editing OurBigBook Markup and publishing it using the Visual Studio Code extension.
  3. https://raw.githubusercontent.com/ourbigbook/ourbigbook-media/master/feature/x/hilbert-space-arrow.png
  4. Infinitely deep tables of contents:
    Figure 6.
    Dynamic article tree with infinitely deep table of contents
    .
    Descendant pages can also show up as toplevel e.g.: ourbigbook.com/cirosantilli/chordate-subclade
All our software is open source and hosted at: github.com/ourbigbook/ourbigbook
Further documentation can be found at: docs.ourbigbook.com
Feel free to reach our to us for any help or suggestions: docs.ourbigbook.com/#contact