well-founded induction WellFoundedInduction 2002-06-01 14:14:53 2007-07-03 01:30:41 Theorem well-founded relation induction % this is the default PlanetMath preamble. as your knowledge % of TeX increases, you will probably want to edit this, but % it should be fine as is for beginners. % almost certainly you want these \usepackage{amssymb} \usepackage{amsmath} \usepackage{amsfonts} % used for TeXing text within eps files %\usepackage{psfrag} % need this for including graphics (\includegraphics) %\usepackage{graphicx} % for neatly defining theorems and propositions %\usepackage{amsthm} % making logically defined graphics \usepackage[arrow,curve,poly,arc,2cell,frame,web]{xypic} %\usepackage[thmmarks]{ntheorem} % there are many more packages, add them here as you need them % define commands here \newcommand{\br}{[\![} \newcommand{\rb}{]\!]} \newcommand{\oq}{\text{``}} \newcommand{\cq}{\text{''}} \newcommand{\im}{\mathbf{Im}} \newcommand{\dom}{\mathbf{Dom}} \newcommand{\Or}{\vee} \newcommand{\Implies}{\Rightarrow} \newcommand{\Iff}{\Leftrightarrow} \newcommand{\proves}{\vdash} \renewcommand{\And}{\wedge} \newcommand{\Sup}{\bigwedge} \newcommand{\Inf}{\bigvee} \newcommand{\Z}{\mathbb{Z}} \newcommand{\F}{\mathbb{F}} \newcommand{\Q}{\mathbb{Q}} \newcommand{\R}{\mathbb{R}} \newcommand{\C}{\mathbb{C}} \newcommand{\Nat}{\mathbb{N}} \newcommand{\M}{\mathfrak{M}} \newcommand{\N}{\mathfrak{N}} \newcommand{\A}{\mathfrak{A}} \newcommand{\B}{\mathfrak{B}} \newcommand{\K}{\mathfrak{K}} \newcommand{\G}{\mathbb{G}} \newcommand{\Def}{\overset{\operatorname{def}}{:=}} \newcommand{\spec}{\text{{\bf Spec}}} \newcommand{\stab}{\text{{\bf Stab}}} \newcommand{\ann}{\text{{\bf Ann}}} \newcommand{\irr}{\text{{\bf Irr}}} \newcommand{\qt}{\text{{\bf Qt}}} \newcommand{\st}{\mathcal{Qt}} \newcommand{\ro}{\mathbf{r.o.}} \newcommand{\Endo}{\text{{\bf End}}} \newcommand{\mat}{\text{{\bf Mat}}} \newcommand{\der}{\text{{\bf Der}}} \newcommand{\rad}{\text{{\bf Rad}}} \newcommand{\trd}{\text{{\bf tr.d.}}} \newcommand{\cl}{\text{{\bf acl}}} \newcommand{\Int}{\text{{\bf int}}} \newcommand{\V}{\mathbb{V}} \newcommand{\D}{\mathbf{D}} \newcommand{\del}{\partial} \renewcommand{\O}{\mathcal{O}} \newcommand{\aut}{\mathbf{Aut}} \newcommand{\height}{\text{\bf Height}} \newcommand{\coheight}{\text{\bf Co-height}} \newcommand{\lcm}{\operatorname{lcm}} \newcommand{\Gal}{\operatorname{Gal}} \newcommand{\x}{\mathbf{x}} \newcommand{\y}{\mathbf{y}} \newcommand{\inner}[2]{\langle #1|#2\rangle} \renewcommand{\r}{{r}} \renewcommand{\t}{{t}} \newcommand{\restr}{\upharpoonright} \newcommand{\Matrix}[4]{\left(\begin{array}{cc} #1 & #2 \\ #3 & #4 \end{array}\right)} \PMlinkescapeword{states} {\bf Definition.} Let $S$ be a non-empty set, and $R$ be a binary relation on $S$. Then $R$ is said to be a {\bf well-founded} relation if and only if every nonempty subset $X\subseteq S$ has an \PMlinkname{$R$-minimal element}{RMinimalElement}. When $R$ is well-founded, we also call the underlying set $S$ well-founded. Note that $R$ is by no means required to be a total order, or even a partial order. When $R$ is a partial order, then $R$-minimality is the same as minimality (of the partial order). A classical example of a well-founded set that is not totally ordered is the set $\Nat$ of natural numbers ordered by division, i.e. $aRb$ if and only if $a$ divides $b$, and $a\not=1$. The $R$-minimal elements of $\Nat$ are the prime numbers. Let $\Phi$ be a property defined on a well-founded set $S$. The principle of well-founded induction states that if the following is true : \begin{enumerate} \item $\Phi$ is true for all the $R$-minimal elements of $S$ \item for every $a$, if for every $x$ such that $xRa$, we have $\Phi(x)$, then we have $\Phi(a)$ \end{enumerate} then $\Phi$ is true for every $a\in S$. As an example of application of this principle, we mention the proof of the fundamental theorem of arithmetic : every natural number has a unique factorization into prime numbers. The proof goes by well-founded induction in the set $\Nat$ ordered by division.