Induction, Coinduction, and Fixed Points: Intuitions and Tutorial
Moez A. AbdelGawad






Induction, Coinduction, and Fixed Points:

Intuitions and Tutorial

Using examples from set theory, number theory, and real
analysis
    Moez A. AbdelGawad

moez@cs.rice.edu
    December 30, 2023
====================================================================================================================================


Recently we presented a concise survey of the formulation of the induction
and coinduction principles, and some concepts related to them, in
five different fields mathematical fields, hence shedding some light
on the precise relation between these fields.

In this article we present few tutorial examples—from set theory,
number theory and real analysis—that illustrate these concepts,
and the intuitions behind them, more concretely.




§ INTRODUCTION


Fixed points and concepts related to them, such as induction and coinduction,
have applications in numerous scientific fields. These mathematical
concepts have applications also in social sciences, and even in common
culture, usually under disguise.

These precise formal mathematical concepts are in fact quite common
in everyday life to the extent that in many activities or situations
(or “systems”) a mapping and a set of its fixed points can be
easily discovered when some little mental effort is exercised. In
particular, in any situation or system where there is some informal
notion of repetition or iteration or continual “come-and-go” or
“give-and-take” together with some informal notion of reaching
a stable condition (e.g., equilibrium in chemical reactions
or “common ground” between spouses) it is usually the case that
an underlying 

self-

mapping

 (a.k.a., endofunction)

, i.e., a mathematical function/map, together with a set of

(one or more) 

fixed points of that mapping, can be easily revealed. This 

self-

mapping is sometimes called a `state transition function', and a
fixed point of the mapping is what is usually called a `stable condition'
or a `steady state' (of the “system”).

These concepts also show up thinly-disguised in visual art and music <cit.>.
However, applications of these mathematical concepts in scientific
fields, in particular, are plenty and more explicit, including ones
in economics and econometrics <cit.>, in mathematical
physics <cit.>, in computer science, and in many other
areas of mathematics itself. Their applications in computer science,
in particular, include ones in programming language semantics—which
we touch upon in this article—as well as in relational database
theory (e.g., recursive or iterated joins) and in concurrency
theory.[For more details on the use of induction, coinduction, and fixed points
in computer science, and for concrete examples of how they are used,
the reader is invited to check relevant literature on the topic, e.g.,
<cit.>.]

Fixed points, induction and coinduction have been formulated and studied
in various subfields of mathematics, usually using different vocabulary
in each field. The interested reader is invited to check our comparative
survey in <cit.>. In this article, for pedagogic
purposes, we illustrate the concepts that we presented formally in <cit.>,
and we attempt to develop intuitions for these concepts using examples
from number theory, set theory and real analysis.




§ INDUCTION AND COINDUCTION INSTANCES





 §.§ Induction Instances


An instance of the set-theoretic induction principle (presented in 3
of <cit.>) is the standard mathematical induction
principle. In this well-known instance, induction is setup as follows:
F is the “successor” function (of Peano)[Namely, F(X)={ 0}∪{ x+1|x∈ X},
where, e.g., F({ 0,3,5})={ 0,1,4,6}.], μ_F (the smallest fixed point of the successor function F)
is the set of natural numbers ℕ,[In fact μ_F defines the set ℕ as the set
of all finite non-negative whole numbers. Its existence (as
the smallest infinite inductive/successor set) is an immediate
consequence of the infinity axiom (and the subset and extensionality
axioms) of set theory (see <cit.> and <cit.>).] and P is any inductive property/set of numbers.


  * An example of an inductive set is the set P of natural numbers
defined as 

    P={n∈ℕ|2^n>n}.

(Equivalently, viewing P as a property, its definition expresses
the property that each of its members, say n, has its exponential
2^n strictly greater than n itself). Set/property P is
an inductive one since ℕ⊆ P—i.e., μ_F⊆ P—can
be proven inductively by proving that P is F-closed,
which is sometimes, equivalently, stated as proving that F preserves
property P or that property P is preserved by F.
The F-closedness (or `F-preservation') of P can be proven
by proving that F(P)⊆ P (i.e.,
that ∀ p∈ F(P),p∈ P). Using the definition
of the successor function F, this means proving that (0∈ P)∧(∀ x∈ℕ.x∈ P(x+1)∈ P),
or, in other words, proving that 2^0>0 (i.e., that the
base case, P(0), holds) and that from (2^x>x)
one can conclude that (2^x+1>x+1) (i.e.,
that the inductive case, P(x) P(x+1),
holds). This last form is the form of proof-by-induction presented
in most standard discrete mathematics textbooks.

