Marked extensional well-founded orders are important in constructing the sets of the cumulative hierarchy $V$ 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 $V$. These become important in constructive mathematics where one cannot in general show that the set of cardinals in $V$ and the set of ordinals in $V$ are in bijection with each other.
A marked extensional well-founded order or mewo is a set $S$ with an extensional well-founded relation $a \prec b$ on a set $S$ and a predicate $m(a)$ on $S$.
An element $x \in S$ is marked if $m(x)$ is true. By the axiom schema of bounded separation, one can construct the subset of marked elements in $S$:
A marked extensional well-founded order homomorphism between two marked extensional well-founded order $S$ and $T$ is a function $f:S \to T$ such that
$f$ preserves the marking predicate: for all $x \in S$, $m(x)$ implies that $m(f(x))$
$f$ preserves the well-founded relation: for all $x \in S$ and $y \in S$, $x \prec y$ implies that $f(x) \prec f(y)$
A marked extensional well-founded order isomorphism is a marked extensional well-founded order homomorphism $f:S \to T$ with a marked extensional well-founded order homomorphism $g:T \to S$ such that for all elements $s \in S$, $g(f(s)) = s$ and for all elements $t \in T$ $f(g(t)) = t$.
The category of marked extensional well-founded order homomorphisms is the concrete category $\mathrm{MEWO}$ whose objects are marked extensional well-founded orders and whose morphisms are marked extensional well-founded order homomorphisms.
There is a forgetful functor $U:\mathrm{MEWO} \to \mathrm{EWO}$ which takes a marked extensional well-founded order $(S, \prec, m)$ to its underlying extensional well-founded order $(S, \prec)$. There is also a functor $F:\mathrm{EWO} \to \mathrm{MEWO}$ which takes an extensional well-founded order $(S, \prec)$ to the marked extensional well-founded order $(S, \prec, \top_S)$, where $\top_S$ is the always true predicate on $S$. The trivialization of a marked extensional well-founded order is defined as the composite of the two functors above $\overline{S} \coloneqq F(U(S))$.
A simulation between marked extensional well-founded orders $S$ and $T$ is a marked extensional well-founded order homomorphism $f:S \to T$ such that its image is downwards closed: for all $x \in S$ and $y \in T$, if $y \prec f(x)$, then there exists $z \in S$ such that $z \prec x$ and $f(z) \prec y$.
We denote the set of simulations between marked extensional well-founded orders $S$ and $T$ by $S \sqsubseteq T$.
The category $\mathrm{MEWO}_\mathrm{Sim}$ is the subcategory of $\mathrm{MEWO}$ 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 $\prec$ is extensional and well-founded, the following is true of simulations:
Every simulation $f:S \to T$ is an injection.
Given marked extensional well-founded orders $S$ and $T$, the set of simulations $S \sqsubseteq T$ has at most one element.
As a result, one could define the relation $S \leq T$ on marked extensional well-founded orders by $\exists x.x \in S \sqsubseteq T$. The relation $S \leq T$ between marked extensional well-founded orders is a partial order
An element $x \in S$ is covered if there exists a marked element $y \in S$ such that $x \prec y$ is true. Given a marked extensional well-founded order $S$ and an element $x \in S$, the initial segment of $S$ is the set of all elements covered by $x \in S$
The initial segment $S \downarrow^+ x$ is a marked extensional well-founded order, with the well-founded relation defined as $y \prec z$ for elements $y \in S \downarrow^+ x$ and $z \in S \downarrow^+ x$, and the marking relation defined as $m_x(y) \coloneqq y \prec x$ for elements $y \in S \downarrow^+ x$.
A marked extensional well-founded order is covered if every element $x \in S$ is covered; i.e.
It follows by well-founded induction that $S \downarrow^+ x$ is a covered marked extensional well-founded order.
Given a marked extensional well-founded order $S$, the function $f:S \downarrow^+ x \to \overline{S}$, defined by the composite of the canonical subset injection $i:S \downarrow^+ x \to S$ and the canonical function $j:S \to \overline{S}$ given by the identity function on the carrier set, is a simulation.
Given a marked extensional well-founded order $S$ and elements $x \in S$ and $y \in S$, $S \downarrow^+ x = S \downarrow^+ y$ implies that $x = y$.
Given marked extensional well-founded orders $S$ and $T$ and a function $f:S \to T$ which preserves the marking predicate; i.e. $m(x)$ implies that $m(f(x))$ for all $x \in S$, then $f$ is a simulation if and only if $S \downarrow^+ x = T \downarrow^+ f(x)$.
A bounded simulation between marked extensional well-founded orders $S$ and $T$ consists of a marked element $y \in M_T$ and a simulation $f:S \to T$ such that the image of $f$ is equal to the initial segment at $y$, $\mathrm{im}(f) = T \downarrow^+ y$. We denote the set of bounded simulations between marked extensional well-founded orders $S$ and $T$ by $S \sqsubset T$.
Given marked extensional well-founded orders $S$ and $T$, the set of bounded simulations $S \sqsubset T$ has at most one element.
As a result, one could define the relation $S \lt T$ on marked extensional well-founded orders by $\exists x.x \in S \sqsubset T$. The relation satisfies the following properties
for all marked extensional well-founded orders $S$ and $T$, $S \lt T$ implies that $S \leq \overline{T}$
for all marked extensional well-founded orders $S$ and $T$ and $U$, $S \lt T$ and $T \lt U$ implies that $S \leq \overline{U}$
for all marked extensional well-founded orders $S$ and $T$ and $U$, $S \lt T$ and $T \leq U$ implies that $S \lt U$
Last revised on January 26, 2023 at 16:24:55. See the history of this page for a list of all contributions to it.