\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{well-founded relation}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{relations}{}\paragraph*{{Relations}}\label{relations}

[[!include relations - contents]]

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{defn}{Definitions}\dotfill \pageref*{defn} \linebreak
\noindent\hyperlink{formulations_in_classical_logic}{Formulations in classical logic}\dotfill \pageref*{formulations_in_classical_logic} \linebreak
\noindent\hyperlink{coalgebraic_formulation}{Coalgebraic formulation}\dotfill \pageref*{coalgebraic_formulation} \linebreak
\noindent\hyperlink{simulations}{Simulations}\dotfill \pageref*{simulations} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

A (binary) [[relation]] $\prec$ on a [[set]] $S$ is called \emph{well-founded} if it is valid to do [[induction]] on $\prec$ over $S$.

\hypertarget{defn}{}\subsection*{{Definitions}}\label{defn}

Let $S$ be a [[set]], and let $\prec$ be a [[binary relation]] on $S$. A [[subset]] $A$ of $S$ is \textbf{$\prec$-inductive} if

\begin{displaymath}
\forall (x\colon S),\; (\forall (t\colon S),\; t \prec x \;\Rightarrow\; t \in A) \;\Rightarrow\; x \in A.
\end{displaymath}
The relation $\prec$ is \textbf{well-founded} if the only $\prec$-inductive subset of $S$ is $S$ itself.

Note that this is precisely what is necessary to validate induction over $\prec$: if we can show that a statement is true of an element $x$ of $S$ whenever it is true of everything that precedes ($\prec$) $x$, then it must be true of everything in $S$. In the presence of [[excluded middle]] it is equivalent to other commonly stated definitions; see \emph{Formulations in classical logic} below.

\hypertarget{formulations_in_classical_logic}{}\subsubsection*{{Formulations in classical logic}}\label{formulations_in_classical_logic}

While the definition above follows how a well-founded relation is generally \emph{used} (namely, to prove properties of elements of $S$ by induction), it is complicated. Two alternative formulations are given by the following:

\begin{enumerate}%
\item The relation $\prec$ has \textbf{no infinite descent} (usually attributed to [[Pierre de Fermat]]) if there exists no [[sequence]] $\cdots \prec x_2 \prec x_1 \prec x_0$ in $S$. (Such a sequence is called an \emph{infinite descending sequence}.)


\item The relation $\prec$ is \textbf{classically well-founded} if every [[inhabited set|inhabited]] subset $A$ of $S$ has a member $x \in A$ such that no $t \in A$ satisfies $t \prec x$. (Such an $x$ is called a \emph{minimal} element of $A$.)



\end{enumerate}
In [[classical mathematics]], both of these conditions are equivalent to being well-founded. In constructive mathematics, we may prove that a well-founded relation has no infinite descent (see Proposition \ref{empty}), but not the converse, and that a classically well-founded relation is well-founded (see Proposition \ref{classical}), but not the converse.

The classical notion of well-foundedness enforces classical logic onto us, in the following sense.

\begin{prop}
\label{LEM}\hypertarget{LEM}{}
If $(X, \prec)$ is an [[inhabited subset|inhabited]] well-founded relation in a classical sense, then the unrestricted [[excluded middle|law of excluded middle]] holds.

