REFLECTIONS ON THE TERMINOLOGY OF "NECESSARILY NON-ANALYTIC INDUCTION PROOFS"
═════════════════════════════════════════════════════════════════════════════

Anders Lundstedt (anders.lundstedt@philosophy.su.se)

2020-02-04


In my research project with the preliminary title "Necessarily non-analytic
induction proofs" I investigate the phenomenon where some mathematical facts
seem to not lend themselves to a "straightforward" induction proof. Sometimes it
does not seem possible to prove a fact ∀x.φ(x) by induction with φ(x) as
induction hypothesis. Instead what works is to prove some other fact ∀x.ψ(x) by
induction (with ψ(x) as induction hypothesis), and ∀x.φ(x) then follows from
∀x.ψ(x). Typically this proof method is called something like "strengthening of
the induction hypothesis". However, there need not always be any precise sense
in which ψ(x) is stronger than φ(x). Thus a more general terminology is wanted.

                                       ∗∗

Hetzl and Wong (2017) have made precise sense of what it would mean that a
fact cannot be proved by "straightforward induction". They proved that
"inductive theorem proving requires non-analytic induction axioms", which can be
phrased precisely as follows. An induction axiom

      φ(0)∧∀x(φ(x)→φ(x+1))→∀x.φ(x)

is ∗non-analytic∗ for a sentence σ if φ(x) is not an instance of a subformula of
σ. Then there are consequences PA ⊢ σ any derivation of which must make use of
induction axioms that are non-analytic for σ.

                                       ∗∗

Based on the notions introduced by Hetzl and Wong, I have made the following
definitions (Lundstedt, 2020).

                                       ∗∗

DEFINITIONS.

─ A first-order language is a ∗(first-order) language of arithmetic∗ if and only
  if it is an expansion of the language ⟨0,1,+⟩.

─ Let L be a language of arithmetic.

  ─ Let φ(x) be an L-formula in the free variable x. The ∗induction instance∗
    for φ is the L-sentence

          IND(φ) :≡ φ(0)∧∀x(φ(x)→φ(x+1))→∀x.φ(x).

  ─ Let T be an L-theory and let φ(x) and ψ(x) be L-formulas in the free
    variable x. Say that ∗ψ(x) witnesses that T proves ∀x.φ(x) by necessarily
    non-analytic induction∗ if and only if

    (1)   T,IND(φ) ⊬ ∀x.φ(x),

    (2)   T ⊢ φ(0),

    (3)   T ⊢ ψ(0),

    (4)   T ⊢ ∀x: ψ(x)→ψ(x+1),

    (5)   T ⊢ ∀x.ψ(x)→∀x.φ(x).

                                       ∗∗

As used here, there are at least two problems with the terminology "T proves
∀x.φ(x) by necessarily non-analytic induction":

(P1)  If (1)–(5) holds then T does not actually prove ∀x.φ(x)──rather it is T
      together with an appropriate induction axiom that prove ∀x.φ(x). Thus "T
      proves ∀x.φ(x) ..." is a bit misleading.

(P2)  It is possible to construct T, φ(x) and ψ(x) such that (1)–(5) holds while
      IND(ψ) is not non-analytic for ∀x.φ(x). Indeed, suppose we have:

            ψ(x) witnesses that T proves ∀x.φ(x) by necessarily non-analytic
            induction.

      Suppose we also have the following strengthening of (5):

      (5')  T ⊢ ∀x: ψ(x)→φ(x).

      (See for example my summary of results (Lundstedt, 2020) for cases where
      (5') holds in addition to (1)–(5).) Then it is an easy exercise to verify
      that we have:

            ψ(x) witnesses that T proves ∀x: φ(x)∨ψ(x) by necessarily
            non-analytic induction.

      But ψ(x) is a subformula of φ(x)∨ψ(x) and thus IND(ψ) is not non-analytic
      for ∀x: φ(x)∨ψ(x). Thus we should not say that T proves ∀x: φ(x)∨ψ(x) by
      necessarily non-analytic induction.

                                       ∗∗

I think a good solution to (P2) would be to simply replace 'non-analytic' with
'non-straightforward'. For solving (P1) I could change the terminology to
something like "T IND-proves ∀x.φ(x) ..." where IND-proves would mean that T
proves ∀x.φ(x) in a first-order logic extended with an induction rule. Right now
I do not know whether this would be a good solution. To avoid extra work I will
keep the terminology as it is until I have solutions to both (P1) and (P2) that
I am happy with.

                                       ∗∗

I will probably replace 'non-analytic' with 'non-straightforward'. But perhaps
it would also make sense to keep an alternative version of the definition where
we keep 'non-analytic' and replace (1) with

(1')  T,IND(β) ⊬ ∀x.φ(x) for all instances β(x) of subformulas of φ(x).

                                       ∗∗

OPEN QUESTION: Would there be any point in point in having such an alternative
definition? Put differently, would there be any point in distinguishing between
'necessarily non-analytic' and the more general 'necessarily
non-straightforward'?

                                       ∗∗

Another terminological problem concerns the title of the research project, even
if changed to "Necessarily non-straightforward induction proofs". The problem is
roughly that it is superfluous to call a non-straightforward induction proof
'necessarily non-straightforward'. On the most reasonable (at least in my
opinion) literal reading, any non-straightforward induction proof is necessarily
non-straightforward, since any straightforward induction proof of the same fact
would be a different proof.

                                       ∗∗

I think the following radical change of terminology would solve all above
problems. Simply call a consequence T ⊢ ∀x.φ(x) 'non-straightforward' if any
derivation of it must make use of induction axioms other than IND(φ). (We could
define 'non-analytic' consequences similarly.) A drawback with this solution is
that 'non-straightforward consequence' is quite non-descriptive.

                                       ∗∗

References
──────────

Hetzl, Stefan and Tin Lok Wong (2017): "Some observations on the logical
foundations of inductive theorem proving", Logical Methods in Computer Science
13(4).

Lundstedt, Anders (2020): "Necessarily non-analytic induction proofs──summary of
some results", manuscript, version 2020-01-22,
https://anderslundstedt.com/research/non-analytic-induction/all-files.html.