Another instance of the induction principle is lexicographic
induction, defined on lexicographically linearly-ordered (i.e.,
“dictionary ordered”) pairs of elements <cit.>. In 

<ref>

4.1 of <cit.> (and 2.1 of <cit.>)
we present a type-theoretic formulation of the induction principle
that is closely related to the set-theoretic one. The type-theoretic
formulation is the basis for yet a third instance of the induction
principle—called structural induction—that is extensively
used in programming semantics and automated theorem proving (ATP),
including reasoning about and proving properties of (functional) software.




 §.§ Coinduction Instances



/**/Use 2^n>n coinductively? Ordinals have to be included?
P⊆ F(P) (P reflected by F) means
??P(x+1)∨ x=0 P(x) ∀ p∈ P,p∈ F(P)
i.e., ??. Check agreement with uses in `Practical Coinduction'.

Coinduction Instances

Induction embodies finiteness. Given that induction seeks minimality
(recall: an inductive set is the smallest closed set), an inductive
set includes only elements that can be finitely-constructed. For example,
a natural number n belongs to the inductively defined set ℕ
if there is a finite construction sequence, using generator
F (the successor function), that starts from the basis of F
(i.e., 0) and ends with the number n. More generally,
an element belongs to an inductively defined set if there is
a finite reason for the element to belong to the inductive
set (i.e., if there is a construction sequence, using the generator,
that starts from some basis element and ends with the element).

On the other hand, dually and probably less-familiarly, coinduction
embodies cofiniteness (a set is cofinite if the complement
of the set is finite, relative to some “universe”/universal set).
Given that coinduction seeks maximality (recall: a coinductive set
is the largest consistent set), a coinductive set excludes
only elements that cannot be finitely-destructed (sometimes
also called finitely-observed). In other words, an element
belongs to a coinductively defined set if there
is no finite reason (i.e., no destruction sequence,
using the generator, starting from the element and ending
with some basis element) for the element not to belong to the
coinductive set. An example of a coinductive set, one that uses the
same generator and thus has the same basis as ℕ, is the
set ℕ_ω=ℕ∪{ω}. The infinite number ω
(which, perhaps confusingly, is sometimes encoded by the set ℕ
itself) belongs to ℕ_ω because ω—ruled
out by induction/finiteness from belonging to ℕ—cannot
be ruled out from belonging to ℕ_ω by a finite
construction sequence that uses F. Another coinductive set is the
set {ω} whose generator is similar to the successor function
but with an empty basis.

Even though coinduction is the dual of induction, and thus apparently
very similar to it, practical uses of coinduction are relatively obscure
compared to those of induction. For some applications of coinduction
see, e.g., <cit.>.




§ INDUCTION AND COINDUCTION INTUITIONS


To develop an intuition for coinduction, let's consider the intuition
behind induction first. While discussing the intuition behind induction
and the goal behind defining sets inductively, Enderton <cit.>
states the following (emphasis added)

“We may want to construct a certain subset of a set U by starting
with some initial elements of U, and applying certain [generating]
operations to them over and over again. The [inductive]
set we seek will be the smallest set containing the initial elements
and closed under the operations. Its members will be those elements
of U which can be built up from the initial elements by applying
the operations a finite number of times.

[...]

The idea is that we are given certain bricks to work with [i.e.,
the initial elements], and certain types of mortar [i.e.,
the generators], and we want [the inductive set] to contain
just the things we are able to build [with a finite amount of bricks
and mortar].”

Using this simple intuition we develop a similar intuition for coinduction.
Like for induction, we want to construct a certain subset of a set
U that includes some initial elements of U, and applying certain
generating operations to them over and over again. The coinductive
set we seek is now the largest set containing the initial elements
and consistent under the operations. As such, its members will
be those elements of U which can be built up from the initial elements
by applying the operations a finite or infinite number
of times.

The idea, as for induction, is that we are given certain bricks to
work with (i.e., the initial elements) and certain types
of mortar (i.e., the generators), and we want the coinductive
set to contain  all things we are able to fathom building
(with a finite or even infinite amount of bricks and mortar,
but, for consistency, using nothing else, i.e., without
using some other kind of building material such as glass or wood).

To illustrate this intuition, a couple of points are worthy of mention:


  * First, while being `closed under generating operations' seems
