Dear Paolo!

I will send you several papers by surface mail tomorrow, 
including a letter of thanks and copy of my suggestions for our joint paper.

If you cannot wait, you can access that copy also via

http://www.ags.uni-sb.de/~cp/p/bussottiwirth/pdf.pdf

An ascii version is also found in the postscript.

You may edit it (do not try to read it, find place for insertion by search)
and send it back to me as an response and to 
bring it into accordance with TeX. You should know that a percentage
sign (%) makes TeX ignore the rest of the line.
Everything else is so simple that you will easily guess it.
But do not waste your precious time on TeX, where I am the expert.

Kind regards, also to your mother,
CP

\section{Introduction}\label
{section Introduction}
In this \daspaper\ we contribute to the 
meta-level knowledge on
the method of mathematical induction and its heuristics. \
Our interest is in the practical proof search of the working mathematician,
but not in the well-known proof-theoretical peculiarities of 
mathematical induction 
that actually do not really have a
practical effect; \ 
\cfnlb\ 
\cite{goedel}, \cite{goedelcollected} for enumerability; \ 
\cite{induction-no-cut} for cut elimination; \ 
\cite{swp200601}, \litnoteref{4} for practical irrelevance. \

We are not interested in the induction methods for simple 
proofs at the level of freshmen 
or at the level of fully automated inductive theorem proving systems.
%by\emph{explicit induction}, such as \ACLTWO\ 
%(\cfnlb\ \cite{ACLTWO,waltherhandbook,bundy-survey}).
To the contrary, we are interested in such proof tasks whose 
level of difficulty requires some ingenuity in proof search and an
explicit presentation in an advanced mathematical publication.
The order in a succinct presentation---say in a journal---more 
often than not
differs from the way the proof was originally found.
Most non-trivial proofs by induction are actually found by the\emph
{Method of \DescenteInfinie}.
This 
the standard induction method for non-trivial proof tasks
of the working mathematician
from the ancient Greeks until today.
It got lost in the Middle Ages and was reinvented and named by \fermat,
\nolinebreak\cfnlb\ \sectref{section Historical Problems}.

Besides using the standard knowledge of working mathematicians,
we approach the Method of\emph\DescenteInfinie\ from two sides,
namely from its history (\cf\ \cite{From-Fermat-to-Gauss})
and from its logical description for 
human-oriented computer-assisted theorem proving (\cfnlb\ \cite{wirthcardinal}).

As a first step we subdivide the Method of\emph\DescenteInfinie\ 
into the sub-methods of\emph{\noetherian\ induction}, indefinite descent,
and reduction-descent, as classified in the following table.
\par\halftop\noindent\LINEnomath{\begin{tabular}{l||l|l}
  \bf\em\DescenteInfinie
 &\bf without Exceptions
 &\bf with Special Cases
\\\hline\hline\bf affirmative
 &\noetherian\ induction
 &affirmative reduction-descent
\\\hline\bf apagogic
 &indefinite descent
 &apagogic reduction-descent
\\\end{tabular}}\par\yestop\noindent
Note that this
table does not refer to positive or negative propositions
(which is a matter of choice of linguistic formulation)
but to affirmative (positive) and apagogic 
(``that lead you away from\closequotecomma negative, refutational) 
methods of demonstration.

\section{Motivation}
\ednote{Thi\es\ may be too long here. But we may remove it in the completed
paper, after it ha\es\ been part of OUR motivation!}

