Marked extensional well-founded orders are important in constructing the sets of the cumulative hierarchy in a model of set theory, in the same way that well-orders or sets with transitive extensional well-founded relations are important in constructing the ordinals of . These become important in constructive mathematics where one cannot in general show that the set of cardinals in and the set of ordinals in are in bijection with each other.
A marked extensional well-founded order or mewo is a set with an extensional well-founded relation on a set and a predicate on .
An element is marked if is true. By the axiom schema of bounded separation, one can construct the subset of marked elements in :
A marked extensional well-founded order homomorphism between two marked extensional well-founded order and is a function such that
preserves the marking predicate: for all , implies that
preserves the well-founded relation: for all and , implies that
A marked extensional well-founded order isomorphism is a marked extensional well-founded order homomorphism with a marked extensional well-founded order homomorphism such that for all elements , and for all elements .
The category of marked extensional well-founded order homomorphisms is the concrete category whose objects are marked extensional well-founded orders and whose morphisms are marked extensional well-founded order homomorphisms.
There is a forgetful functor which takes a marked extensional well-founded order to its underlying extensional well-founded order . There is also a functor which takes an extensional well-founded order to the marked extensional well-founded order , where is the always true predicate on . The trivialization of a marked extensional well-founded order is defined as the composite of the two functors above .
A simulation between marked extensional well-founded orders and is a marked extensional well-founded order homomorphism such that its image is downwards closed: for all and , if , then there exists such that and .
We denote the set of simulations between marked extensional well-founded orders and by .
The category is the subcategory of whose objects are marked extensional well-founded orders and whose morphisms are simulations. We show that the above category is a poset:
Since the relation is extensional and well-founded, the following is true of simulations:
Every simulation is an injection.
Given marked extensional well-founded orders and , the set of simulations has at most one element.
As a result, one could define the relation on marked extensional well-founded orders by . The relation between marked extensional well-founded orders is a partial order
An element is covered if there exists a marked element such that is true. Given a marked extensional well-founded order and an element , the initial segment of is the set of all elements covered by
The initial segment is a marked extensional well-founded order, with the well-founded relation defined as for elements and , and the marking relation defined as for elements .
A marked extensional well-founded order is covered if every element is covered; i.e.
It follows by well-founded induction that is a covered marked extensional well-founded order.
Given a marked extensional well-founded order , the function , defined by the composite of the canonical subset injection and the canonical function given by the identity function on the carrier set, is a simulation.
Given a marked extensional well-founded order and elements and , implies that .
Given marked extensional well-founded orders and and a function which preserves the marking predicate; i.e. implies that for all , then is a simulation if and only if .
A bounded simulation between marked extensional well-founded orders and consists of a marked element and a simulation such that the image of is equal to the initial segment at , . We denote the set of bounded simulations between marked extensional well-founded orders and by .
Given marked extensional well-founded orders and , the set of bounded simulations has at most one element.
As a result, one could define the relation on marked extensional well-founded orders by . The relation satisfies the following properties
for all marked extensional well-founded orders and , implies that
for all marked extensional well-founded orders and and , and implies that
for all marked extensional well-founded orders and and , and implies that
Last revised on January 26, 2023 at 16:24:55. See the history of this page for a list of all contributions to it.