intuitive, being `consistent under generating operations'
may initially seem to be unintuitive, and thus be a main hinderance
in having an intuitive understanding of coinduction and coinductive
sets.

  * Second, inductiveness of a set necessitates that elements belonging
to the set result from applying the generating operations (i.e.,
generators) only a finite number of times. This finiteness
condition/restriction is a consequence of induction seeking the smallest
subset of U that can be constructed using the generators. As such,
to define a set inductively induction works from below (starts small)
and gets bigger using the generators (which sounds intuitive). Coinduction,
on the other hand, allows, but does not necessitate, applying the
generating operations an infinite number of times. This freedom is
part of coinduction seeking the largest subset of U that
can conceivably be constructed using the generators. As such, to define
a set coinductively, coinduction works from above (starts big) and
gets smaller (removing invalid constructions) using the “generating”
operations—which initially may seem unintuitive (in fact, as explained
precisely below, we will see that the complement of a coinductive
set is a closely-related inductive set, and vice versa

TODO. An adjunction seems to be at play here!

).

The best intuition regarding coinductive sets, however, seems to come
from the fact Kozen and Silva state in <cit.> that
relates coinductive sets to inductive sets and to set complementation
(which, supposedly, are two well-understood concepts):

“It is a well-known fact that a [set X] is coinductively
defined as the greatest fixpoint of some monotone operator [F]
iff its complement is inductively defined as the least fixpoint of
the dual operator; expressed in the language of μ-calculus, 

    ¬ν X.F(X)=μ X.¬ F(¬ X)

[i.e., ν X.F(X)=¬μ X.¬ F(¬ X)].”

(Note the triple use of complementation. The fact Kozen and
Silva state sounds to be indeed a true and intuitive one. Unfortunately,
however, in <cit.> Kozen and Silva only stated this fact
in a footnote, merely as a `well-known fact,' without them citing
any references to corroborate the fact).

Trying to understand the intuition behind this well-known fact, which
gives a simple but indirect definition of a coinductive set
in terms of an inductive one, gives an intuitive understanding of
coinductive sets; an understanding that depends only on the intuitive
understanding of inductive sets and of (set-theoretic) complementation.