Mathematical methods are still taught only by paradigmatic examples.
This has the advantages that lecturers do not have to provide 
meta-level descriptions of the methods 
and that students can proceed by a stepwise understanding
of concrete examples and then use their 
highly-developed inductive-learning abilities. 
(Note that inductive learning is learning by examples and has nothing 
to do with mathematical induction in general.)
The disadvantage of this procedure of teaching and learning, however, is that 
nobody really knows what a certain method exactly is and what the heuristics
for its application are.
While the whole process of mathematical theory development
and theorem proving might never be grasped by the human intellect 
on the meta level,
we are convinced that 
meta-level descriptions of standard proof methods are indeed possible.
Such meta-level descriptions could be beneficial\begin{enumerate}
\noitem\item to improve the clarity of mathematical discussion,
\noitem\item to ensure the success of inductive learning by providing
a meta-level description in the conclusion,
\noitem\item to refine the understanding of the history of the methods, 
\noitem\item to apply methods in software systems that assist 
the working mathematician in his daily work 
(\MASlong s, \cfnlb\ \cite{omegacadetwo,pds}),
and
% \noitem\item to implement the guidance and control 
% in computer-assisted learning systems for mathematics 
% % This seems to be something for the 22nd century, not for now
\noitem\end{enumerate}
This is not conceptually opposed 
to the wide-spread belief that a scientific\emph
{paradigm} does not need any concrete meta-level 
rules and that such rules would destroy
scientific creativity, \cfnlb\ \cite{kuhn,against-method}.
Indeed, the history of mathematics shows
that concrete meta-level rules are not essential.
As paradigm changes in mathematics are rarer
than in natural sciences, we think that it is time to approach
such meta-level descriptions for the classical methods in mathematics.
And, if the enterprise of formulating these rules is successful,
we still do not have to teach them if they are then
found out to destroy creativity.
%
Mathematical induction is an excellent candidate for starting this
very difficult enterprise, because it is 
that area of mathematical theorem 
proving where our heuristic knowledge is best.
This is the case both for 
human and for machine-oriented heuristics, \cfnlb\ \cite{swp200601}.

We are quite aware of the difficulty of our enterprise
and that the most advanced meta-level descriptions of 
mathematical methods in computer-assisted theorem proving 
and proof planning
have not yet reached the level of difficulty we intend for our proofs,
\cfnlb\ \cite
{bundy-inductive-proof-planning,meierproofplanningone,meierproofplanningtwo,wirthcardinal,samoa-phd}.
Nevertheless, we are confident to do a first practically relevant step 
toward the meta-level description of the Method 
of\emph\DescenteInfinie\ and its application heuristics
on the level of difficulty described in \sectref{section Introduction}.

Besides clearly describing the Method of\emph\DescenteInfinie\ 
on a refined level and besides providing the paradigmatic historical examples,
we want to develop some deeper knowledge on the area of application
of certain sub-methods, for instance to find out
why the method of\emph{reduction-descent}
is rarely applied apagogically.