\end{prop}
For a [[topos]]-theoretic proof see \href{http://ncatlab.org/toddtrimble/published/classical+well-foundedness}{here}.

\begin{proof}
Suppose there are $x$ and $y$ such that $y\prec x$, and let $Q$ be an arbitrary proposition. Consider then a set $P \subset X$ defined as $P = \{ x \} \cup \{ a \mid a \prec x \;\wedge\; Q\}$. Clearly, the set $P$ is inhabited, thus by classical well-foundedness it has a minimal element $x_0$. By intuitionistic reasoning, either $x_0$ is in $\{ x \}$, i.e. $x_0 = x$, or $x_0 \in \{ a \mid a \prec x \;\wedge\; Q\}$, i.e. $x_0 \prec x \;\wedge\; Q$. In the latter case we immediately see that $Q$ holds. So, suppose that $x_0 = x$ is the minimal element of $P$; we will show that $\neg Q$ holds. For suppose that $Q$ holds; then $y \in P$ and $y \prec x = x_0$, violating the condition that $x_0$ is a minimal element of $P$.

Since $Q$ was an arbitrary proposition, we can deduce $\forall Q. (Q \vee \neg Q)$.

\end{proof}
\begin{remark}
\label{LEM_rem}\hypertarget{LEM_rem}{}
We note that classical well-foundedness is really too strong for constructive (i.e., intuitionistic) mathematics, due to Proposition \ref{LEM}. On the other hand, the infinite descent condition is too weak to be of much use in constructive mathematics. It is the inductive notion of well-foundedness that is just right.

\end{remark}
Note however that in [[predicative mathematics]], the definition of well-founded may be impossible to even state, and so either of these alternative definitions would be preferable, provided classical logic is used.

Even in constructive predicative mathematics, (1) is strong enough to establish the [[Burali-Forti paradox]] (when applied to [[linear orders]]). In [[material set theory]], (2) is traditionally used to state the [[axiom of foundation]], although the impredicative definition could also be used as an axiom scheme (and must be in constructive versions). In any case, either (1) or (2) is usually preferred by classical mathematicians as simpler.

To round out the discussion we prove the following two results, both valid in intuitionistic mathematics:

\begin{prop}
\label{empty}\hypertarget{empty}{}
If $(X, \prec)$ is a well-founded relation and $A \subseteq X$ has no minimal element, then $A$ is empty.

\end{prop}
This result makes it trivial to infer (under classical logic) that classical well-foundedness is a consequence of well-foundedness. It also shows that well-foundedness rules out infinite descent (intuitionistically), since an infinite descent sequence has no minimal element.

\begin{proof}
Let $U = \{u \in X: u \notin A\; \wedge \; (\forall x: X),\; x \prec u \Rightarrow x \notin A\}$. Clearly $U \cap A = \emptyset$. We show $U$ is inductive, so that under well-foundedness $U = X$ and $A = X \cap A = U \cap A = \emptyset$, as desired.

So, suppose $z$ is an element such that $y \in U$ whenever $y \prec z$. We must show $z \in U$. Claim: $z \notin A$. For if $z \in A$, then $z$ would be a minimal element of $A$ (as $y \prec z \Rightarrow y \in U \Rightarrow y \notin A$). But this negates the assumption that $A$ has no minimal element.

Thus $z \notin A$, and $y \prec z \Rightarrow y \in U \Rightarrow y \notin A$, so that $z \in U$. This completes the proof.

\end{proof}
\begin{prop}
\label{classical}\hypertarget{classical}{}
In intuitionistic set theory, classical well-foundedness implies (inductive) well-foundedness.

\end{prop}
\begin{proof}
Let $\prec$ be a classically well-founded relation on $X$, and let $U$ be an inductive subset. We must show that every element $x \in X$ belongs to $U$. Since $U$ is inductive, it suffices to show that every $u \prec x$ belongs to $U$, i.e. we may assume given a $u$ such that $u\prec x$ and show $u\in U$. But under this assumption we have that $\prec$ is inhabited, so according to Remark \ref{LEM}, the law of [[excluded middle]] follows and we might as well then argue classically. The argument is well-known but we include it for completeness: under classical well-foundedness, if an inductive subset $U$ is not the entirety of $X$, then the complement $\neg U$ has a minimal element $y$. In that case, $v \prec y$ implies $v \in \neg\neg U = U$, but then $y \in U$ since $U$ is inductive, contradiction. Hence $U = X$ and in particular $u \in U$, which is what we wanted.

\end{proof}
To bring us full circle: in classical set theory we may prove that if $(X, \prec)$ has no infinite descent, then $\prec$ is classically well-founded. For suppose an inhabited subset $P \subseteq X$ (say with an element $x \in P$) failed to have a least element. Then we can find an infinite descent sequence $x_n \in P$ with $x_0 = x$, by choosing at each stage $x_{n+1} \in P$ such that $x_{n+1} \prec x_n$. Technically this requires the use of [[dependent choice]], but generally this is felt to be a mild choice principle (that is true even for intuitionistic mathematics).

\hypertarget{coalgebraic_formulation}{}\subsubsection*{{Coalgebraic formulation}}\label{coalgebraic_formulation}

Many inductive or recursive notions may also be packaged in [[coalgebra|coalgebraic]] terms. For the concept of well-founded relation, first observe that a binary relation $\prec$ on a set $X$ is the same as a coalgebra structure $\theta\colon X \to P(X)$ for the covariant [[power-set]] endofunctor on $Set$, where $y \prec x$ if and only if $y \in \theta(x)$.

In this language, a [[subset]] $i\colon U \hookrightarrow X$ is $\prec$-inductive, or $\theta$-inductive, if in the [[pullback]]

\begin{displaymath}
\itexarray{
H & \stackrel{j}{\to} & X \\ 
\downarrow & & \downarrow^\mathrlap{\theta} \\
P U & \underset{P i}{\to} & P X
}
\end{displaymath}
the map $j$ factors through $i$. (Note that $j$ is necessarily [[monomorphism|monic]], since $P$ preserves monos.) Unpacking this a bit: for any $x \in X$, if $\theta(x) = V$ belongs to $P U$, that is if $\theta(x) \subseteq U$, then $x \in U$. This says the same thing as $\forall_{x\colon X} (\forall_{y\colon X} y \prec x \Rightarrow y \in U) \Rightarrow x \in U$.

Then, as usual, the $P$-coalgebra $(X, \theta)$ is well-founded if every $\theta$-inductive subset $U \hookrightarrow X$ is all of $X$.

Other relevant notions may also be packaged; for example, the $P$-coalgebra $X$ is [[extensional relation|extensional]] if $\theta\colon X \to P X$ is monic. See also [[well-founded coalgebra]].

\hypertarget{simulations}{}\subsubsection*{{Simulations}}\label{simulations}

Given two sets $S$ and $T$, each equipped with a well-founded relation $\prec$, a [[function]] $f\colon S \to T$ is a \textbf{[[simulation]]} of $S$ in $T$ if

\begin{enumerate}%
\item $f(x) \prec f(y)$ whenever $x \prec y$ and


\item given $t \prec f(x)$, there exists $y \prec x$ with $t = f(y)$.



\end{enumerate}
Then sets so equipped form a [[category]] with simulations as [[morphisms]]. See [[extensional relation]] for more uses of simulations.

For example, a simulation $X \to Y$ between two [[well-ordered sets]] is an isomorphism of $X$ onto an [[lower set|initial segment]] of $Y$.

In coalgebraic language, a simulation $S \to T$ is simply a $P$-coalgebra homomorphism $f\colon S \to T$. Condition (1), that $f$ is merely $\prec$-preserving, translates to the condition that $f$ is a [[colax morphism]] of coalgebras, in the sense that there is an inclusion

\begin{displaymath}
\itexarray{
X & \stackrel{\theta_X}{\to} & P X \\
 ^\mathllap{f} \downarrow & \swArrow & \downarrow^\mathrlap{P f} \\
Y & \underset{\theta_Y}{\to} & P Y.
}
\end{displaymath}
\begin{prop}
\label{}\hypertarget{}{}
If $(X, \prec)$ is well-founded and $(Y, \prec)$ is (weakly) extensional, then there is at most one simulation $f: X \to Y$.

\end{prop}
\begin{proof}
It is enough to show that if $f, g: X \to Y$ are $P$-coalgebra morphisms, then $U = \{u \in X: f(u) = g(u)\}$ is an inductive subset. Suppose $y \in X$ is an element such that $f(u) = g(u)$ whenever $u \prec y$. Then $f(\{u: u \prec y\}) = g(\{u: u \prec y\})$; since $f, g$ are $P$-coalgebra maps, this is the same as the equality $\{x: x \prec f(y)\} = \{x: x \prec g(y)\}$. By extensionality, we infer $f(y) = g(y)$, so that $y \in U$. Thus $U$ is inductive.

\end{proof}
\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

Every well-founded relation is [[irreflexive relation|irreflexive]]; that is, $x \nprec x$. Sometimes one wants a reflexive version $\preceq$ of a well-founded relation; let $x \preceq y$ if and only $x \prec y$ or $x = y$. Then the requirement that $x$ be a minimal element of a subset $A$ states that $t \preceq x$ only if $t = x$. But infinite descent or direct proof by induction still require $\prec$ rather than $\preceq$.

A [[well-order|well order]] may be defined as a well-founded [[linear order]], or alternatively as a [[transitive relation|transitive]], [[extensional relation|extensional]], well-founded relation.

A [[well-quasi-order]] is a well-founded [[preorder]] (referring to the reflexive version of well-foundedness above) that in addition has no infinite [[antichain|antichains]].

The [[axiom of foundation]] in material [[set theory]] states precisely that the membership relation $\in$ on the proper class of all [[pure sets]] is well-founded. In structural set theory, accordingly, one uses well-founded relations in building structural models of well-founded pure sets.

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

Let $S$ be a [[finite set]]. Then any relation on $S$ whose [[transitive closure]] is irreflexive is well-founded.

Let $S$ be the set of [[natural numbers]], and let $x \prec y$ if $y$ is the [[successor]] of $x$: $y = x + 1$. That this relation is well-founded is the usual principle of \emph{mathematical induction}.

Again let $S$ be the set of natural numbers, but now let $x \prec y$ if $x \lt y$ in the usual order. That this relation is well-founded is the principle of \emph{strong induction}.

More generally, let $S$ be a set of [[ordinal numbers]] (or even the proper class of all ordinal numbers), and let $x \prec y$ if $x \lt y$ in the usual order. That this relation is well-founded is the principle of \emph{transfinite induction}.

Similarly, let $S$ be a set of [[pure sets]] (or even the proper class of all pure sets), and let $x \prec y$ if $x \in y$. That this relation is well-founded is the \emph{[[axiom of foundation]]}.

Let $S$ be the set of [[integers]], and let $x \prec y$ mean that $x$ properly divides $y$: $y/x$ is an integer other than $\pm{1}$. This relation is also well-founded, so one can prove properties of integers by induction on their proper divisors.

[[!redirects well-founded relation]] [[!redirects well-founded relations]] [[!redirects well founded relation]] [[!redirects well founded relations]]

[[!redirects classically well-founded relation]] [[!redirects classically well-founded relations]] [[!redirects classically well founded relation]] [[!redirects classically well founded relations]]

[[!redirects relation without infinite descent]] [[!redirects relations without infinite descent]] [[!redirects relation with no infinite descent]] [[!redirects relations with no infinite descent]] [[!redirects Fermat's method of infinite descent]] [[!redirects Fermat's method of infinite descent]] [[!redirects Fermat's method of infinite descent]] [[!redirects Fermat method of infinite descent]] [[!redirects method of infinite descent]] [[!redirects infinite descent]]



\end{document}