In particular, to gain an intuitive understanding of coinductive sets
using this fact, we focus first on understanding the concept of the
`dual operator' F^δ of a monotone operator F defined
as 

    F^δ=¬∘ F∘¬

(where ∘ is the function composition operator). According to
the definition, the endofunction F^δ:𝕌→𝕌
is an operator on sets (i.e., on subsets of U) that, simply,
complements its input set, passes that complement to generator F,
then returns the complement of what F returns as its own result
set.

Given that F is assumed monotonic, F^δ is easily proved
to be monotonic too. That is, we have

    ∀ X,Y⊆ U.X⊆ Y F^δ(X)⊆ F^δ(Y),

because (by the contravariance of complementation[Also called antimonotonicity or antitonicity of ¬,
i.e., ∀ A,B⊆ U.A⊆ B¬ B⊆¬ A.]) we have X⊆ Y¬ Y⊆¬ X which (by
the monotonicity of F) implies that F(¬ Y)⊆ F(¬ X),
which implies (again, by complementation contravariance) that F^δ(X)=¬ F(¬ X)⊆¬ F(¬ Y)=F^δ(Y)
as required. As such, like F, F^δ is also a sets-generator.

Now, as a sets generator F^δ:𝕌→𝕌
has a least fixed point, called μ_F^δ, which is an inductively
defined set. The complement of set μ_F^δ (i.e.,
the set ¬μ_F^δ=U-μ_F^δ) is the coinductively
defined set we seek, i.e., is the the greatest fixpoint
of F (i.e., ν_F). As such, eliding the composition
operator (as is customary), we have

    ν_F=¬μ_¬ F¬

which, we believe, expresses precisely and concisely the intuition
behind coinduction and coinductive sets.




  §.§.§ Notes



  * Noting that complementing a finite subset of an infinite set U
produces a cofinite set (`the complement of a finite set'),
we can intuitively see that when starting with a finite set (the initial
“building bricks,” using Enderton's terminology) then applying
complementation thrice (as is done in the definition of ν_F)
defines some special sort of an infinite set (particularly, some special
sort of a cofinite set). This special sort of infinite sets constitutes
coinductive sets.

  * For example, given the Peano generator F(X):℘(ℕ)→℘(ℕ)={ 0}∪{ x+1|x∈ X}
that we discussed earlier, we have 

    F^δ(X)=ℕ-({ 0}∪{ x+1|x∈(ℕ-X)}).

As such, if ℕ^+ is the set of positive integers, ℕ_e
is the set of even natural numbers, and ℕ_o is the set
of odd natural numbers, then (as readers are invited to ascertain
for themselves) we have 

    F^δ(ϕ)=ϕ, F^δ(ℕ)={ 1,2,3,...} =ℕ^+, F^δ({0,1,2})={ 1,2,3} , F^δ({ 1,2})={ 2,3} ,


    F^δ(ℕ_o)=ℕ_e-{ 0} , F^δ(ℕ_e)=ℕ_o, and F^δ(ℕ^+)={ 0,1} =ℕ^++,

which intuitively justifies stating that F^δ(X)={ x+1|x∈ X}.[Note that for all X, F^δ(X) never contains
0 (i.e., the initial “bricks”), and also that F^δ(ℕ)=ℕ^+
and F^δ(ℕ^+)=ℕ^++ are proper
subsets of ℕ. Nevertheless, F^δ is monotonic—which
initially appears to defy intuition, as is usual when reasoning about
infinite sets.]

As is obvious from F^δ(ϕ), the set ϕ
is the least fixed point of F^δ, and thus μ_F^δ=ϕ.
Accordingly, we have 

    ν_F=ℕ-μ_F^δ=ℕ-ϕ=ℕ.

This means that, for this particular F (with the chosen domain
℘(ℕ)), we have μ_F=ν_F (i.e.,
the least fixed point and the greatest fixed point of F agree,
and F has only one fixed point). 

If the domain of F (successor) was larger than ℕ (e.g.,
contained the ordinals, or reals), then ν_F=??? ... TODO ...
reconciliate with coinductive types in FP, which assert that ν_F=ℕ∪{ω}.






To further strengthen our intuitions, let's consider yet a third
intuition about coinductive sets—the one offered in <cit.>,
which states that

“[An element] will belong to a coinductive [set] as long
as there is not a good finite reason for it not to.”

which is also expressed, a little less-precisely, in <cit.>
as

“A property [e.g., an element belonging to a set] holds
by induction if there is good reason [e.g., a finite construction
of the element] for it to hold; whereas a property holds by coinduction
if there is no good reason [e.g., a finite construction]
for it not to hold.”

Connecting these two similar intuitions with the prior intuition (i.e.,
the one based on Kozen and Silva's well-known fact), we can see that
the role of the dual operator F^δ (i.e., in defining
ν_F) is to define (inductively) those elements for which
there is “a good finite reason” to not belong to ν_F
(we call these the rejected elements). F^δ defines
these rejected elements by precomposing F with negation (set complementation)
then postcomposing the resulting operator with negation again. The
role of μ_F^δ, the least fixed set of F^δ,
is then to collect all these rejected elements (all of which
have a finite “bad” reason—i.e., inconsistency with F—to
belong, or, equivalently, a finite good reason not to belong),
and nothing but them (since μ_F^δ is a
minimal inductive set), in one set. Then, finally, the role of the
third (i.e., the outermost) negation in the definition of ν_F
is to exclude those rejected elements from belonging to ν_F
(the greatest fixed set of F).




  §.§.§ Notes



  * Combining the intuitive understanding of inductive and coinductive
sets, it is now easy to observe that a sets-generator F defined
over (subsets of) an infinite universe U defines three disjoint
(and possibly empty) subsets of U:



  * A set μ_F containing the “good and finite” elements of
U (relative to F) that “break no rules” (i.e., that
can be constructed by F, and are thus consistent with it), and
that can be constructed finitely (in a finite number of steps/applications
of F),

  * A set ν_F-μ_F (note that μ_F⊆ν_F always
holds) containing the “in-between, good but infinite” elements
of U (relative to F) that also break no rules, (i.e.,
can be constructed by F and are thus consistent with it), but that
cannot be finitely constructed by it (and thus do not belong to μ_F
but only to ν_F), and

  * A set U-ν_F containing the “bad” elements of U (relative
to F) that “break the rules” (of F) and thus cannot be finitely
or even infinitely constructed by F (i.e., are inconsistent
with F) and thus are not included even in ν_F (these are
elements of U that, whether finite or infinite elements, cannot
be constructed by F, whether F is applied a finite or infinite
number of times, and are thus “totally inconsistent” with F).


This observation can be summarized as saying that relative to a generator
F elements of set U are either: finitely-consistent with
F, infinitely-consistent with F, or (finitely or
infinitely) inconsistent with F.


  * An example of dual operators are the logical operators ∀
(forall) and ∃ (there exists) in first-order logic. Note
that ∀≡¬∃¬ and ∃≡¬∀¬.
Same applies for ∩ and ∪ (in set theory), and for ∧
and ∨ (in propositional logic). The statements that these pairs
of operators are dual operators are usually called `De Morgan's
Laws.'

TODO: Given the adjunction connection between ∀ and ∃
and preimages of functions <cit.>,
we expect category theory to tell us more about negation in categories
other than the category of sets.



  * Note that `complementation as negation' makes sense in set theory
(and, accordingly, also in structural type theory and in first-order
logic. See 

<ref>

4.1 and 

<ref>

5 of <cit.>), thus making coinductive sets (and
coinductive structural data types and coinductive first-order logical
statements) relatively simple to understand, i.e., are understandable
based on the intuitive understanding of inductive sets. A counterpart
of set-theoretic complementation may not, however, be easily definable
as the meaning of negation (¬) in other mathematical fields <cit.>.
This makes coinductive objects in these fields a bit harder to reason
about. (We intend to deliberate on this point more in future versions
of this article.

TODO

 But see also 

<ref>

3.2 of <cit.> for a discussion of type negation
in the context of OO/nominal type theory).

  * Another less-obvious instance of a coinductive set is the standard
subtyping relation in (nominally-typed) object-oriented programming
languages. See the notes of 2.2 of <cit.>
for more details.




§ ILLUSTRATING INDUCTION AND COINDUCTION


In this section we strengthen our intuitive understanding of pre-fixed
points, post-fixed points, and fixed points by illustrating these
concepts in set theory, and also by presenting a pair of examples
(and exercises) from analysis and number theory—examples that, as
such, are most likely familiar to many readers—that exemplify these
concepts.




 §.§ In Set Theory


Figure fig:Illus visually illustrates the main concepts we
discuss in this article in the context of set theory, by particularly
presenting the pre-/post-/fixed points of some abstract generator
F over the powerset (a complete lattice) 𝕌=℘(U)
for some abstract set U.



Figure <ref> illustrates that subsets U_1, U_2
and μ_F of U are among the F-closed/F-large/F-pre-fixed
subsets of U (i.e., the upper diamond, approximately), while
subsets U_3, U_4 and ν_F are among its F-consistent/F-small/F-post-fixed
subsets (i.e., the lower diamond, approximately). Of the sets
illustrated in the diagram, only sets μ_F and ν_F are
F-fixed subsets of U, i.e., belong to the intersection
of F-pre-fixed and F-post-fixed subsets (i.e., the inner
diamond, exactly). It should be noted that some other subsets of U
(i.e., points/elements of 𝕌) may neither be among
the pre-fixed subsets of F nor be among the post-fixed subsets
of F (and thus are not among the fixed subsets of F too). Such
subsets are not illustrated in Figure <ref>. (If drawn,
such subsets would lie, mostly, outside all three diamonds illustrated
in Figure <ref>.)

Figure <ref> also illustrates that μ_F≤ν_F

Intentional “mistake” of using ≤ rather than ⊆.

is true for any set U and any generator F. However, depending
on the particular F, it may (or may not) be the case that μ_F=ν_F
(e.g., if F is a constant function or if F happens to
have only one fixed point).[In the context of category theory, the symbol = is usually interpreted
as denoting an equivalence or isomorphism relation between
objects, rather than denoting the equality relation. See 6
of <cit.>.]

With little alterations (such as changing the labels of its objects,
the direction of its arrows, and the symbols on its arrows) the diagram
in Figure <ref> can be used to illustrate these same concepts
in the context of order theory, type theory, first-order logic or
category theory. (Exercise: Do that.)




 §.§ In Analysis


Most readers will definitely have met (and have been intrigued by?)
fixed points in their high-school days, particularly during their
study of analysis (the subfield of mathematics concerned with the
study of real numbers ℝ

, with functions over the real numbers,

 and with mathematical concepts related to them). To further motivate
the imagination and intuitions of readers, we invite them to consider
the function f:ℝ→ℝ defined as 

    f(x)=(x-5)^3-5x+29


same as

    F(x)=x^3-15x^2+70x-96=


and graphed in

SageMath: (plot([x,(x-5)ˆ3-5*x+29],(-1,10),color=['green','blue'],linestyle=['–','-'])
+ line([(2.65,0),(2.65,2.65)],color='lightgrey') + line([(4.82,0),(4.82,4.82)],
color='lightgrey') + line([(7.52,0),(7.52,7.52)], color='lightgrey')).show(ymin=-1,ymax=9) 


 Figure fig:fixed-zeros. In particular, we invite the reader
to decide: (1) which points of the totally-ordered real line
(the x-axis) are pre-fixed points of f, (2) which points/real
numbers are post-fixed points of f and, (3) most easily, which
points are fixed points of f.[To decide these sets of points using Figure <ref>,
readers should particularly take care: (1) not to confuse the fixed
points of f (i.e., crossings of the graph of f with the
graph of the identity function, which are solutions of the equation
f(x)-x=0) with the zeroes of F (i.e.,
crossings with the x-axis, which are solutions of the equation
f(x)=0), and (2) not to confuse pre-fixed points of
f for its post-fixed points and vice versa.

Since F is not a monotonic function (i.e., is not
a generator) we compensate by giving some visual hints in Figure <ref>
so as to make the job of readers easier. The observant reader will
recall that diagrams such as that in Figure <ref>
are often used (e.g., in high-school/college math textbooks),
with “spirals” that are zeroing in on fixed points overlaid on
the diagrams, to explain iterative methods—such as the renowned
Newton-Raphson method—that are used in numerical analysis to compute
numerical derivatives of functions in analysis. These methods can
be easily seen to be seeking to compute fixed points of some related
functions. As such, these numerical analysis methods for computing
numerical derivatives can also be explained in terms of pre-fixed
points and post-fixed points.]

(Exercise: Do the same for the monotonic function g:ℝ→ℝ
defined as

    g(x)=x^24    0≤ x<4
    
    x     4≤ x≤6
    (x-8)^34+8     6<x≤10

and depicted in

SageMath: (plot([x],(-1,10),color=['green'],linestyle=['–'])+plot([xˆ2/4],(0,4),color=['blue'],linestyle=['-'])+plot([x],(4,6),color=['blue'],linestyle=['-'])+
plot([(x-8)ˆ3/4+8],(6,10),color=['blue'],linestyle=['-'])+line([(4,0),(4,4)],color='lightgrey')+line([(6,0),(6,6)],color='lightgrey')+line([(8,0),(8,8)],color='lightgrey')).show(ymin=-1,ymax=10) 


 Figure fig:fixed-set, and then relate your findings to Figure <ref>

TODO: fig:Illus

. Now also relate your findings regarding f(x) in Figure fig:fixed-zeros—or
regarding mono­tonic/mono­tonically-increasing and anti­monotic/mono­tonically-decreasing
sections of f(x)—to Figure <ref>. Based
on your relating of Figure <ref> and Figure <ref>
to Figure <ref>, what do you conclude?).

The main goal of presenting these two examples from analysis is to
let the readers strengthen their understanding of pre-/post-/fixed
points and dispel any misunderstandings they may have about them,
by allowing them to connect examples of fixed points that they are
likely familiar with (i.e., in analysis) to the more general
but probably less familiar concepts of fixed points found in order
theory, set theory, and other branches of mathematics. Comparing the
illustration of fixed points and related concepts in set theory (e.g.,
as in Figure <ref>) with illustrations of them using examples
from analysis (e.g., as in Figure <ref> and
Figure <ref>) makes evident the fact that a function
over a partial order (such as 𝕌) is not as simple to imagine
or draw as doing so for a function over a total order (such as ℝ)
is. However, illustrations and examples using functions over total
orders can be too specific and thus misleading, since they may hide
the more generality, the wider applicability, and the greater mathematical
beauty of the concepts depicted in the illustrations.




 §.§ In Number Theory


For a non-visual example, consider perfect numbers in arithmetic.[This example is taken from <cit.>. The example,
being tangential and in a different context than ours, is mentioned
without reference to pre-/post-/fixed points. More on perfect
numbers can be found in other standard texts on arithmetic and number
theory.] A positive integer is perfect if it equals the sum of its
smaller divisors, e.g., 6=1+2+3. It is deficient (or
abundant) if the sum of its smaller divisors is less then (or
greater than, respectively) the number itself. The first four perfect
numbers are 6, 28, 496, and 8128.

A watchful reader will immediately note that deficient numbers are
the proper pre-fixed points (ones that are not fixed points) of a
function from numbers to numbers, abundant numbers are the proper
post-fixed points of the function, and perfect numbers are its fixed
points. That function, namely, is the endofunction that sums the smaller
divisors of its input number.

Lets call this function sd (for `sum of divisors'). If ℙ
is the (totally-ordered) set of positive whole numbers, then deficient
numbers are exactly the members of the set dn={ p∈ℙ|sd(p)<p}
of proper pre-fixed points of sd, abundant numbers are exactly
members of the set an={ p∈ℙ|p<sd(p)}
of proper post-fixed points of sd, and perfect numbers are exactly
members of the set pn={ p∈ℙ|p=sd(p)}
of fixed points of sd. (Note that sd is not a mono­tonic/co­var­iant/in­creas­ing/mono­tonically-in­creasing
function, and that ℙ is not a complete lattice.
However, the notions pre-fixed points, post-fixed points, and fixed
points still have relevance in such a context. See 

<ref>

2.2 of <cit.> for a similar situation.)

plain
10
	
	AbdelGawad2018f
	Moez A. AbdelGawad.
	Induction, coinduction, and fixed points in order theory, set theory,
	type theory, first-order logic, and category theory: A concise comparative
	survey.
	eprint available at http://arxiv.org/abs/1812.10026, 2018.
	
	AbdelGawad2019b
	Moez A. AbdelGawad.
	Induction, coinduction, and fixed points in programming languages
	type theory.
	eprint available at http://arxiv.org/abs/1902.xxxxxx, 2019.
	
	Bertot2004
	Yves Bertot and Pierre Casteran.
	Interactive Theorem Proving and Program Development Coq'Art: The
		Calculus of Inductive Constructions.
	Springer, 2004.
	
	Brandt1998
	M. Brandt and F. Henglein.
	Coinductive axiomatization of recursive type equality and subtyping.
	Fundamenta Informaticae, 33(4):309–338, 1998.
	
	EndertonLogic72
	Herbert B. Enderton.
	A Mathematical Introduction to Logic.
	Academic Press, New York, 1972.
	
	Enderton77
	Herbert B. Enderton.
	Elements of Set Theory.
	Academic Press, New York, 1977.
	
	Forster2003
	Thomas Forster.
	Logic, Induction, and Sets.
	London Mathematical Society Student Texts. Cambridge University
	Press, 2003.
	
	Greiner92
	John Greiner.
	Programming with inductive and co-inductive types.
	Technical Report CMU-CS-92-109, School of Computer Science, Carnegie
	Mellon University, Jan 1992.
	
	Halmos60
	Paul R. Halmos.
	Naive Set Theory.
	D. Van Nostrand Company, Inc., 1960.
	
	GEB
	Douglas R. Hofstadter.
	Gödel, Escher, Bach: an Eternal Golden Braid.
	Basic Books, second edition, 1999.
	
	Horn2001
	Laurence R. Horn.
	A Natural History of Negation.
	CSLI Publications, 2001.
	
	Kozen2016
	Dexter Kozen and Alexandra Silva.
	Practical coinduction.
	Mathematical Structures in Computer Science, 27(7):1132–1152,
	2016.
	
	McLenn2018
	Andrew McLennan.
	Advanced Fixed Point Theory for Economics.
	Springer, 2018.
	
	Penrose2004
	Roger Penrose.
	The Road to Reality: A Complete Guide to the Laws of the
		Universe.
	Jonathan Cape, 2004.
	
	TAPL
	Benjamin C. Pierce.
	Types and Programming Languages.
	MIT Press, 2002.
	
	DM
	Kenneth A. Ross and Charles R. B. Wright.
	Discrete Mathematics.
	Prentice Hall, third edition, 1992.
	
	Sangiorgi2012
	Davide Sangiorgi.
	Introduction to Bisimulation and Coinduction.
	2012.
	