\section{Historical Problems}\label
{section Historical Problems}
\ednote{To be written by  Paolo!}
\subsection{\euclid}
\subsection{\fermat's \pythagorean\ Triangle}
\subsection{One of \euler's Demonstrations by Reduction-Descent}
\eulername\ \eulerlifetime
\subsection{Where these Methods are Used}

\section{Logical Considerations}
\subsection{Logical Equivalence}
\noindent\thelogicalpointofview

The proposition to be proved by\emph\descenteinfinie\
is represented in \inpit{\ident{N}} by \bigmaths{\forall x\stopq\app P x}. \ 
Roughly speaking, 
\mbox{a\emph{counterexample}}
for \nlbmath\Gamma\ is an instance \nlbmath{a} for which 
\bigmath{\neg\app P a}{} holds, but we should be more careful here 
because this is actually a semantical notion and not a syntactical one;
\cfnlb\ \cite{wirthcardinal}, \litsectref{2.3.2}. \ 
To treat counterexamples properly,
a logic that actually models
the mathematical process of proof search by\emph\descenteinfinie\ itself and 
directly supports it with the data structures required for a formal treatment
requires a semantical treatment of free variables.
The only such logic can be found in \cite{wirthcardinal}.

The level of abstraction of our previous 
discussion of\emph\descenteinfinie\
is well-suited for the description of the structure of 
mathematical proof search in two-valued logics,
where the difference between a proof by contradiction and a
positive proof of a given theorem is only a linguistic one and
completely disappears when we formalize these proofs in a 
state-of-the-art modern logic calculus, such as the one of 
\cite{wirthcardinal}.
An investigation into the history of mathematics, however, also 
has to consider the linguistic representation and the 
exact logical form of the presentation.

We suggest the following classification scheme for proof by mathematical
induction, which is unproblematic in the sense that it does not
refer the working mathematician's consciousness, but only to the written
documents.
It suffices to speak of \begin{enumerate}\noitem\item
quasi-general proofs (\ie\ proofs by generalizable examples)
\ednote{Thi\es\ ha\es\ to be explained somewhere!}, 
\noitem\item general proofs 
(\ie\ proofs we would accept from our students in an examination today), 
\noitem\item
proofs with an explicit statement of the related instance 
of an induction axiom or theorem,
and \noitem\item
proofs with an explicit statement of an induction axiom or theorem itself.
\end{enumerate}
There is evidence that 
such a linguistic and logic-historical refinement
is necessary to understand the fine structure of historical reasoning
in mathematics.
For instance, in \euclid's Elements
\litpropref{VIII.7} is just the contrapositive of \litpropref{VIII.6}, 
% \ (\cfnlb\ our \cororef{corollary Euclid VIII 7} 
% and \lemmref{lemma Euclid VIII 6}, \resp), \ 
and this is just one of several cases that we find a proposition with
a proof in the Elements, where today we just see a corollary.
Moreover, even \fermat\ reported in his letter 
for \huygens\ \ednote{Thi\es\ ha\es\ to be presented somewhere!}
that he had had problems to apply the Method of\emph\DescenteInfinie\
to positive mathematical statements.
\begin{quote}``\frenchtextone''
\getittotheright{\opt{\cite{fermat-oeuvres}, \Vol\,II, \p\,432}}
\par\halftop\noindent``\frenchtextoneinenglish'' 
\getittotheright{(our translation)}
\end{quote}
Due to the work of \frege\ and \peano,
these logical differences may be considered trivial today.
Nevertheless, they were not trivial before, and to understand the
history of mathematics and the fine structure in which mathematicians reasoned,
the distinction between affirmative and negative theorems 
and between direct and apagogic methods of demonstration is important.

Therefore, in \cite{From-Fermat-to-Gauss}, following the above statement of
\fermat,
the Method of\emph\DescenteInfinie\
is subdivided into\emph{indefinite descent} \nlbmath{\inpit{\ident{ID}}} 
and\emph{reduction-descent} \nlbmath{\inpit{\ident{RD}}}:
\par\halftop\noindent\math{\begin{array}{@{}l@{\ \ \ }r@{\ }l@{}}
  \inpit{\ident{ID}}
 &\forall P\stopq
 &\inparentheses{\headroom
      \forall x\stopq\app P  x
    \nottight{\nottight{\nottight{\nottight\antiimplies}}}
      \exists\tight<\stopq\inparenthesesoplist{
       \forall v\stopq\inparentheses{
            \neg\app P  v
          \nottight{\nottight\implies}
            \exists u\tight<v\stopq\neg\app P  u}
     \oplistund
        \Wellfpp <}}
\\
\\\inpit{\ident{RD}}
 &\forall P\stopq
 &\inparentheses{
      \forall x\stopq\app P  x
    \nottight{\nottight{\nottight{\nottight\antiimplies}}}
      \exists\tight<\stopq\exists S\stopq\inparenthesesoplist{
       \forall u\stopq\inparentheses{
            \app S u\nottight{\implies}\app P u}
     \oplistund
       \forall v\stopq\inparenthesesoplist{
            \neg\app S v\und\neg\app P  v
          \oplistimplies
            \exists u\tight<v\stopq\neg\app P  u}
     \oplistund
        \Wellfpp <}}
\\\end{array}}
\par\yestop\noindent
Actually the \Wellfpp< does not occur in \cite{From-Fermat-to-Gauss}
because for \fermat\ the Method of\emph\Descenteinfinie\ was actually 
restricted to the wellfounded ordering of the natural numbers.

% Although \inpit{\ident{N}}, \inpit{\ident{ID}}, and \inpit{\ident{RD}}
% are logically equivalent in two-valued logics, 
% according to \cite{From-Fermat-to-Gauss}\emph
% \descenteinfinie\ does not subsume
% proofs by \noetherian\ or structural induction. 
% This is in opposition to our more coarse-grained discussion above.
% With this fine-grained distinction, on \p\,2 of
% \cite{From-Fermat-to-Gauss} we find the surprising claim
% that there is only a single proof by indefinite descent in the whole
% Elements, namely the above-cited Proof of \litpropref{VII.31}\@. \ 
% Indeed, at least all those proofs in the Elements besides VII.31 
% which I reexamined and which proceed by mathematical induction,
% actually proceed by reduction-descent or structural induction,
% but not by indefinite descent:
% The correctness proofs of the 
% \euclid ian Algorithm (\litpropref{VII.2}
% and \litpropref{X.3}) are reduction-descents
% with a horrible linguistic surface structure.
% Similarly, the proofs of \litproprefs{IX.12}{IX.13} are reduction-descents
% with superfluous sentences confusing the proof idea.

Notice that, as already repeatedly expressed above, a logical formalization 
cannot capture a mathematical method. Moreover, as also already
expressed above for \noetherian\ and structural induction,
logical equivalence of formulas does not imply the equivalence of the
formalized methods. 
For an interesting discussion of this difficult subject 
\mbox{\cf\ \cite{From-Fermat-to-Gauss}, \litchapref 7}.

\begin{sloppypar}
Nevertheless, \inpit{\ident{N}}, \inpit{\ident{ID}}, and \inpit{\ident{RD}}
sketch methods of proof search equivalent for the 
working mathematician of today.
Indeed: \inpit{\ident{ID}}---roughly speaking---is the 
\mbox{contrapositive of \inpit{\ident{N}}}, 
which means that in two-valued logics
the methods only differ in verbalization.
Moreover, 
a proof by \inpit{\ident{ID}} is a proof by \inpit{\ident{RD}}
when we set \math S to the empty predicate.
Finally, a proof by \inpit{\ident{RD}} can be transformed into a proof by
\inpit{\ident{ID}} as follows:
Suppose we have proofs for the statements in the conjunction 
of the premise of \nlbmath{\inpit{\ident{RD}}}.
The proofs of 
\ \mbox{\math{\forall u\stopq\inparentheses{
\app S u\nottight{\implies}\app P u}}} \ 
\\and \hfill{\maths{\forall v\stopq\inparenthesesoplist{
            \neg\app S v\und\neg\app P  v
          \oplistimplies
            \exists u\tight<v\stopq\neg\app P  u}}{} \hfill
give a proof of \hfill\maths{\forall v\stopq\inparenthesesoplist{
            \neg\app S v\und\neg\app P  v
          \oplistimplies
            \exists u\tight<v\stopq\inpit{\neg\app S v\und\neg\app P  u}}}.}\\
Instantiating the \math P in \inpit{\ident{ID}} via
\bigmaths{\{P \mapsto\lambda z\stopq\inpit{\app S z\oder\app P z}\}},
the latter proof can be schematically transformed into a proof of \bigmaths
{\forall x\stopq\inpit{\app S x\oder\app P x}}{} by 
\bigmaths{\inpit{\ident{ID}}}. \ 
And then from the proof of \ \mbox{\math{\forall u\stopq\inparentheses{
\app S u\nottight{\implies}\app P u}}} \ again,
we get a proof of \bigmaths{\forall x\stopq\app P  x}, as intended. \ 
Thus, in any case, the resulting proof does not significantly 
differ in the mathematical structure from the original one.
\end{sloppypar}

Notice that this is contrary to the case of \noetherian\ \vs\ structural 
induction,
where the only transformation I see from the former to the latter 
\ (the other direction is trivial, 
   \cfnlb\ \cite{wirthcardinal}, \litsectref{1.1.3}) \ 
is to show that the\emph{axiom} \inpit{\ident{S}} implies \Wellfpp\ssymbol,
and then leave the application of \inpit{\ident{N}} unchanged.
This 
% which makes a significant difference in structure,
% although it is not even a 
transformation, however, is not complete because it does not remove the
application of \inpit{\ident{N}}, which is a\emph{theorem} anyway.

All in all, this shows that---while structural and \noetherian\ induction
vastly differ in practical applicability---for a working mathematician today
it is not important for his proof search to be aware of
the differences between 
\noetherian\ induction \nlbmath{\inpit{\ident{N}}}, 
indefinite descent \nlbmath{\inpit{\ident{ID}}}, and 
reduction-descent \nlbmath{\inpit{\ident{RD}}}. \ 

\subsection{Relevance for Mathematical Methods}

\section{Discussion}

\section{Conclusion}