#  Quantifier-free induction for lists

Stefan Hetzl111corresponding author Vienna University of Technology
Institute of Discrete Mathematics and Geometry<EMAIL_ADDRESS>Jannik Vierling  Vienna University of Technology
Institute of Discrete Mathematics and Geometry<EMAIL_ADDRESS>
###### Abstract

We investigate quantifier-free induction for Lisp-like lists constructed
inductively from the empty list $\mathit{nil}$ and the operation
$\mathit{cons}$, that adds an element to the front of a list. First we show
that, for $m\geq 1$, quantifier-free $m$-step induction does not simulate
quantifier-free $(m+1)$-step induction. Secondly, we show that for all $m\geq
1$, quantifier-free $m$-step induction does not prove the right cancellation
property of the concatenation operation on lists defined by left-recursion.

Keywords: weak theories of arithmetic, theories of lists, automated inductive
theorem proving, transfinite lists

##  1 Introduction

In this article we consider Lisp-like lists in the context of the automation
of proof by mathematical induction. The subject of automated inductive theorem
proving (AITP) aims at automating the process of proving statements about
inductively constructed objects such as natural numbers, lists and trees. The
formal verification of software is a particularly prominent application of
automated inductive theorem proving. Since every non-trivial program contains
loops or recursion, some form of mathematical induction is necessary to reason
about such programs. By Gödel’s incompleteness theorem the task addressed by
AITP is in general not even semi-decidable. Therefore, there is a lot more
freedom in the choice of the proof systems than in the case of first-order
validity. For that reason and because of technical constraints, a great
variety of methods have been developed for that purpose. To name just a few
examples, there are methods based on recursion analysis [5], integration into
saturation-based provers [26, 21, 10], cyclic proofs [3], theory exploration
[6], proof by consistency [8].

The current methodology in automated inductive theorem proving concentrates
primarily on the implementation of systems and their empirical evaluation. The
work in this article is part of a research program that aims at complementing
this state of the art by focusing on the formal analysis of methods for
automated inductive theorem proving. In particular, we aim at understanding
the theoretical limits of systems by developing upper bounds on the logical
strength of methods. Establishing sufficiently tight upper bounds on the
strength of AITP systems often allows us to provide practically meaningful
unprovability results whereas an empirical evaluation only shows the failure
of a particular implementation. Moreover, upper bounds typically reveal the
particular form of induction underlying the AITP systems. This knowledge
permits the direct comparison of methods and helps in judging the
applicability of AITP systems to certain domains.

So far the work in this research program [20, 17, 18, 19, 31] has concentrated
on induction for natural numbers only. However, since lists and other
inductive data types are fundamental structures of computer science, it is of
paramount importance for the subject of AITP to analyze the mechanical
properties of these inductive datatypes. In this article we make a first
important step towards extending this research program to inductively defined
lists. In particular, we show that the right cancellation property of the
concatenation of lists is not provable by a form of induction used in some
automated inductive theorem proving systems. With this result we pave the way
for obtaining further unprovability results for AITP systems on lists and
other inductive data types.

In the following we briefly mention some aspects of axiomatic theories of
finite lists have been studied in theoretical computer science. In [23] an
axiomatic theory of linear lists (Lisp-like lists) is defined and some basic
results about consistency, completeness, and independency of the axioms are
shown. Similar theories are considered in a more general setting in [24]. In
[12, 2, 1] the computability aspects of list structures are investigated.

Axiomatic theories of lists are closely related to theories of concatenation
studied in logic [29, 25]. Theories of concatenation axiomatise strings of
symbols over a finite alphabet. Theories of concatenation have been proposed
as alternative basic systems for the development of metamathematical results
such as Gödel’s incompleteness theorems and computability [32, 13, 14, 9, 30].
In such theories there is no need to develop a coding of finite sequences [25,
13]. Hence, theories of concatenation permit a more natural development of
syntax.

In this article we consider the provability of the right-cancellation of the
concatenation of finite lists from quantifier-free big-step first-order
induction for Lisp-like lists. After recalling some basic concepts and
notations in Section 2, we show the two main results of this article in
Sections 3 and 4. First, in Section 3, we show that in general $m$-step
quantifier-free induction does not prove $(m+1)$-step quantifier-free
induction. This results sets induction on lists in contrast with induction for
natural numbers where big-step quantifier-free induction is not stronger than
one-step quantifier-free induction. Secondly, in Section 4, we show that for
all $m\geq 1$, $m$-step induction, over the language consisting of the list
constructors and a concatenation operator, does not prove the right
cancellation property of the concatenation operation. In order to show these
unprovability results we will construct models whose domain contains sequences
of transfinite length.

##  2 Preliminaries

In this section we introduce some concepts, notations, and results that we
will use throughout the article. In Section 2.1 we recall some basic concepts
and notations of many-sorted first-order logic. Section 2.2 defines some basic
axioms of the list constructors and the traditional induction schema for lists
as well as related terminology. Finally, in Section 2.3 we introduce some
concepts on transfinite sequences, which we will use in the model theoretic
constructions of Section 3 and Section 4.

###  2.1 Many-sorted first-order logic

We work in the setting of classical many-sorted first-order logic with
equality. Let $S$ be a finite set of sorts, then for each sort $s\in S$ we let
$\mathfrak{V}_{s}$ be a countably infinite set of variable symbols of the sort
$s$. We write $x:s$ to indicate that $x$ is a variable symbol of sort $s$,
that is, $x\in\mathfrak{V}_{s}$. When the sort of a variable is irrelevant or
clear from the context, we omit the sort annotation and simply use the
variable symbol. We assume that the sets of variable symbols for the sorts in
$S$ are pairwise disjoint. A many-sorted first-order language $\mathcal{L}$
over the sorts $S$ is a set of predicate symbols of the form
$P:s_{1}\times\dots\times s_{n}\to o$ and function symbols of the form
$f:s_{1}\times\dots\times s_{n}\to s_{n+1}$, where $P,f$ are symbols,
$s_{1},\dots,s_{n},s_{n+1}\in S$ and $o$ is a special sort symbol assumed not
to appear in $S$. For a function symbol $f$ the expression
$f:s_{1}\times\dots\times s_{n}\to s_{n+1}$ with $s_{1},\dots,s_{n+1}\in S$
indicates that $f$ takes arguments of sorts $s_{1}$, …, $s_{n}$ to a value of
sort $s_{n+1}$. Similarly, for a predicate symbol $P$ the expression of the
form $P:s_{1}\times\dots\times s_{n}\to o$ indicates that $P$ is a predicate
with arguments of sorts $s_{1}$, …, $s_{n}$. Terms of $\mathcal{L}$ are
constructed as usual from the variable symbols and function symbols according
to their respective types. Each thus constructed term $t$ has a uniquely
determined sort $s$ and, therefore, we call $t$ an $s$-term. Formulas of
$\mathcal{L}$ are constructed from terms, predicate symbols, the connectives
$\top$, $\bot$, $\wedge$, $\neg$, $\vee$, $\rightarrow$ and the quantifiers
$({\forall}{x:s}){}$, $({\exists}{x:s}){}$ for $s\in S$ and
$x\in\mathfrak{V}_{s}$.

In this article we will make heavy, albeit elementary, use of model theoretic
techniques. Hence, we recall some basic model theoretic concepts and
notations. A first-order structure $M$ for the language $\mathcal{L}$ (over
sorts $S$) is a function that assigns: To each sort $s\in S$ a non-empty set
${M}({s})$; To each function symbol $f:s_{1}\times\dots\times s_{n}\to
s_{n+1}$ a function $f^{M}:\bigtimes_{i=1}^{n}{M}({s_{i}})\to{M}({s_{n+1}})$;
To each predicate symbol $P:s_{1}\times\dots\times s_{n}\to o$ a set
$P^{M}\subseteq\bigtimes_{i=1}^{n}{M}({s_{i}})$. A variable assignment
$\sigma$ is a function that assigns to each variable symbol $v:s$ with $s\in
S$ an element of ${M}({s})$. We write $M,\sigma\models\varphi$ if the formula
$\varphi$ is true in $M$ under the variable assignment $\sigma$. Let
$\varphi(x_{1}:s_{1},\dots,x_{n}:s_{n},\vec{y})$ be a formula and
$d_{i}\in{M}({s_{i}})$ for $i=1,\dots,n$, then we write $M,\\{x_{i}\mapsto
d_{i}\mid i=1,\dots,n\\}\models\varphi$ (or
$M\models\varphi(d_{1},\dots,d_{n},\vec{y})$) if $M,\sigma\models\varphi$, for
all variable assignments $\sigma$ with $\sigma(x_{i})=d_{i}$ for
$i=1,\dots,n$. Thus, in particular, $M\models\varphi$ if
$M,\sigma\models\varphi$ for all variable assignments $\sigma$. Let
$t(x_{1}:s_{1},\dots,x_{n}:s_{n})$ be a term and $d_{1},\dots,d_{n}$ a finite
sequence in ${M}({s_{1}})\times\cdots\times{M}({s_{n}})$, then we write
$t^{M}(\vec{d})$ to denote the element $b$ of $M$ such that $M,\\{x_{i}\mapsto
d_{i}\mid i=1,\dots,n\\}\models t=b$.

In the arguments given in Sections 3 and 4 it is often necessary to consider
terms and formulas of a language $\mathcal{L}$ under some partial variable
assignment over an $\mathcal{L}$ structure $M$. In order to simplify the
notation, we let $\mathcal{L}(M)$ denote the language $\mathcal{L}$ extended
by a fresh function symbol $c_{d}:s$ for each element $d\in{M}({s})$ and sort
$s\in S$. Moreover, we let the structure $M$ interpret the language
$\mathcal{L}(M)$ by letting $M$ interpret $c_{d}$ as the object $d$.

In this article we define a theory $T$ to be a set of sentences, which we call
the axioms of $T$. Let $\varphi$ be formula, then we write $T\vdash\varphi$ if
$\varphi$ is provable in (many-sorted) first-order logic from the axioms of
$T$. Let $T_{1},T_{2}$ be theories, then $T_{1}+T_{2}$ denotes the theory
axiomatized by the set of sentences $T_{1}\cup T_{2}$.

Finally, let us define some notation for some particular sets of formulas. By
$\mathrm{Open}(\mathcal{L})$ we denote the set of quantifier-free formulas of
the language $\mathcal{L}$. Let $\Phi$ be a set of formulas, then we write
$\forall_{1}(\Phi)$ ($\exists_{1}(\Phi)$) for the set of formulas in $\Phi$ of
the form $({\forall}{\vec{x}}){\varphi}$ ($({\exists}{\vec{x}}){\varphi}$)
where $\varphi$ is a quantifier-free formula and $\vec{x}$ is a possibly empty
sequence of variables. We also write $\forall_{1}(\mathcal{L})$ for the
formulas of the above form in the language $\mathcal{L}$.

###  2.2 Induction and lists

In this section we introduce the basic construction of finite Lisp-like lists
that we work with in this article. We also recall the traditional induction
schema for lists and its related terminology. Throughout the article we will
consider various forms of induction that will be defined when needed. We use
the traditional induction schema as defined in this section as a reference in
the sense that we justify the other induction schemata in terms of the
traditional one.

Now we will define the basic language of finite Lisp-like lists and the
corresponding induction schema.

######  Definition 2.1.

The language $\mathcal{L}_{0}$ consists of the sort $\mathsf{i}$ of elements
and the sort $\mathsf{list}$ of finite lists. Moreover, the language
$\mathcal{L}_{0}$ contains the function symbols $\mathit{nil}:\mathsf{list}$
and $\mathit{cons}:\mathsf{i}\times\mathsf{list}\to\mathsf{list}$.

Informally, the symbol $\mathit{nil}$ denotes the empty list and
$\mathit{cons}$ denotes the operation that adds a given element to the front
of a given list. For the sake of legibility we will use upper case letters
$X$, $Y$, $Z$ and variants thereof to denote variables that range over the
sort $\mathsf{list}$. For these variables we omit the the sort annotation,
that is, the “: $\mathsf{list}$” part.

The traditional induction schema for Lisp-like lists is analogous to the one
for natural numbers with the exception that the induction step also quantifies
over elements.

######  Definition 2.2.

Let $\varphi(X,\vec{z})$ be a formula, then the formula $I_{X}{\varphi}$ is
given by

$\left(\varphi(\mathit{nil},\vec{z})\wedge({\forall}{X}){({\forall}{x}){\left(\varphi(X,\vec{z})\rightarrow\varphi(\mathit{cons}(x,X),\vec{z}))\right)}}\right)\rightarrow({\forall}{X}){\varphi(X,\vec{z})}.$

For a set of formulas $\Phi$, the theory ${\Phi}\text{-}\mathrm{IND}$ is
axiomatized by the universal closure of the formulas $I_{X}{\varphi}$, where
$\varphi(X,\vec{z})\in\Phi$.

The induction schema given above is parameterized by the set of possible
induction formulas. This permits to consider various theories by varying the
structure of the induction formulas.

We will also refer to the above induction principle as one-step induction,
since the induction step proceeds by a step of size one. In Section 3 we will
introduce the big-step induction principle that proceeds in larger steps.

When we work with theories of lists we usually work over the following base
theory that provides the disjointness and the injectivity of the list
constructors $\mathit{nil}$ and $\mathit{cons}$.

######  Definition 2.3.

The theory $T_{0}$ is axiomatized by the following axioms

$\displaystyle\mathit{nil}\neq\mathit{cons}(x,X),$ (L0.1)
$\displaystyle\mathit{cons}(x,X)=\mathit{cons}(y,Y)\rightarrow x=y\wedge X=Y.$
(L0.2)

###  2.3 Transfinite sequences

In this section we introduce some notations and definitions related to
transfinite sequences, that is, sequences indexed by ordinals. Later on in
Sections 3 and 4, we will heavily rely on transfinite sequences, of length up
to $\omega^{3}$, for the construction of non-standard models of induction over
lists.

Let $\mathcal{X}$ be a set and $\alpha$ be an ordinal number, then as usual
$\mathcal{X}^{\alpha}$ denotes the set $\\{f:\alpha\to\mathcal{X}\\}$ of
sequences of elements of $\mathcal{X}$ with length $\alpha$. By
$\mathcal{X}^{<\alpha}$ ($\mathcal{X}^{\leq\alpha}$) we denote the set
$\bigcup_{\beta<\alpha}\mathcal{X}^{\beta}$
($\bigcup_{\beta\leq\alpha}\mathcal{X}^{\beta}$). In particular, we denote by
$\mathcal{X}^{*}$ the set
$\mathcal{X}^{<\omega}=\bigcup_{i\in\mathbb{N}}\mathcal{X}^{i}$ of all finite
sequences of elements of $\mathcal{X}$. Let $a\in\mathcal{X}^{\leq\alpha}$,
then $|a|$ denotes the ordinal $\beta\leq\alpha$ such that
$a\in\mathcal{X}^{\beta}$. The empty sequence $()$ ($=\varnothing$) is also
denoted by $\varepsilon$ and $(x)$ denotes the one element sequence
$\\{0\mapsto x\\}$.

In the following we define concatenation of ordinal indexed sequences. The
definition as given below relies on the well-definedness of ordinal
subtraction of an ordinal $\beta$ from an ordinal $\alpha$ when
$\alpha\geq\beta$ (see [28, Theorem 8.8]).

######  Definition 2.4.

Let $\mathcal{X}$ be a set, $\alpha,\beta$ ordinals,
$a\in\mathcal{X}^{\alpha}$, and $b\in\mathcal{X}^{\beta}$, then the sequence
$a\frown b\in\mathcal{X}^{\alpha+\beta}$ is defined by

$\displaystyle(a\frown b)_{\gamma}\coloneqq\begin{cases}a_{\gamma}&\text{if
$\gamma<\alpha$}\\\ b_{\delta}&\text{otherwise}\end{cases},$

where $\gamma<\alpha+\beta$ and $\delta$ is the unique ordinal such that
$\alpha+\delta=\gamma$.

Observe that the definition of concatenation of ordinal indexed sequences
given above generalizes the concatenation of finite sequences, since

$\displaystyle(a_{0},\dots,a_{n-1})\frown(b_{0},\dots,b_{m-1})=(a_{0},\dots,a_{n-1},b_{0},\dots,b_{m-1}).$

The concatenation of ordinal indexed sequences as defined above has some
interesting properties.

######  Lemma 2.5.

Let $\mathcal{X}$ be a set, $\alpha,\beta,\gamma$ ordinals,
$a\in\mathcal{X}^{\alpha}$, $b\in\mathcal{X}^{\beta}$,
$c\in\mathcal{X}^{\gamma}$, then we have:

  1. (i)

associativity: $a\frown(b\frown c)=(a\frown b)\frown c$;

  2. (ii)

left cancellation: If $a\frown b=a\frown c$, then $b=c$.

###### Proof.

For (i) let $\mu<\alpha+\beta+\delta$. By the associativity of ordinal
addition we have $a\frown(b\frown c),(a\frown b)\frown
c\in\mathcal{X}^{\alpha+\beta+\gamma}$. Now we have to consider three cases.
If $\mu<\alpha$, then $\mu<\alpha+\beta$. Hence

$(a\frown(b\frown c))_{\mu}=a_{\mu}=(a\frown b)_{\mu}=((a\frown b)\frown
c)_{\mu}.$

If $\alpha\leq\mu<\alpha+\beta$, then there is a unique ordinal $\delta$ such
that $\alpha+\delta=\mu$. Moreover, by the monotonicity properties of ordinal
addition we have $\delta<\beta$. Hence

$(a\frown(b\frown c))_{\mu}=(b\frown c)_{\delta}=b_{\delta}=(a\frown
b)_{\mu}=((a\frown b)\frown c)_{\mu}.$

Finally, if $\alpha+\beta\leq\mu<\alpha+\beta+\gamma$, then there are unique
$\delta_{1}$ and $\delta_{2}$ such that $\alpha+\delta_{1}=\mu$ and
$\alpha+\beta+\delta_{2}=\mu$. Furthermore, we have $\delta_{1}\geq\beta$,
hence there is $\delta_{3}$ such that $\beta+\delta_{3}=\delta_{1}$. Thus
$\mu=\alpha+\delta_{1}=\alpha+\beta+\delta_{3}=\alpha+\beta+\delta_{2}$, hence
$\delta_{2}=\delta_{3}$. Therefore

$(a\frown(b\frown c))_{\mu}=(b\frown
c)_{\beta+\delta_{3}}=c_{\delta_{3}}=c_{\delta_{2}}=((a\frown b)\frown
c)_{\mu}.$

For (ii) observe that since $a\frown b\in\mathcal{X}^{\alpha+\beta}$, $a\frown
c\in\mathcal{X}^{\alpha+\gamma}$ we have $\alpha+\beta=\alpha+\gamma$ and
therefore by the left cancellation of ordinal addition $\beta=\gamma$. Now let
$\delta<\beta$, then we have $(a\frown
b)_{\alpha+\delta}=b_{\delta}=c_{\delta}=(a\frown c)_{\alpha+\delta}$. Hence,
$b=c$. ∎

Observe, however, that since already ordinal addition does not have right
cancellation, the concatenation of ordinal indexed sequences does clearly also
not have right cancellation.

For sequences we will often be interested in suffixes. In the following
definition we introduce some notation for accessing the suffix of a sequence.

######  Definition 2.6 (Sequence suffix).

Let $\mathcal{X}$ be a set, $\alpha,\beta$ ordinals with $\beta\leq\alpha$,
and $a\in\mathcal{X}^{\alpha}$, then the sequence $a\uparrow\beta$ is given by

$(a\uparrow\beta)_{\gamma}=a_{\beta+\gamma},$

for $\gamma<\mu$ where $\mu$ is the unique ordinal such that
$\beta+\mu=\alpha$.

Finally, let us give some notation for the sequence obtained by concatenating
sequences of uniform length. This construction will be used in Section 4 and
relies on ordinal division with remainder (see [28, Theorem 8.27]).

######  Definition 2.7.

Let $\mathcal{X}$ be a set, $\alpha,\beta$ ordinals with $\alpha>0$, and
$\mathfrak{a}\in(\mathcal{X}^{\alpha})^{\beta}$. The sequence
$\lfloor\mathfrak{a}\rfloor\in\mathcal{X}^{\alpha\cdot\beta}$ is defined by

$\lfloor\mathfrak{a}\rfloor_{\xi}\coloneqq\mathfrak{a}_{\delta,\mu},$

for $\xi<\alpha\cdot\beta$ where $\mu,\delta$ are the unique ordinals such
that $\xi=(\alpha\cdot\delta)+\mu$ with $\mu<\alpha$. Furthermore, for
$a\in\mathcal{X}^{\alpha}$, we denote by $a^{\beta}$ the sequence
$\lfloor(a)_{\gamma<\beta}\rfloor$ consisting of $\beta$ times the sequence
$a$.

##  3 Big-step induction

Big-step induction is a generalization of the induction principle of
Definition 2.2 in which the induction step proceeds by adding more than one
element. Big-step induction and other induction principles are often used in
automated inductive theorem provers [4]. Some formulas can be proved more
naturally by a special induction principle. Hence a special induction
principle may allow a prover to find a proof faster under the constraints of
its proof search algorithm or even enable the prover to prove the formula in
the first place [31]. It is therefore interesting to investigate the relation
between the one-step induction principle and special induction principles
implemented in AITP systems.

In this section we show the first main result of this article, namely that,
for all $m\geq 1$, quantifier-free $(m+1)$-step induction for lists does not
follow from quantifier-free $m$-step induction. In particular, quantifier-free
big-step induction for lists cannot be reduced to quantifier-free one-step
induction, which is in contrast to induction on natural numbers where such a
reduction is possible (see for example [31]).

The definition below defines the big-step induction principle for lists
considered in this article. Let us introduce some notation to make it easier
to state big-step induction for lists. Let $t_{1},\dots,t_{n}$ be a possibly
empty list of terms of sort $\mathsf{i}$ and $T$ a term of sort
$\mathsf{list}$, then the term $\mathit{cons}(t_{1},\dots,t_{n};T)$ is defined
inductively by

$\displaystyle\mathit{cons}(;T)=T,$
$\displaystyle\mathit{cons}(t_{1},\dots,t_{n+1};T)=\mathit{cons}(t_{1},\dots,t_{n},\mathit{cons}(t_{n+1},T)).$

######  Definition 3.1.

Let $\varphi(x,\vec{z})$ be a formula and $m\geq 1$, then the formula
$I_{x\curvearrowright m}{\varphi}$ is given by

$\left(\begin{split}&\bigwedge_{i=1,\dots,m}({\forall}{x_{1},\dots,x_{i-1}}){\varphi}(\mathit{cons}(x_{1},\dots,x_{i-1};\mathit{nil}),\vec{z})\\\
&\wedge({\forall}{X}){({\forall}{x_{1},\dots,x_{m}}){\left(\varphi(X,\vec{z})\rightarrow\varphi(\mathit{cons}(x_{1},\dots,x_{m};X),\vec{z})\right)}}\end{split}\right)\rightarrow({\forall}{X}){\varphi(X,\vec{z})}.$

Let $\Phi$ be a set of formulas and $m\geq 1$, then the $m$-step induction
schema ${\Phi}\text{-}\mathrm{IND}_{\curvearrowright{m}}$ over $\Phi$ is
axiomatized by the universal closure of the formulas $I_{x\curvearrowright
m}{\varphi}$ where $\varphi(x,\vec{z})\in\Phi$.

A simple example of formulas that have natural proofs by big-step induction
are the acyclicity formulas given below, which express that adding a finite
number $n\geq 1$ of elements to a list results in a different list:

$X\neq\mathit{cons}(x_{1},\dots,x_{n};X).$

To prove this formula by $n$-step induction it suffices to proceed by
induction on $X$ in the formula itself. For the base case we have to show that
$\mathit{nil}\neq\mathit{cons}(x_{1},\dots,x_{n};\mathit{nil})$, which follows
readily from (L0.1). For the induction step we assume (3). For a contradiction
assume

$\mathit{cons}(x_{1}^{\prime},\dots,x_{n}^{\prime};X)=\mathit{cons}(x_{1},\dots,x_{n},x_{1}^{\prime},\dots,x_{n}^{\prime};X).$

Then by an $n$-fold application of (L0.2) we obtain $x_{i}^{\prime}=x_{i}$ for
$i=1,\dots,n$ and

$X=\mathit{cons}(x_{1}^{\prime},\dots,x_{n}^{\prime};X).$

This contradicts the induction hypothesis and thus completes the induction
step. Interestingly, however, the acyclicity formula (3) also has a slightly
less natural proof using one-step quantifier-free induction.

######  Lemma 3.2.

The theory $T_{0}+{\mathrm{Open}(\mathcal{L}_{0})}\text{-}\mathrm{IND}$ proves

  1. (i)

$X\neq\mathit{cons}(x_{1},\dots,x_{n};X)$ for $n\geq 1$;

  2. (ii)

$X=\mathit{nil}\vee({\exists}{x^{\prime}}){({\exists}{X^{\prime}}){X=\mathit{cons}(x^{\prime},X^{\prime})}}$.

###### Proof.

For (i) we assume $X=\mathit{cons}(x_{1},\dots,x_{n};X)$ and proceed by
induction on $X^{\prime}$ in the formula

$\underbrace{X^{\prime}\neq
X}_{\psi_{1}(X^{\prime})}\wedge\underbrace{X^{\prime}\neq\mathit{cons}(x_{n},X)}_{\psi_{2}(X^{\prime})}\wedge\dots\wedge\underbrace{X^{\prime}\neq\mathit{cons}(x_{2},\dots,x_{n};X)}_{\psi_{n}(X^{\prime})}.$

For the base case we have to show $\psi_{i}(\mathit{nil})$ for $i=1,\dots,n$.
For $i>1$, this follows easily from (L0.1) and for $i=0$ we obtain
$X^{\prime}\neq X$ from the assumption $X=\mathit{cons}(x_{1},\dots,x_{n};X)$
and (L0.1). For the induction step we assume
$\bigwedge_{i=1}^{n}\psi_{i}(X^{\prime})$. Let $i\in\\{1,\dots,n\\}$. If $i=1$
assume $\mathit{cons}(x^{\prime},X^{\prime})=X$, then by the assumption
$X=\mathit{cons}(x_{1},\dots,x_{n};X)$ and $\eqref{ax:thlistbase:2}$ we obtain
$X^{\prime}=\mathit{cons}(x_{2},\dots,x_{n};X)$ which contradicts the
assumption $\psi_{n}(X^{\prime})$. If $i>1$, then assume
$\mathit{cons}(x^{\prime},X^{\prime})=\mathit{cons}(x_{n-i+2},\dots,x_{n};X)$,
then by (L0.2) we obtain $X^{\prime}=\mathit{cons}(x_{n-i+1},\dots,x_{n};X)$,
which contradicts $\psi_{i-1}(X^{\prime})$. Hence, we finally obtain
$({\forall}{X^{\prime}}){\left(\bigwedge_{i=1}^{n}\psi_{i}(X^{\prime})\right)}$.
Thus, in particular, we have
$\bigwedge_{i=1}\psi_{i}(\mathit{cons}(x_{1},\dots,x_{n};X))$. Therefore, we
obtain

$\mathit{cons}(x_{1},\dots,x_{n};X)\neq X,$

which contradicts the first assumption.

For (ii) we proceed by induction on $Y$ in the formula $X\neq Y$. For the base
case we have to show $X\neq\mathit{nil}$. Assume $X=\mathit{nil}$, then we are
done. For the induction step, we assume $X\neq Y$ and $X=\mathit{cons}(y,Y)$
and we are done. Hence we have $({\forall}{Y}){X\neq Y}$. Thus in particular
$X\neq X$, which is a contradiction and thus implies the claim. ∎

This gives rise to the question whether a similar technique as we have used to
prove the acyclicity formulas with quantifier-free induction is also possible
in general. It is straightforward to see that we can simulate big-step
induction with single-step induction by making use of universal quantifiers
and conjunction. For the sake of completeness we recall the argument.

######  Lemma 3.3.

Let $m\geq 1$ and $\varphi(X,\vec{z})$ be a formula, then

$\vdash
I_{X}{\bigwedge_{i=1}^{m}({\forall}{x_{1}}){\dots({\forall}{x_{i-1}}){\varphi(\mathit{cons}(x_{1},\dots,x_{i-1};X),\vec{z})}}}\rightarrow
I_{X\curvearrowright m}{\varphi(X,\vec{z})}.$

###### Proof.

Assume
$({\forall}{x_{1}}){\dots({\forall}{x_{i-1}}){\varphi(\mathit{cons}(x_{1},\dots,x_{i-1};\mathit{nil}),\vec{z})}}$
for $i=1,\dots,m$ and

$({\forall}{X}){({\forall}{x_{1}}){\dots({\forall}{x_{m}}){\left(\varphi(X,\vec{z})\rightarrow\varphi(\mathit{cons}(x_{1},\dots,x_{m};X),\vec{z})\right)}}}.$
($\star$)

Clearly it suffices to show the following formula.

$\bigwedge_{j=1}^{m}({\forall}{x_{1}}){\dots({\forall}{x_{j-1}}){\varphi(\mathit{cons}(x_{1},\dots,x_{j-1};X),\vec{z})}}.$
($\dagger$)

We proceed by induction on $X$ in the formula ($\dagger$ ‣ 3). The base case
follows immediately from the assumptions. For the induction step case we
assume ($\dagger$ ‣ 3). Now let $i\in\\{1,\dots,m\\}$, let
$x^{\prime},x_{1},\dots,x_{i-1}$ be fixed but arbitrary. If $i<m$, then we
have to show
$\varphi(\mathit{cons}(x_{1},\dots,x_{i-1},x^{\prime};X),\vec{z})$, which
follows from the induction hypothesis with $j=i+1$. If $i=m$, then we have to
show $\varphi(\mathit{cons}(x_{1},\dots,x_{m-1},x^{\prime};X),\vec{z})$. By
($\dagger$ ‣ 3) with $j=1$, we have $\varphi(X,\vec{z})$, hence by ($\star$ ‣
3) we obtain the desired formula. ∎

######  Remark 3.4.

When the domain of the elements provably consists of a finite number of
elements $n\geq 1$, then the quantifiers over elements in the induction
formula of Lemma 3.3 can be replaced by a conjunction. Hence, in this
situation $(m+1)$-step induction reduces to $m$-step induction without an
increase in quantifier-complexity of the induction formulas.

However, as we will show, the increase of the quantifier complexity when
simulating big-step induction with one-step induction is in general
unavoidable. The remainder of the section is devoted to the proof of the
following proposition.

######  Definition 3.5.

The language $\mathcal{L}_{A}$ extends the base language of lists
$\mathcal{L}_{0}$ by the predicate symbol $A:\mathsf{list}\to o$.

######  Proposition 3.6.

Let $m\geq 2$, then

$T_{0}+\bigcup_{1\leq
j<m}{\mathrm{Open}(\mathcal{L}_{A})}\text{-}\mathrm{IND}_{\curvearrowright{j}}\not\vdash
I_{x\curvearrowright m}{A(x)}.$

This proposition entails, in particular, that
$T_{0}+{\mathrm{Open}(\mathcal{L}_{A})}\text{-}\mathrm{IND}\not\vdash{\mathrm{Open}(\mathcal{L}_{A})}\text{-}\mathrm{IND}_{\curvearrowright
2}$. We will show the above claim by constructing a model of quantifier-free
induction over the language $\mathcal{L}_{A}$ in which the predicate $A$ does
not satisfy two-step induction. In such a model we call an element a standard
element if it can be expressed as a term of the form
$\mathit{cons}(x_{1},\dots\mathit{cons}(x_{n},\mathit{nil}))$ under a suitable
variable assignment. All other elements are called the non-standard elements.
By Lemma 3.2.(ii) a non-standard element can be decomposed any finite number
of times and thus resemble transfinite sequences of length at least $\omega$.
The model constructed in Definition 3.8 will use transfinite sequences of
length up to $\omega$ as the non-standard elements. Since for example the
transfinite sequence $v^{\omega}$ with $v\in\mathbb{N}^{*}$ satisfies
$v^{\omega}=v\frown v^{\omega}$ it violates the acyclicity property
$X\neq\mathit{cons}(x_{1},\dots,x_{|v|},X)$ (see Lemma 3.2). Hence we have to
avoid sequences that absorb a finite prefix.

The following definition introduces the non-standard elements that we use for
the model constructed in this section.

######  Definition 3.7.

Let $k\in\mathbb{N}$, then by $N_{k}$ we denote the sequence $(i)_{k\leq
i<\omega}$. Now we define

$\mathcal{N}\coloneqq\\{w\frown N_{k}\mid
w\in\mathbb{N}^{*},k\in\mathbb{N}\\}.$

Let $N\in\mathcal{N}$, then there is a unique decomposition $N=w\frown N_{k}$
such that $|w|$ and $k$ are minimal. We write $w_{N}$ for this $w$ and $k_{N}$
for this $k$. We call $w_{N}$ the main prefix of $N$ and $N_{k_{N}}$ the main
suffix of $N$.

We can now define a structure whose domain consists of the finite sequences of
natural numbers and the non-standard elements defined above.

######  Definition 3.8.

Let $m\geq 1$, then the structure $M_{1}^{m}$ interprets the sort $\mathsf{i}$
as the natural numbers and the sort $\mathsf{list}$ as
$M_{1}^{m}(\mathsf{list})=\mathbb{N}^{*}\cup\mathcal{N}$. Furthermore,
$M_{1}^{m}$ interprets the non-logical symbols as follows

$\displaystyle\mathit{nil}^{M_{1}^{m}}\coloneqq\varepsilon,$
$\displaystyle\mathit{cons}^{M_{1}^{m}}(n,l)\coloneqq(n)\frown l,$
$\displaystyle
A^{M_{1}^{m}}\coloneqq\mathbb{N}^{*}\cup\left\\{N\in\mathcal{N}\mid\text{$w_{N}\neq\varepsilon$
or $m\nmid k_{N}$}\right\\}.$

We say that an element $l_{1}$ is a predecessor of an element $l_{2}$ if there
are $k,n_{1},\dots,n_{k}\in\mathbb{N}$ such that $M_{1}^{m}\models
l_{2}=\mathit{cons}(n_{1},\dots,n_{k};l_{1})$.

We start by observing that the structure defined above satisfies the basic
axioms of the constructors $\mathit{nil}$ and $\mathit{cons}$ of finite
sequences.

######  Lemma 3.9.

Let $m\geq 1$, then $M_{1}^{m}\models T_{0}$.

###### Proof.

We start with the axiom (L0.1). We have
$\mathit{nil}^{M_{1}^{m}}=\varepsilon=\varnothing$. Let $n\in\mathbb{N}$ and
$l\in M_{1}^{m}(\mathsf{list})$, then $(0,n)\in(n)\frown
l=\mathit{cons}^{M_{1}^{m}}(n,l)$. Hence,
$\mathit{nil}^{M_{1}^{m}}\neq\mathit{cons}^{M_{1}^{m}}(n,l)$ and therefore
$M_{1}^{m}\models\eqref{ax:thlistbase:1}$. Now let $n_{1},n_{2}\in\mathbb{N}$
and $l_{1},l_{2}\in M_{1}^{m}(\mathsf{list})$ and assume that
$\mathit{cons}^{M_{1}^{m}}(n_{1},l_{1})=(n_{1})\frown l_{1}=(n_{2})\frown
l_{2}$. Clearly, $n_{1}=n_{2}$, hence by Lemma 2.5 we immediately obtain
$M_{1}^{m}\models\eqref{ax:thlistbase:2}$. ∎

The following lemma shows that unary $A$ predicates of $M_{1}^{m}$, eventually
periodically become true on predecessors of non-standard elements.

######  Lemma 3.10.

Let $m\geq 1$, $t(X)$ be a $\mathcal{L}_{A}(M_{1}^{m})$ term, then there is a
$K\in\mathbb{N}$ such that for all $k\in\mathbb{N}$ with $k\geq K$ and $m\nmid
k$, $M_{1}^{m}\models A(t(N_{k})).$

###### Proof.

There clearly is a $w\in\mathbb{N}^{*}$ such that $M_{1}^{m}\models
t(l)=w\frown l$ for all $l\in M_{1}^{m}(\mathsf{list})$. If $w=\varepsilon$,
then we are done by letting $K=0$. Otherwise, we let $K=(w)_{|w|-1}+2$. For
$k\geq K$, the sequence $N_{k}$ is the main suffix of the sequence $w\frown
N_{k}$ and the main prefix of $w\frown N_{k}$ is not empty. Thus
$M_{1}^{m}\models A(t(N_{k}))$. ∎

Informally, the following lemma states that unary equational predicates over
elements of $M_{1}^{m}$ eventually stabilize.

######  Lemma 3.11.

Let $m\geq 1$ and $E(X)$ an $\mathcal{L}_{A}(M_{1}^{m})$ equation. If
$M_{1}^{m}\not\models E(X)$ then there exists $K\in\mathbb{N}$ such that
firstly $M_{1}^{m}\not\models E(w)$ for all $w\in\mathbb{N}^{*}$ with $|w|\geq
K$ and secondly $M_{1}^{m}\not\models E(N_{k})$ for all $k\geq K$.

###### Proof.

The case where $X\notin\mathit{Var}(E)$ is trivial. Let $E(X)$ be $u(X)=v(X)$.
If $X\in\mathit{Var}(u)$ and $\mathit{Var}(v)=\varnothing$, then there is
$w\in\mathbb{N}^{*}$ and $l^{\prime}\in M_{1}^{m}(\mathsf{list})$ such that
$M_{1}^{m}\models u(l)=w\frown l$ for all $l\in M_{1}^{m}(\mathsf{list})$ and
$M_{1}^{m}\models v=l^{\prime}$. If $|w|>|l^{\prime}|$, then we are done by
letting $K=0$. Otherwise, if $|w|\leq|l^{\prime}|$ we consider the prefix of
$l^{\prime}$. If $w$ is not a prefix of $l^{\prime}$, then again we are done
by letting $K=0$. If $w$ is the prefix of $l^{\prime}$, then
$l^{\prime}=w\frown l^{\prime\prime}$ for some
$l^{\prime\prime}\in\mathbb{N}^{\leq|l^{\prime}|}$. We have
$l^{\prime\prime}\in M_{1}^{m}(\mathsf{list})$, since
$M_{1}^{m}(\mathsf{list})$ is closed under predecessors. Thus
$M_{1}^{m}\models E(l)$ if and only if $l=l^{\prime\prime}$. If
$l^{\prime\prime}$ is a standard element, then $M_{1}^{m}\not\models E(l)$ for
all $l\in M_{1}^{m}(\mathsf{list})$ with $|l|>|l^{\prime\prime}|$. Hence, we
let $K=|l^{\prime\prime}|+1$. Otherwise, if $l^{\prime\prime}$ is non-
standard, then we readily have $M_{1}^{m}\not\models E(l)$ for all
$l\in\mathbb{N}^{*}$. Furthermore, we have $M_{1}^{m}\not\models E(l)$ for all
non-standard $l\in M_{1}^{m}(\mathsf{list})$ with
$(l)_{0}\neq(l^{\prime\prime})_{0}$. Hence, it suffices to let
$K=(l^{\prime\prime})_{0}+1$.

Now let us consider the case where
$\mathit{Var}(u)\cap\mathit{Var}(v)=\\{X\\}$. There exist
$w,w^{\prime}\in\mathbb{N}^{*}$ such that for all $l\in
M_{1}^{m}(\mathsf{list})$, $M_{1}^{m}\models u(l)=w\frown l$ and
$M_{1}^{m}\models v(l)=w^{\prime}\frown l$. Moreover, by the assumption that
$M_{1}^{m}\not\models E(X)$ we have $w\neq w^{\prime}$. Hence,
$M_{1}^{m}\not\models E(l)$ for all $l\in M_{1}^{m}(\mathsf{list})$. Thus, we
let $K=0$. ∎

We are now ready to show that the structure $M_{1}^{m}$ satisfies quantifier-
free $j$-step induction for $1\leq j<m$ over the language consisting of the
list constructors $\mathit{nil}$, $\mathit{cons}$, and the predicate symbol
$A$.

######  Lemma 3.12.

Let $m\geq 2$, then $M_{1}^{m}\models\bigcup_{1\leq
j<m}{\mathrm{Open}(\mathcal{L}_{A})}\text{-}\mathrm{IND}_{\curvearrowright{j}}$.

###### Proof.

Let $j\in\mathbb{N}$ with $1\leq j<m$ and $\varphi(X)$ be a quantifier-free
$\mathcal{L}_{A}(M_{1}^{m})$ formula. Assume that

$\displaystyle
M_{1}^{m}\models\varphi(\mathit{cons}(x_{1},\dots,x_{i-1};\mathit{nil})),$
($\ast$)

for $i=1,\dots,j$ and

$\displaystyle
M_{1}^{m}\models\varphi(X)\rightarrow\varphi(\mathit{cons}(x_{1},\dots,x_{j};X)),$
($\star$)

Let $l\in M_{1}^{m}(\mathsf{list})$. We have to show that
$M_{1}^{m}\models\varphi(l)$. If $l$ is standard, then we are done by a
straightforward induction on $|l|$ making use of ($\ast$ ‣ 4) and ($\star$ ‣
4).

Now let us consider the case where $l$ is non-standard, that is,
$l\in\mathcal{N}$. Let $E_{1}(X),\dots,E_{n}(X)$ be all the list equations of
$\varphi$ with $M_{1}^{m}\not\models E_{i}(X)$ for $i=1,\dots,n$. Then by
Lemma 3.11 there exists $K\in\mathbb{N}$ such that $M_{1}^{m}\not\models
E_{i}(w)$ for all $w\in\mathbb{N}^{*}$ with $|w|\geq K$ and
$M_{1}^{m}\not\models E_{i}(N_{k})$ for all $k\geq K$.

Now let $A(t_{1}(X))$, …, $A(t_{p}(X))$ be all the $A$ atoms of $\varphi$. By
Lemma 3.10, there exists $K^{\prime}\geq K$ such that for all $k\in\mathbb{N}$
with $k\geq K^{\prime}$ and $m\nmid k$, we have $M\models A(t_{q}(N_{k}))$ for
$q=1,\dots,p$. Hence, by taking a sufficiently long prefix $w$ of $l$
($|w|\geq j$), we obtain $K^{\prime\prime}\geq K^{\prime}$ such that
$l=w\frown N_{K^{\prime\prime}}$ and $m\mid K^{\prime\prime}-1$. Since $m\mid
K^{\prime\prime}-1$ and $j<m$, we have $m\nmid K^{\prime\prime}+i$ for
$i=0,\dots,j-1$. Thus, $M_{1}^{m}\models A(t_{q}(l\uparrow|w|-i))$ for
$q=1,\dots,p$ and $i=0,\dots,j-1$.

Let $\psi(X)$ be any atom of $\varphi(X)$ and $w^{\prime}\in\mathbb{N}^{*}$
with $|w^{\prime}|\geq K$, then by the above, for $i=0,\dots,j-1$, we have
$M_{1}^{m}\models\psi(w^{\prime})$ if and only if
$M_{1}^{m}\models\psi(l\uparrow|w|-i)$. Hence,
$M_{1}^{m}\models\varphi(l\uparrow|w|-i)\leftrightarrow\varphi(w^{\prime})$.
In the first part of the proof we have already shown that
$M_{1}^{m}\models\varphi(w^{\prime})$. Hence, we have
$M_{1}^{m}\models\varphi(l\uparrow|w|-i)$.

Therefore, by a straightforward induction starting with
$M_{1}^{m}\models\varphi(l\uparrow|w|-i)$ for $i=0,\dots,j-1$ and by making
use of ($\star$ ‣ 4) we obtain
$M_{1}^{m}\models\varphi(w^{\prime}\frown(l\uparrow|w|))$ for all
$w^{\prime}\in\mathbb{N}^{*}$. In particular, we have
$M_{1}^{m}\models\varphi(l)$. ∎

######  Lemma 3.13.

Let $m\geq 2$, then $M_{1}^{m}\not\models I_{x\curvearrowright m}{A(x)}$.

###### Proof.

We have $M_{1}^{m}\models A(w)$ for all $w\in\mathbb{N}^{*}$, hence in
particular

$M_{1}^{m}\models A(\mathit{cons}(x_{1},\dots,x_{j-1};\mathit{nil}))$ for
$j=1,\dots,m$.

Now we consider the induction step. Let $l\in M_{1}^{m}(\mathsf{list})$ and
$n_{1},\dots,n_{m}\in\mathbb{N}$. If $l\in\mathbb{N}^{*}$, then by the above
we have

$(\mathit{cons}(n_{1},\dots,n_{m};l))^{M_{1}^{m}}\in\mathbb{N}^{*}\subseteq
A^{M_{1}^{m}}.$

Hence, $M_{1}^{m}\models A(X)\rightarrow
A(\mathit{cons}(n_{1},\dots,n_{m};l))$. For $l\in\mathcal{N}$ we show the
contrapositive of the induction step. Suppose first that
$(n_{1},\dots,n_{m})\frown l\notin A^{M_{1}^{m}}$. Hence, we have
$(n_{1},\dots,n_{k})\frown l=N_{k}$ for some $k\in\mathbb{N}$ and $m\mid k$.
Thus, $l=N_{k+m}$ that is $l\notin A^{M_{1}^{m}}$. Hence, $M_{1}^{m}\models
A(x)\rightarrow A(\mathit{cons}(x_{1},\dots,x_{m};X))$. However, we also have
$N_{0}\not\in A^{M_{1}^{m}}$. Hence, $M_{1}^{m}\not\models
I_{x\curvearrowright m}{A(x)}$. ∎

###### Proof of Proposition 3.6.

An immediate consequence of Lemmas 3.9 and 3.12, and Lemma 3.13. ∎

So far we have shown that simulating quantifier-free $m+1$-step induction over
lists with $m$-step induction, is not possible when induction formulas are
quantifier-free. The simulation of big-step induction in Lemma 3.3 by one-step
induction makes use of universal quantifiers and conjunction. This gives rise
to the question whether the use of conjunction is necessary. We conjecture
that it is necessary in the following sense. By $\mathrm{Clause}(\mathcal{L})$
we denote the set of all clauses (disjunctions of atoms and their negation)
over the language $\mathcal{L}$.

######  Conjecture 3.14.

Let $m\geq 2$, then

$T_{0}+\bigcup_{1\leq
j<m}{\forall_{1}\mathrm{Clause}(\mathcal{L}_{A})}\text{-}\mathrm{IND}_{\curvearrowright{j}}\not\vdash
I_{x\curvearrowright m}{A(x)}.$

This conjecture is particularly interesting for the methods presented in [26,
15, 16]. As shown in [19, 31] these methods carry out induction on literals
and clauses. However, the results in [19, 31] are formulated for induction
over natural numbers and need to be adapted to the case for induction over
lists and other recursive datatypes. A positive answer to the conjecture above
together with analogues of the results [19, 31] would provide a formal
justification for the necessity to implement more powerful induction rules
that handle conjunction and quantification such as described in [16]. As a
byproduct, the formulas $I_{X\curvearrowright m}{A(X)}$ with $m\geq 1$ form a
set of benchmark problems of increasing difficulty for automated theorem
provers.

The above shows that mechanizing induction on lists is more complicated than
induction on natural numbers in the sense that a reduction of big-step
induction to one-step induction requires induction formulas with a higher
quantifier-complexity. In the following we will consider lists with a
concatenation operation and we will show that big-step induction does not
prove the right cancellation of concatenation.

##  4 Right cancellation of list concatenation

In the previous section we have shown that quantifier-free $(m+1)$-big step
induction is strictly stronger than quantifier-free $m$-step induction, but
not stronger than $\forall_{1}$ induction. In this section we show that big-
step quantifier-free induction is in general strictly weaker than
$\forall_{1}$ induction. We will prove this result by showing that the right
cancellation property of the append operation on lists can not be proved with
quantifier-free big-step induction on lists. This result is of particular
interest for the automation of proof by mathematical induction, since it
implies the necessity to work with induction rules that exceed the power
quantifier-free big-step induction to handle comparatively basic properties
such as the right cancellation of list concatenation.

In the following we will work with a language that extends the base language
of lists $\mathcal{L}_{0}$ by an infix symbol for the concatenation of lists.
We will work with the usual left-recursive definition of concatenation.

######  Definition 4.1.

The infix function symbol
$\cdot\frown\cdot:\mathsf{list}\times\mathsf{list}\to\mathsf{list}$ represents
the append operation on lists. We define the language $\mathcal{L}_{1}$ to be
$\mathcal{L}_{0}\cup\\{\frown\\}$. The theory $T_{1}$ extends the base theory
of lists $T_{0}$ by the following axioms

$\displaystyle\mathit{nil}\frown Y=Y,$ (L1.1)
$\displaystyle\mathit{cons}(x,X)\frown Y=\mathit{cons}(x,X\frown Y).$ (L1.2)

In the following lemmas we prove several properties about lists, and in
particular the concatenation operation, using increasingly powerful induction
principles. We start by proving some simple properties with quantifier-free
induction.

######  Lemma 4.2.

The theory $T_{1}+{\mathrm{Open}(\mathcal{L}_{1})}\text{-}\mathrm{IND}$ proves
the following formulas

  1. (i)

$X\frown\mathit{nil}=X$,

  2. (ii)

$X\frown(Y\frown Z)=(X\frown Y)\frown Z$.

###### Proof.

For both formulas we use a straightforward induction on $X$ and making use of
(L1.1), (L1.2). ∎

We prove the next property, the right cancellation for single-element lists,
using simultaneous induction on two variables.

######  Definition 4.3.

Let $\varphi(X,Y,\vec{z})$ be a formula, then the formula $I_{X,Y}{\varphi}$
is given by

$\left(\begin{split}&({\forall}{X}){\varphi(X,\mathit{nil},\vec{z})}\wedge({\forall}{Y}){\varphi(\mathit{nil},Y,\vec{z})}\\\
&\wedge({\forall}{X}){({\forall}{Y}){({\forall}{x}){({\forall}{y}){\left(\varphi(X,Y,\vec{z})\rightarrow\varphi(\mathit{cons}(x,X),\mathit{cons}(y,Y),\vec{z})\right)}}}}\end{split}\right)\\\
\rightarrow({\forall}{X}){({\forall}{Y}){\varphi(X,Y,\vec{z})}}.$

Let $\Gamma$ be a set of formulas, then the theory
${\Gamma}\text{-}\mathrm{DIND}$ is axiomatized by the sentences
$({\forall}{\vec{z}}){I_{X,Y}{\varphi(X,Y,\vec{z})}}$ with
$\varphi(X,Y,\vec{z})\in\Gamma$.

######  Lemma 4.4.

$T_{1}+{\mathrm{Open}(\mathcal{L}_{1})}\text{-}\mathrm{DIND}$ proves

$Y\frown\mathit{cons}(x,\mathit{nil})=Z\frown\mathit{cons}(x,\mathit{nil})\rightarrow
Y=Z.$

###### Proof.

We proceed by induction on $Y$ and $Z$ simultaneously. We consider only one of
the two base cases, since the other one is symmetric. For the base case
$Y=\mathit{nil}$ we assume
$\mathit{nil}\frown\mathit{cons}(x,\mathit{nil})=Z\frown\mathit{cons}(x,\mathit{nil})$
and we have to show that $Z=\mathit{nil}$. First of all, by (L1.1) we obtain
$\mathit{cons}(x,\mathit{nil})=Z\frown\mathit{cons}(x,\mathit{nil})$. By Lemma
3.2 we can consider two cases. If $Z=\mathit{nil}$, then we are done.
Otherwise, there are $z^{\prime}$ and $Z^{\prime}$ such that
$Z=\mathit{cons}(z^{\prime},Z^{\prime})$. Thus

$\displaystyle\mathit{cons}(x,\mathit{nil})$
$\displaystyle=\mathit{cons}(z^{\prime},Z^{\prime})\frown\mathit{cons}(x,\mathit{nil})$
$\displaystyle=_{\eqref{ax:thlistappend:2}}\mathit{cons}(z^{\prime},Z^{\prime}\frown\mathit{cons}(x,\mathit{nil})).$

Therefore, by (L0.2) we have in particular
$\mathit{nil}=Z^{\prime}\frown\mathit{cons}(x,\mathit{nil})$. We apply Lemma
3.2 and consider two cases. If $Z^{\prime}=\mathit{nil}$, then
$\mathit{nil}=\mathit{nil}\frown\mathit{cons}(x,\mathit{nil})=\mathit{cons}(x,\mathit{nil})$,
which contradicts (L0.1). Otherwise, there are $z^{\prime\prime}$ and
$Z^{\prime\prime}$ such that
$Z^{\prime}=\mathit{cons}(z^{\prime\prime},Z^{\prime\prime})$, then, by
(L1.2),
$\mathit{nil}=\mathit{cons}(z^{\prime\prime},Z^{\prime\prime}\frown\mathit{cons}(x,\mathit{nil}))$,
which contradicts (L0.1). For the induction step assume
$Y\frown\mathit{cons}(x,\mathit{nil})=Z\frown\mathit{cons}(x,\mathit{nil})\rightarrow
Y=Z$ and
$\mathit{cons}(y,Y)\frown\mathit{cons}(x,\mathit{nil})=\mathit{cons}(z,Z)\frown\mathit{cons}(x,\mathit{nil})$.
Then by (L1.2) and (L0.2) we obtain $y=z$ and

$Y\frown\mathit{cons}(x,\mathit{nil})=Z\frown\mathit{cons}(x,\mathit{nil}).$

By the induction hypothesis we obtain $Y=Z$, thus,
$\mathit{cons}(y,Y)=\mathit{cons}(z,Z)$. ∎

Observe that double induction is contained within induction on $\forall_{1}$
formulas when working modulo case analysis $\mathrm{CA}$ given by

$({\forall}{X}){\left(X=\mathit{nil}\vee({\exists}{X^{\prime}}){({\exists}{x^{\prime}}){X=\mathit{cons}(x^{\prime},X^{\prime})}}\right)}.$

######  Lemma 4.5.

$\mathrm{CA}+{\forall_{1}(\mathcal{L})}\text{-}\mathrm{IND}\vdash{\mathrm{Open}(\mathcal{L})}\text{-}\mathrm{DIND}$.

###### Proof.

Let $\varphi(X,Y,\vec{z})$ be a quantifier-free $\mathcal{L}$ formula. Let
$X,Y,\vec{z}$ be fixed and assume
$({\forall}{X}){\varphi(X,\mathit{nil},\vec{z})}$,
$({\forall}{Y}){\varphi(\mathit{nil},Y,\vec{z})}$, and

$({\forall}{X}){({\forall}{Y}){({\forall}{x}){({\forall}{y}){\left(\varphi(X,Y,\vec{z})\rightarrow\varphi(\mathit{cons}(x,X),\mathit{cons}(y,Y),\vec{z})\right)}}}}.$

We proceed by induction on $X$ in $({\forall}{Y}){\varphi(X,Y,\vec{z})}$. The
base case follows immediately from the assumptions. For the step case assume
$({\forall}{Y}){\varphi(X,Y,\vec{z})}$ and let $Y$ be fixed. By $\mathrm{CA}$
we can consider two cases. If $Y=\mathit{nil}$, then we are done by the
assumption. Otherwise, there are $y^{\prime}$ and $Y^{\prime}$ such that
$Y=\mathit{cons}(y^{\prime},Y^{\prime})$. By the induction hypothesis, we
obtain $\varphi(X,Y^{\prime},\vec{z})$. Hence, by the third assumptions, we
have
$\varphi(\mathit{cons}(x,X),\mathit{cons}(y^{\prime},Y^{\prime}),\vec{z})$,
that is, $\varphi(\mathit{cons}(x,X),Y,\vec{z})$. ∎

Using induction on a $\forall_{1}$ formula, we can straightforwardly prove the
right cancellation of the append operation for arbitrary lists.

######  Lemma 4.6.

The theory $T_{1}+{\forall_{1}(\mathcal{L}_{1})}\text{-}\mathrm{IND}$ proves

$Y\frown X=Z\frown X\rightarrow Y=Z.$

###### Proof.

We proceed by induction on $X$ in the formula

$({\forall}{Y}){({\forall}{Z}){\left(Y\frown X=Z\frown X\rightarrow
Y=Z\right)}}.$

For the base case, let $Y$ and $Z$ be arbitrary and assume
$Y\frown\mathit{nil}=Z\frown\mathit{nil}$. By Lemma 4.2 we readily obtain
$Y=Z$. For the step case we assume

$({\forall}{Y}){({\forall}{Z}){Y\frown X=Z\frown X\rightarrow Y=Z}}.$

and $Y\frown\mathit{cons}(x,X)=Z\frown\mathit{cons}(x,X)$. By (L1.1), (L1.2),
and Lemma 4.2 we obtain

$\displaystyle(Y\frown\mathit{cons}(x,\mathit{nil}))\frown
X=(Z\frown\mathit{cons}(x,\mathit{nil}))\frown X.$

By the induction hypothesis we obtain
$Y\frown\mathit{cons}(x,\mathit{nil})=Z\frown\mathit{cons}(x,\mathit{nil})$.
Hence, by Lemmas 4.4 and 4.5 we obtain $Y=Z$. ∎

In the remainder of this section we will show that right cancellation of
append cannot be proved by quantifier-free big-step induction on lists.

######  Theorem 4.7.

$T_{1}+\bigcup_{m\in\mathbb{N}}{\mathrm{Open}(\mathcal{L}_{1})}\text{-}\mathrm{IND}_{\curvearrowright{m+1}}\not\vdash
Y\frown X=X\rightarrow Y=\mathit{nil}.$

We proceed as usual by constructing a structure that satisfies the base theory
of lists with append together with quantifier-free induction for lists, but
which contains elements $l_{1},l_{2}$ such that $l_{1}\frown l_{2}=l_{2}$ and
$l_{1}\neq\varepsilon$. Since the concatenation of transfinite sequences of
length greater or equal to $\omega$ does not have the right cancellation
property, as for example $a\frown a^{\omega}=a^{\omega}$, it seems natural to
use concatenation as an interpretation of the append symbol $\frown$.

In Section 3 we have already mentioned that, in order to construct a model of
$T_{0}+{\mathrm{Open}(\mathcal{L}_{0})}\text{-}\mathrm{IND}$ we have to avoid
transfinite sequences $\lambda$ such that $\lambda=w\frown\lambda$ for some
$w\in\mathbb{N}^{*}$, cf. Lemma 3.2. However, we may introduce sequences that
have a transfinitely periodic structure, such as, the sequence
$N_{0}^{\omega}=N_{0}\frown N_{0}^{\omega}$ of length $\omega^{2}$.

In the following we define the set of elements that we will use for the
construction of the model of quantifier-free big-step induction.

######  Definition 4.8.

The structure $M_{2}$ interprets the sort $\mathsf{i}$ as the set $\mathbb{N}$
and the sort $\mathsf{list}$ as the set $\mathfrak{L}$ given by

$\left\\{\lfloor\mathfrak{l}\rfloor\frown w\mid
w\in\mathbb{N}^{*},\mathfrak{l}\in\mathcal{N}^{\beta},\beta<\omega^{2}\right\\}.$

Furthermore, the structure $M_{2}$ interprets the non-logical symbols as
follows

$\displaystyle\mathit{nil}^{M_{2}}\coloneqq\varepsilon,$
$\displaystyle\mathit{cons}^{M_{2}}(n,l)\coloneqq n\frown l,$ $\displaystyle
l_{1}\frown^{M_{2}}l_{2}\coloneqq l_{1}\frown l_{2}.$

We will now first ensure that the structure $M_{2}$ defined above is indeed a
well-defined $\mathcal{L}_{1}$ structure, that is, that it is closed under the
functions $\mathit{nil}^{M_{2}}$, $\mathit{cons}^{M_{2}}$, and
$\frown^{M_{2}}$.

######  Lemma 4.9.

$M_{2}$ is an $\mathcal{L}_{1}$ structure.

###### Proof.

We have to show that $M_{2}$ is closed under the operations
$\mathit{nil}^{M_{2}}$, $\mathit{cons}^{M_{2}}(\cdot,\cdot)$, and
$\cdot\frown^{M_{2}}\cdot$. We have
$\mathit{nil}^{M_{2}}=\varepsilon\in\mathbb{N}^{*}\subseteq\mathfrak{L}$. Now
let $n\in\mathbb{N}$ and $l\in\mathfrak{L}$. Let
$l=\lfloor(m_{\gamma})_{\gamma\leq\beta}\rfloor\frown w$ with
$\beta<\omega^{2}$, $m\in\mathcal{N}^{\beta}$, and $w\in\mathbb{N}^{*}$. If
$\beta=0$, then $n\frown l=n\frown\varepsilon\frown w=n\frown
w\in\mathbb{N}^{*}\subseteq\mathfrak{L}$. Otherwise, if $0<\beta$, then for
$\gamma<\beta$ we let

$m_{\gamma}^{\prime}\coloneqq\begin{cases}(n)\frown m_{0}&\text{if
$\gamma=0$,}\\\ m_{\gamma}&\text{otherwise}\end{cases}$

Now observe that
$(n)\frown\lfloor(m_{\gamma})_{\gamma<\beta}\rfloor=\lfloor(m^{\prime}_{\gamma})_{\gamma<\beta}\rfloor$
and clearly $m^{\prime}_{\gamma}\in\mathcal{N}$, for all $\gamma<\beta$.
Hence, $\mathit{cons}^{M_{2}}(n,l)\in\mathfrak{L}$. Now let
$l_{1},l_{2}\in\mathfrak{L}$ and consider $l_{1}\frown^{M_{2}}l_{2}$. If
$l_{1}\in\mathbb{N}^{*}$, then we use an analogous argument as above. If
$l_{2}\in\mathbb{N}^{*}$, then we clearly have $l_{1}\frown
l_{2}\in\mathfrak{L}$. If $l_{1}$ and $l_{2}$ are non-standard, then for
$i=1,2$ there are $\alpha_{i}<\omega^{2}$,
$\mathfrak{a}_{i}\in\mathcal{N}^{\alpha_{i}}$, $w_{i}\in\mathbb{N}^{*}$ such
that $l_{i}=\lfloor\mathfrak{a}_{i}\rfloor\frown w_{i}$. Moreover, there
exists $\delta\leq\alpha_{2}$ and $w^{\prime}\frown N_{k}\in\mathcal{N}$ such
that $1+\delta=\alpha_{2}$ and $l_{2}=w^{\prime}\frown
N_{k}\frown\lfloor(\mathfrak{a}_{2,1+\gamma})_{\gamma<\delta}\rfloor$.
Therefore, we have

$l_{1}\frown l_{2}=\lfloor\mathfrak{a}_{1}\rfloor\frown(w_{1}\frown
w^{\prime}\frown
N_{k})\frown\lfloor(\mathfrak{a}_{2,1+\gamma})_{\gamma<\delta}\rfloor\frown
w_{2}.$

Since $w_{1}\frown w^{\prime}\frown N_{k}\in\mathcal{N}$ and
$\beta_{1}+\beta_{2}<\omega^{2}$ we have $l_{1}\frown l_{2}\in\mathfrak{L}$. ∎

Next we show that $M_{2}$ satisfies the basic axioms of the list constructors
$\mathit{nil}$ and $\mathit{cons}$, as well as those of the append symbol.

######  Lemma 4.10.

$M_{2}\models T_{1}$.

###### Proof.

Let $n\in\mathbb{N}$ and $l\in\mathfrak{L}$, then there is some ordinal
$\alpha<\omega^{3}$ such that $l\in\mathbb{N}^{\alpha}$. Hence,
$\mathit{cons}^{M_{2}}(n,l)\in\mathbb{N}^{1+\alpha}$. Therefore
$\mathit{cons}^{M_{2}}(n,l)\neq\mathit{nil}^{M_{2}}=\varepsilon=\varnothing$.
Thus $M_{2}\models\eqref{ax:thlistbase:1}$. Now let $n_{1},n_{2}\in\mathbb{N}$
and $l_{1},l_{2}\in\mathfrak{L}$ and assume that $n_{1}\frown
l_{1}=n_{2}\frown l_{2}$. For $i=1,2$, let $\alpha_{i}<\omega^{3}$ such that
$l_{i}\in\mathbb{N}^{\alpha_{i}}$. We thus have $1+\alpha_{1}=1+\alpha_{2}$
which implies $\alpha_{1}=\alpha_{2}$. Therefore, $n_{1}=(n_{1}\frown
l_{1})_{0}=(n_{2}\frown l_{2})_{0}=n_{2}$. Let $\gamma<\alpha_{1}$, then
$l_{1,\gamma}=(n_{1}\frown l_{1})_{1+\gamma}=(n_{2}\frown
l_{2})_{1+\gamma}=l_{2,\gamma}$. Thus, $l_{1}=l_{2}$. Hence
$M_{2}\models\eqref{ax:thlistbase:2}$. Now let $l\in\mathfrak{L}$. We have
$\mathit{nil}^{M_{2}}\frown l=\varepsilon\frown l=l$. Hence,
$M_{2}\models\eqref{ax:thlistappend:1}$. Now let $n\in\mathbb{N}$,
$l,l^{\prime}\in\mathfrak{L}$. Then we have

$\mathit{cons}^{M_{2}}(n,l)\frown^{M_{2}}l^{\prime}=((n)\frown l)\frown
l^{\prime}=(n)\frown(l\frown
l^{\prime})=\mathit{cons}^{M_{2}}(n,l\frown^{M_{2}}l^{\prime}).$

Thus, $M_{2}\models\eqref{ax:thlistappend:2}$. ∎

Since the domain of $M_{2}$ interprets the sort of lists as transfinite
sequences and the append operation as the concatenation of transfinite
sequences, we can decompose $\mathsf{list}$ terms as follows.

######  Lemma 4.11.

Let $t(X,\vec{y})$ be a $\mathcal{L}_{1}$ $\mathsf{list}$-term and $\vec{b}$
elements of $M_{2}$, then there exist $n\in\mathbb{N}$ and
$l_{0},\dots,l_{n}\in\mathfrak{L}$ such that

$M_{2}\models t(X,\vec{b})=l_{0}\frown X\frown l_{1}\frown\dots\frown
l_{n-1}\frown X\frown l_{n}.$

###### Proof.

We proceed by induction on the structure of the term $t$. If $t$ is
$\mathit{nil}$, then $M_{2}\models t=\varepsilon$, and thus we are done. If
$t$ is the variable $X$, then we are done by letting $n=0$ and
$l_{0}=\varepsilon\in\mathbb{N}^{0}$. If $t$ is of the form
$\mathit{cons}(u,t^{\prime})$, then $M_{2}\models u(\vec{b})=k$, for some
$k\in\mathbb{N}$. Hence we apply the induction hypothesis in order to obtain
$n^{\prime}\in\mathbb{N}$ and
$l_{0}^{\prime},\dots,l_{n^{\prime}}^{\prime}\in\mathfrak{L}$ such that
$M_{2}\models t^{\prime}(X,\vec{b})=l_{0}^{\prime}\frown X\frown\dots\frown
l_{n^{\prime}-1}^{\prime}\frown X\frown l_{n^{\prime}}^{\prime}$. Hence,

$M_{2}\models t(X,\vec{b})=(k)\frown l_{0}^{\prime}\frown X\frown\dots\frown
l_{n^{\prime}-1}^{\prime}\frown X\frown l^{\prime}_{n^{\prime}}.$

Thus, we let $n=n^{\prime}$ and $l_{0}=(k))\frown l_{0}^{\prime}$ and
$l_{i}=l_{i}^{\prime}$ for $1\leq i\leq n$. If $t$ is of the form $t_{1}\frown
t_{2}$, then simply apply the induction hypothesis to $t_{1}$ and $t_{2}$. ∎

Equational predicates over $M_{2}$ in one variable stabilize eventually in a
similar way to Lemma 3.11.

######  Lemma 4.12.

Let $E(X)$ be an $\mathcal{L}_{1}(M_{2})$ equation such that $M_{2}\not\models
E(X)$, then there exists $N\in\mathbb{N}$ such that $M_{2}\not\models
E((n)\frown l)$ for all $n\geq N$ and $l\in\mathfrak{L}$.

###### Proof.

Let $E(X)$ be $t_{1}(X)=t_{2}(X)$, then by Lemma 4.11 for $i=1,2$ there exist
$n_{i}\in\mathbb{N}$ and $l_{0}^{i},\dots,l_{n_{i}}^{i}\in\mathfrak{L}$ such
that

$M_{2}\models t_{i}=l_{0}^{i}\frown X\frown\dots\frown l_{n_{i}-1}^{i}\frown
X\frown l_{n_{i}}^{i}.$

By the symmetry of equality we can assume $n_{1}\leq n_{2}$ without loss of
generality. Since $M_{2}\not\models E(X)$ we either have $n_{1}\neq n_{2}$ or
$l_{i}^{1}\neq l_{i}^{2}$ for some $i\in\\{0,\dots,n_{1}\\}$. We start by
assuming that $l_{i}^{1}=l_{i}^{2}$ for $i=0,\dots,n_{1}$ and $n_{1}<n_{2}$.
Then by the left cancellation of $\frown$ we obtain

$M_{2}\models E(X)\leftrightarrow\varepsilon=X\frown
l_{n_{1}+1}^{2}\frown\dots\frown l_{n_{2}-1}^{2}\frown X\frown l_{n_{2}}^{2}.$

Hence, we have $M_{2}\not\models E((n)\frown l)$, for all $n\in\mathbb{N}$ and
$l\in\mathfrak{L}$. Now consider the case where there exists
$j\in\\{0,\dots,n_{1}\\}$ such that $l_{j}^{1}\neq l_{j}^{2}$ and let
$j_{0}\in\\{0,\dots,n_{1}\\}$ be the least such number. There are sequences
$l,l_{j_{0}}^{1\prime}$ and $l_{j_{0}}^{2\prime}$ such that
$l_{j_{0}}^{i}=l\frown l_{j_{0}}^{i\prime}$ for $i=1,2$ and either
$|l_{j_{0}}^{1\prime}|=0$, $|l_{j_{0}}^{2\prime}|\geq 1$, or
$|l_{j_{0}}^{1\prime}|\geq 1$, $|l_{j_{0}}^{2\prime}|=0$, or
$|l_{j_{0}}^{1^{\prime}}|\geq 1$, $|l_{j_{0}}^{2^{\prime}}|\geq 1$ and
$(l_{j_{0}}^{1^{\prime}})_{0}\neq(l_{j_{0}}^{2^{\prime}})_{0}$. Hence, by left
cancellation of concatenation, we obtain

$M_{2}\models E(X)\leftrightarrow l_{j_{0}}^{1\prime}\frown X\frown\dots\frown
l_{n_{1}-1}^{1}\frown X\frown l_{n_{1}}=\\\ l_{j_{0}}^{2\prime}\frown
X\frown\dots\frown l_{n_{2}-1}^{2}\frown X\frown l_{n_{2}}.$

If $l_{j_{0}}^{1^{\prime}}=\varepsilon$ and
$l_{j_{0}}^{2^{\prime}}\neq\varepsilon$, then for $n\neq(l_{j_{0}}^{2})_{0}$,
we have $M_{2}\not\models E((n)\frown l)$ for all $l\in\mathfrak{L}$. The case
where $l_{j_{0}}^{1^{\prime}}\neq\varepsilon$ and
$l_{j_{0}}^{2^{\prime}}=\varepsilon$ is symmetric. Finally, in the case that
$l_{j_{0}}^{1^{\prime}},l_{j_{0}}^{2^{\prime}}\neq\varepsilon$ with
$(l_{j_{0}}^{1^{\prime}})_{0}\neq(l_{j_{0}}^{2^{\prime}})$, we trivially have
$M_{2}\not\models E(l)$ for all $l\in\mathfrak{L}$. ∎

As an immediate consequence of the previous lemma, we obtain the following
result, which essentially says that for a non-standard element $\lambda$ a
$\mathsf{list}$-equation $E(X)$ can eventually be stabilized for predecessors
of $\lambda$.

######  Lemma 4.13.

Let $E(X)$ be an $\mathcal{L}_{1}(M_{2})$ equation such that $M_{2}\not\models
E(X)$ and $\lambda\in\mathfrak{L}\setminus\mathbb{N}^{*}$. Then there exists
$N\in\mathbb{N}$ such that $M_{2}\not\models E(\lambda\uparrow n)$ for all
$n\geq N$.

###### Proof.

First by applying Lemma 4.12 we obtain $m_{0}$ such that $M\not\models
E((m)\frown l)$ for all $m\geq m_{0}$ and $l\in\mathfrak{L}$. Since
$\lambda\not\in\mathbb{N}^{*}$, there clearly is $n_{0}\in\mathbb{N}$ such
that $\lambda\uparrow n_{0}=N_{m_{0}}\frown\lambda^{\prime}$ for some
$\lambda^{\prime}\in\mathfrak{L}$. Since $(\lambda\uparrow
N+k)_{0}=m_{0}+k\geq m_{0}$ for $k\in\mathbb{N}$, we have $M_{2}\not\models
E(\lambda\uparrow n)$ for all $n\geq n_{0}$. ∎

The previous two lemmas show that the truth value of formulas in $M_{2}$ on
non-standard elements eventually synchronizes with that on standard elements,
when considering sufficiently distant predecessors.

######  Lemma 4.14.

Let $\varphi(X)$ be an open $\mathcal{L}_{1}(M_{2})$ formula and
$\lambda\in\mathfrak{L}$, then there exists $n_{0}\in\mathbb{N}$ such that

$M_{2}\models\varphi(\lambda\uparrow n)\leftrightarrow\varphi((n)),$

for all $n\geq n_{0}$.

###### Proof.

Clearly, it suffices to consider the $\mathsf{list}$-equations of $\varphi$,
since the $\mathsf{i}$-equations do not depend on the variable $X$. Let
$E_{1}(X),\dots,E_{k}(X)$ be the atoms of $\varphi$ with $M_{2}\not\models
E_{i}(X)$, for $i=1,\dots,k$. Then by Lemmas 4.13 and 4.12 there is
$n_{0}\in\mathbb{N}$ such that $M_{2}\not\models E_{i}(\lambda\uparrow n)$ and
$M_{2}\not\models E_{i}((n))$ for $n\geq n_{0}$ and $i=1,\dots,k$. Since we
have $M_{2}\models E(X)$ for the other $\mathsf{list}$-atoms of $\varphi$, we
obtain $M_{2}\models\varphi(\lambda\uparrow n)\leftrightarrow\varphi((n))$ for
$n\geq n_{0}$. ∎

We are now ready to show that $M_{2}$ satisfies open big-step induction.

######  Proposition 4.15.

Let $m\in\mathbb{N}$ with $m\geq 1$, then
$M_{2}\models{\mathrm{Open}(\mathcal{L}_{1})}\text{-}\mathrm{IND}_{\curvearrowright{m}}$.

###### Proof.

Let $\varphi(X)$ be a quantifier-free $\mathcal{L}_{1}(M_{2})$ formula. Assume
that

$\displaystyle
M_{2}\models\bigwedge_{i=1,\dots,m}\varphi(\mathit{cons}(x_{1},\dots,x_{i-1};\mathit{nil})),$
($\ast$) $\displaystyle
M_{2}\models\varphi(X)\rightarrow\varphi(\mathit{cons}(x_{1},\dots,x_{m};X)).$
($\star$)

Let $\lambda\in\mathfrak{L}$. If $\lambda\in\mathbb{N}^{*}$, then a
straightforward induction making use of ($\ast$ ‣ 4) and ($\star$ ‣ 4) yields
$M_{2}\models\varphi(\lambda)$. Now we consider the case
$\lambda\notin\mathbb{N}^{*}$, that is, $\lambda$ is a non-standard element.
By Lemma 4.14 there is $n_{0}\in\mathbb{N}$ such that
$M_{2}\models\varphi(\lambda\uparrow n)$ if and only if
$M_{2}\models\varphi((n))$ for all $n\geq n_{0}$. In particular, we thus have

$M_{2}\models\varphi(\lambda\uparrow
n_{0}+m+i)\leftrightarrow\varphi((n_{0}+m+i))$

for $i=0,\dots,m-1$. Since, $M_{2}\models\varphi(w)$ for all
$w\in\mathbb{N}^{*}$, we obtain $M_{2}\models\varphi(\lambda\uparrow
n_{0}+m+i)$ for $i=0,\dots,m-1$. By a straightforward induction starting with
$M_{2}\models\varphi(\lambda\uparrow n_{0}+m-1)$, …,
$M_{2}\models\varphi(\lambda\uparrow n_{0})$ and making use of ($\star$ ‣ 4)
we obtain $M_{2}\models\varphi(w\frown(\lambda\uparrow n_{0}))$ for all
$w\in\mathbb{N}^{*}$. Therefore, we have in particular
$M_{2}\models\varphi(\lambda)$. ∎

###### Proof of Theorem 4.7.

Clearly, $N_{0}\in\mathfrak{L}$. Since
$N_{0}^{\omega}=\lfloor(N_{0})_{\gamma<\omega}\rfloor$, we have
$N_{0}^{\omega}\in\mathfrak{L}$. Now observe that $N_{0}\frown
N_{0}^{\omega}=N_{0}^{\omega}$ but $N_{0}\neq\varnothing$. Hence, by
Proposition 4.15 we are done. ∎

This result is of interest for automated inductive theorem proving, because it
essentially provides a lower bound on the power necessary for the proof of a
rather simple yet practically relevant property about the important datatype
of lists.

The unprovability of right cancellation of concatenation is a first step
towards a classification of the inductive power needed to prove certain
practically interesting properties of finite Lisp-like lists. Theorem 4.7 as
well as the auxiliary results of this section give rise to many related
questions and conjectures that we will briefly discuss in the following.

We conjecture that even quantifier-free simultaneous induction on several
variables with big-steps does not prove right cancellation of the
concatenation operation. Let $\vec{x}=(x_{1},\dots,x_{n})$ be a finite
sequence and $i\in\mathbb{N}$ such that $1\leq i\leq n$, then by
$\vec{x}_{<i}$ we denote the sequence $(x_{1},\dots,x_{i-1})$. Similarly,
$\vec{x}_{>i}$ denotes the sequence $(x_{i+1},\dots,x_{n})$.

######  Definition 4.16.

Let $\vec{X}=(X_{1},\dots,X_{m})$ be pairwise distinct variables with $m\geq
1$, $\vec{p}=(p_{1},\dots,p_{m})$ a sequence of non-zero natural numbers, and
$\varphi(\vec{X},\vec{z})$ a formula. The multivariate big-step list induction
axiom $I_{\vec{X}\curvearrowright\vec{p}}^{\mathsf{list}}\varphi$ for
$\varphi$ is given by

$\left(\begin{split}\bigwedge_{i=1}^{m}\bigwedge_{j=1}^{p_{i}}({\forall}{\vec{X}_{<i}}){({\forall}{\vec{X}_{>i}}){({\forall}{x_{1},\dots,x_{j-1}}){\varphi(\vec{X}_{<i},\mathit{cons}(x_{1},\dots,x_{j-1};\mathit{nil}),\vec{X}_{>i},\vec{z})}}}\\\
\wedge({\forall}{\vec{X}}){({\forall}{\vec{x}^{p_{1}}}){\dots({\forall}{\vec{x}^{p_{m}}}){\left(\varphi(\vec{X},\vec{z})\rightarrow\varphi(\mathit{cons}(\vec{x}^{p_{1}};X_{1}),\dots,\mathit{cons}(\vec{x}^{p_{m}};X_{m}),\vec{z})\right)}}}\end{split}\right)\\\
\rightarrow({\forall}{\vec{X}}){\varphi(\vec{X})}.$

where the $\vec{x}^{p_{i}}$ with $i\in\\{1,\dots,m\\}$ are vectors of
variables of sort $\mathsf{i}$ whose elements are all pairwise distinct. Let
$\Phi$ be a set of formulas, then theory
${\Phi}\text{-}\mathrm{IND}^{\mathsf{list}}_{\nearrow_{\curvearrowright}}$ is
axiomatized by $I_{\vec{X}\curvearrowright\vec{p}}^{\mathsf{list}}\varphi$
with $\varphi(\vec{X},\vec{z})\in\Phi$ and $\vec{X},\vec{p}$ as above.

######  Conjecture 4.17.

$T_{1}+{\mathrm{Open}(\mathcal{L}_{1})}\text{-}\mathrm{IND}^{\mathsf{list}}_{\nearrow_{\curvearrowright}}\not\vdash
Y\frown X=Z\frown X\rightarrow Y=Z$.

A positive answer to this question would thus greatly improve upon our Theorem
4.7. A related question of interest is whether single-element right
cancellation can be proven by quantifier-free big-step induction in one
variable.

The subject of AITP mainly focuses on the mechanization of induction in
general, rather than on the mechanization of individual theories.
Nevertheless, the theories of lists with concatenation considered in this
section are of some practical relevance. Hence, it may be valuable to
investigate their mechanization separately. Because of the homomorphic
relation between natural numbers with addition and lists with concatenation,
it could be especially interesting to investigate whether simple theories of
lists such as $T_{1}+{\forall_{1}(\mathcal{L}_{1})}\text{-}\mathrm{IND}$ have
finite axiomatizations analogous to the one shown in [27] for natural numbers
with addition.

Finally, let us observe that as an immediate consequence of Proposition 4.15
we obtain the unprovability of right-decomposition of list by open big-step
induction.

######  Corollary 4.18.

$T_{1}+\bigcup_{m\geq
1}{\mathrm{Open}(\mathcal{L}_{1})}\text{-}\mathrm{IND}_{\curvearrowright{m}}$
does not prove

$X=\mathit{nil}\vee({\exists}{x^{\prime}}){({\exists}{X^{\prime}}){X=X^{\prime}\frown\mathit{cons}(x^{\prime},\mathit{nil})}}.$

###### Proof.

Consider the element $N_{0}\in{M_{2}}({\mathsf{list}})$ and observe that
$N_{0}\neq\mathit{nil}$ but since $|N_{0}|=\omega$, we cannot express $N_{0}$
as $\lambda\frown(n)$ with $\lambda\in\mathbb{N}^{\leq\omega}$ and
$n\in\mathbb{N}$. Now, the claim follows from Proposition 4.15. ∎

Clearly, the formula
$X=\mathit{nil}\vee({\exists}{x^{\prime}}){({\exists}{X^{\prime}}){X=X^{\prime}\frown\mathit{cons}(x^{\prime},\mathit{nil})}}$
is provable by induction on the formula itself, that is, by $\exists_{1}$
induction. This gives rise to the question whether right-decomposition can be
proved by $\forall_{1}$ induction and more generally to the more general
question how $\exists_{1}$ induction and $\forall_{1}$ induction over lists
with concatenation are related. This question is relevant for AITP, since
there are systems such as [21] that are based on $\exists_{1}$ induction [18]
and systems such as [10] that are based on $\forall_{1}$ induction [31,
Chapter 5]. We plan to investigate this question separately in the future.

##  5 Conclusion

In this article we have shown two main results about induction for lists.
Firstly, in Section 3 we have shown that quantifier-free $(m+1)$-step
induction can in general not be simulated with quantifier-free $m$-step
induction. In particular, this result thus renders impossible a reductive
implementation of quantifier-free big-step induction in AITP systems with an
induction mechanism based on quantifier-free induction. This observation may
be relevant for future extensions of systems based on quantifier-free one-step
induction mechanism, such as the AITP system described in [26, Section 3.2].
The idea is that whenever an induction principle can be reduced to a simpler
one, then for the sake of soundness one should consider the reduction.

The second main result of this article, shown in Section 4, is the
unprovability of right cancellation of the concatenation for lists by
quantifier-free big-step induction. Thus automated inductive theorem provers
have to implement a comparatively strong induction mechanism in order to the
prove seemingly simple property of right cancellation of concatenation.

In the light of the results of Section 3, a natural choice would be to
implement an induction principle that can handle at least $\forall_{1}$
induction formulas with conjunction. Such an induction principle permits a
reductive implementation of $\forall_{1}$ big-step induction. An example of a
system implementing such an induction mechanism is the one described in [10]
and analyzed in [31, Chapter 5].

One direction for future research is to carry out similar investigations
focusing on other datatypes, induction principles, and properties. In
principle questions such as the one addressed in Section 4 could be considered
for every problem in benchmark suites such as [7] in order to obtain a
classification of the difficulty of the problems that complements empirical
results.

Furthermore, the results in this article raise a number of questions and
conjectures that we would like to address in the future. In particular, we
would like to investigate 4.17, since a positive answer, showing that
quantifier-free induction combining, both, simultaneous induction and big-step
induction does not prove right cancellation of concatenation, would
significantly strengthen the result of Section 4. Another interesting question
is whether the right injectivity of concatenation (see Lemma 4.4) can be
proved with quantifier-free big-step induction. Finally, the use of
transfinite lists used in this article are reminiscent of streams defined by
coinduction. It could be interesting investigate to which extent the
techniques employed for the analysis of AITP systems can be transferred to
systems that automate the coinduction principle such as [22, 11].

AITP

    automated inductive theorem proving

## References

  * [1] S. A. Aleksandrova and N. A. Bazhenov.  On decidability of list structures.  Siberian Mathematical Journal, 60(3):377–388, May 2019.
  * [2] N. A. Bazhenov.  Automatic structures and the theory of lists.  Siberian Electronic Mathematical Reports, 12:714–722, 2015.
  * [3] James Brotherston, Nikos Gorogiannis, and Rasmus Lerchedahl Petersen.  A generic cyclic theorem prover.  In Ranjit Jhala and Atsushi Igarashi, editors, Programming Languages and Systems, volume 7705 of Lecture Notes in Computer Science, pages 350–367. Springer, 2012.
  * [4] Alan Bundy, David A. Basin, Dieter Hutter, and Andrew Ireland.  Rippling - meta-level guidance for mathematical reasoning, volume 56 of Cambridge tracts in theoretical computer science.  Cambridge University Press, 2005.
  * [5] Alan Bundy, Frank van Harmelen, Jane Hesketh, Alan Smaill, and Andrew Stevens.  A rational reconstruction and extension of recursion analysis.  In N. S. Sridharan, editor, Proceedings of the Eleventh International Joint Conference on Artificial Intelligence, volume 1, pages 359–365. Morgan Kaufmann, 1989.
  * [6] Koen Claessen, Moa Johansson, Dan Rosén, and Nicholas Smallbone.  Automating inductive proofs using theory exploration.  In Maria Paola Bonacina, editor, Automated Deduction - CADE-24, volume 7898 of Lecture Notes in Computer Science, pages 392–406. Springer, 2013.
  * [7] Koen Claessen, Moa Johansson, Dan Rosén, and Nicholas Smallbone.  TIP: Tons of inductive problems.  In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 333–337. Springer, 2015\.
  * [8] Hubert Comon.  Inductionless induction.  In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, volume 1, chapter 14, pages 913 – 962. North-Holland, Amsterdam, 2001.
  * [9] John Corcoran, William Frank, and Michael Maloney.  String theory.  The Journal of Symbolic Logic, 39(4):625–637, 1974.
  * [10] Simon Cruanes.  Superposition with structural induction.  In Clare Dixon and Marcelo Finger, editors, Frontiers of Combining Systems, volume 10483 of Lecture Notes in Computer Science, pages 172–188. Springer, 2017.
  * [11] Sólrún Halla Einarsdóttir, Moa Johansson, and Johannes Åman Pohjola.  Into the infinite - theory exploration for coinduction.  In Jacques D. Fleuriot, Dongming Wang, and Jacques Calmet, editors, Artificial Intelligence and Symbolic Computation, volume 11110 of Lecture Notes in Computer Science, pages 70–86. Springer, 2018.
  * [12] S. S. Goncharov.  A theory of lists and its models.  Vychislitel’nye Sistemy, 114:84–95, 1986.
  * [13] Andrzej Grzegorczyk.  Undecidability without arithmetization.  Studia Logica, 79(2):163–230, 2005.
  * [14] Andrzej Grzegorczyk and Konrad Zdanowski.  Undecidability and Concatenation.  In A. Ehrenfeucht, V.W. Marek, and M. Srebrny, editors, Andrzej Mostowski and Foundational Studies, pages 72–91. IOS Press, 2008.
  * [15] Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl, and Andrei Voronkov.  Induction with generalization in superposition reasoning.  In Christoph Benzmüller and Bruce R. Miller, editors, Intelligent Computer Mathematics, volume 12236 of Lecture Notes in Computer Science, pages 123–137. Springer, 2020.
  * [16] Márton Hajdu, Petra Hozzová, Laura Kovács, and Andrei Voronkov.  Induction with recursive definitions in superposition.  In Ruzica Piskac and Michael W. Whalen, editors, Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021, volume 2 of Conference Series: Formal Methods in Computer-Aided Design, pages 246–255. TU Wien Academic Press, 2021.
  * [17] Stefan Hetzl and Jannik Vierling.  Clause Set Cycles and Induction.  Logical Methods in Computer Science, 16(4):11:1–11:17, November 2020.
  * [18] Stefan Hetzl and Jannik Vierling.  Unprovability results for clause set cycles.  Theoretical Computer Science, 2022.
  * [19] Stefan Hetzl and Jannik Vierling.  Induction and Skolemization in saturation theorem proving.  Annals of Pure and Applied Logic, 174(1), 2023.
  * [20] Stefan Hetzl and Tin Lok Wong.  Some observations on the logical foundations of inductive theorem proving.  Logical Methods in Computer Science, 13(4):10:1–10:26, April 2018\.
  * [21] Abdelkader Kersani and Nicolas Peltier.  Combining superposition and induction: A practical realization.  In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Frontiers of Combining Systems, volume 8152 of Lecture Notes in Computer Science, pages 7–22. Springer, 2013.
  * [22] K. Rustan M. Leino and Michał Moskal.  Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier.  In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: Formal Methods, volume 8442 of Lecture Notes in Computer Science, pages 382–398. Springer, 2014.
  * [23] Daniel J. Moore and Bruce Russell.  Axiomatic data type specifications: A first order theory of linear lists.  Acta Informatica, 15:193–207, 1981.
  * [24] Derek C. Oppen.  Reasoning about recursively defined data structures.  In Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’78, page 151–157, New York, NY, USA, 1978. Association for Computing Machinery.
  * [25] W. V. Quine.  Concatenation as a basis for arithmetic.  The Journal of Symbolic Logic, 11(4):105–114, 1946.
  * [26] Giles Reger and Andrei Voronkov.  Induction in saturation-based proof search.  In Pascal Fontaine, editor, Automated Deduction - CADE 27, volume 11716 of Lecture Notes in Computer Science, pages 477–494. Springer, 2019.
  * [27] Joseph Robert Shoenfield.  Open sentences and the induction axiom.  Journal of Symbolic Logic, 23(1):7–12, 1958.
  * [28] Gaisi Takeuti and Wilson M. Zaring.  Introduction to axiomatic set theory, volume 1 of Graduate texts in mathematics.  Springer, 1971.
  * [29] Alfred Tarski.  Der Wahrheitsbegriff in den formalisierten Sprachen.  Studia Philosophica, 1:261–405, 1935.
  * [30] J. W. Thatcher.  Decision problems for multiple successor arithmetics.  The Journal of Symbolic Logic, 31(2):182–190, 1966.
  * [31] Jannik Vierling.  The limits of automated inductive theorem provers.  PhD thesis, Technische Universität Wien, 2022.
  * [32] Albert Visser.  Growing Commas. A Study of Sequentiality and Concatenation.  Notre Dame Journal of Formal Logic, 50(1):61–85, 2009.

  *[AITP]: automated inductive theorem proving


# A generalization of the Brauer–Fowler theorem

Saveliy V. Skresanov The research was carried out within the framework of the
Sobolev Institute of Mathematics state contract (project FWNF-2022-0002).

###### Abstract

The famous Brauer-Fowler theorem states that the order of a finite simple
group can be bounded in terms of the order of the centralizer of an
involution. Using the classification of finite simple groups, we generalize
this theorem and prove that if a simple locally finite group has an involution
which commutes with at most $n$ involutions, then the group is finite and its
order is bounded in terms of $n$ only. This answers a question of Strunkov
from the Kourovka notebook.

## Introduction

In 1955 Brauer and Fowler proved a result which became one of the staples of
the classification of finite simple groups (CFSG):

The Brauer-Fowler theorem [2, Corollary (2I)] _If $G$ is a finite simple group
and the centralizer of some involution has order $n$, then $|G|<[n(n+1)/2]!$.
In particular, there exist only a finite number of finite simple groups with a
given centralizer of an involution._

The proof of this theorem is elementary and relies on an ingenious technique
to count involutions in a group. Since then this method was applied to obtain
other results relating the structure of a group with properties of its
involutions, notable examples being the Thompson order formula and the Brauer-
Wielandt formula (see [5, Part I, chapter 34]). The Brauer-Fowler theorem
itself was also widely generalized. For example, in [7] it is proved that for
a finite group $G$ with an involution $t$, one has $|G:F(G)|<|C_{G}(t)|^{4}$,
where $F(G)$ is the Fitting subgroup of $G$. Hartley proved [10] that if a
nonabelian finite simple group $G$ admits an automorphism of order $k$ having
$n$ fixed points, then $|G|$ is bounded in terms of $k$ and $n$.

In 1985 Strunkov showed that in some cases the order of the centralizer of an
involution can be replaced by the number of involutions in that centralizer.
The following is a corollary from his results:

######  Proposition 1 ([15, Theorem 1]).

Let $G$ be a periodic simple group, and let $t,z\in G$ be nonconjugate
involutions. If the sets $C_{G}(t)\cap(t^{G}\cup z^{G})$ and
$C_{G}(z)\cap(t^{G}\cup z^{G})$ are finite and have at most $n$ elements, then
$G$ is also finite and its order can be bounded in terms of $n$ only.

In particular, if $t$ and $z$ centralize at most $n$ involutions each, then
$G$ is finite and its order is bounded in terms of $n$.

It is natural to ask if it is possible to prove a result similar to Strunkov’s
for one involution only (at least in the case of finite groups). And indeed,
in 11th issue of the Kourovka notebook [13] Strunkov asks:

Question 11.96. _Is it true that, for a given number $n$, there exist only
finitely many finite simple groups each of which contains an involution which
commutes with at most $n$ involutions of the group? Is it true that there are
no infinite simple groups satisfying this condition?_

For the second part of the question the answer is “no”, since
$\mathrm{PSL}_{2}(\mathbb{R})$ is an infinite simple group which contains an
involution, but does not contain a subgroup isomorphic to the Klein 4-group.
Nevertheless, the answer to the first part of the question is positive, in
fact, it is true in the more general context of simple locally finite groups.

######  Theorem 1 (mod CFSG).

Let $G$ be a simple locally finite group, and let $t\in G$ be an involution.
If there are at most $n$ involutions in $G$ commuting with $t$, then $G$ is
finite and its order is bounded in terms of $n$ only.

The principal case in the proof is that of a finite simple group of Lie type.
We use a result of Guralnick and Robinson [8] to bound the rank of the group,
and a combinatorial argument together with character ratio bounds to bound the
field. An explicit bound of the form $|G|\leq C_{1}\cdot n^{C_{2}\cdot n^{2}}$
for some universal constants $C_{1},C_{2}>0$ can be extracted from the proof,
but it is clearly far from being tight.

We end the introduction with an open problem. Recall that by Shunkov’s theorem
[14], a periodic group with a finite centralizer of an involution is almost
solvable, so a simple group with such an involution is finite, and hence the
Brauer–Fowler theorem can be extended to periodic groups. Proposition 1 of
Strunkov also applies to periodic groups. It is quite interesting whether
Theorem 1 can be generalized to periodic simple groups:

Open problem. _Let $G$ be a periodic simple group, and suppose that $G$
contains an involution which commutes only with a finite number of
involutions. Is it true that $G$ is finite?_

It follows from another theorem of Strunkov [15, Theorem 2] that if an
infinite 2-group $G$ has an involution $t\in G$ such that $C_{G}(t)\cap t^{G}$
is finite, then the center of $G$ is nontrivial. In particular, such $G$
cannot be simple and hence a hypothetical counterexample to the above question
must contain elements of odd order.

We also note that a result of Durakov [4, Theorem 2] implies that a positive
solution to this problem, even in the case when the centralizer of an
involution $t\in G$ is a Prüfer 2-group, would resolve a question of Mazurov
from the Kourovka notebook [13, 15.54]. Namely, it is conjectured that in such
$G$ all elements of odd order inverted by $t$ form a subgroup.

## Proof

First we prove the result for _finite_ simple groups. Let $G$ be a finite
simple group, and let $t\in G$ be some involution. We may assume that $G$ is
nonabelian and its order is larger than some universal constant, in particular
it is not a sporadic finite simple group. Suppose that there are at most $n$
involutions commuting with $t$. We start from a result by Guralnick and
Robinson.

######  Proposition 2 ([8, Corollary 2]).

Let $G$ be a finite quasisimple group. If $x,y\in G$ are involutions, then $x$
commutes with some conjugate of $y$.

It follows that there are at most $n$ conjugacy classes of involutions in $G$.
If $G$ is an alternating group of degree $m$, then $G$ contains at least
$\lfloor m/4\rfloor$ conjugacy classes of involutions, and hence $m\leq 4n+1$,
so the order of $G$ is bounded in terms of $n$.

From now on we may assume that $G$ is a finite simple group of Lie type of
rank $r$ over the field of order $q$. Note that the rank $r$ of $G$ can be
bounded in terms of the number of conjugacy classes of involutions (and hence
in terms of $n$). Indeed, this follows from [6, Table 4.5.1] for $q$ odd, and
[1, Sections 4–6] for $q$ even. Now it suffices to bound $q$ in terms of $n$.

Suppose that $G$ has at least two conjugacy classes of involutions, and let
$\mathcal{K}$ be a conjugacy class of involutions not containing $t$. For any
$w\in\mathcal{K}$ the group generated by $t$ and $w$ is a dihedral group. Its
order must be divisible by $4$, since otherwise the subgroups generated by $t$
and $w$ would be conjugate as the Sylow subgroups of the dihedral group in
question. Hence there exists some involution $z$ commuting with $t$ and $w$.
Since there are at most $n$ involutions commuting with $t$, by pigeonhole
principle there exists an involution $z$ such that it commutes with at least
$|\mathcal{K}|/n$ elements from $\mathcal{K}$, or in other words,
$|\mathcal{K}\cap C_{G}(z)|\geq|\mathcal{K}|/n$. Now to deduce a bound on $q$
we will apply what is essentially an argument about fixed-point ratios, cf.
[3, Lemma 1.2 (iv)].

Let $\pi:G\to\mathbb{C}$ be the permutation character of a transitive action
of $G$ on its conjugacy class $\mathcal{K}$. By definition of $\pi$, for $g\in
G$ we have $\pi(g)=|\mathcal{K}\cap C_{G}(g)|$. Since $\pi(1)=|\mathcal{K}|$,
we have

$\frac{\pi(z)}{\pi(1)}=\frac{|\mathcal{K}\cap
C_{G}(z)|}{|\mathcal{K}|}\geq\frac{1}{n}.$

As the action is transitive, we have a decomposition
$\pi=1_{G}+\chi_{1}+\dots+\chi_{k}$, $k\geq 1$, where $1_{G}$ is the trivial
character and $\chi_{1},\dots,\chi_{k}$ are some nontrivial irreducible
ordinary characters (with repetitions allowed). We claim that for some $i$ we
have

$\frac{\pi(z)}{\pi(1)}\leq\frac{1+|\chi_{i}(z)|}{1+\chi_{i}(1)}.$

Set $f=\pi(z)/\pi(1)$, and assume that for all $i=1,\dots,k$ we have
$f(1+\chi_{i}(1))>1+|\chi_{i}(z)|$. Then

$\pi(z)=\left|1+\sum_{i=1}^{k}\chi_{i}(z)\right|\leq
1-k+\sum_{i=1}^{k}(1+|\chi_{i}(z)|)<1-k+f\sum_{i=1}^{k}(1+\chi_{i}(1))=\\\
=1-k+f(k-1+\pi(1))=\pi(z)-(k-1)(1-f)\leq\pi(z)$

and this is a contradiction.

Therefore for some $i$ we have $1/n\leq(1+|\chi_{i}(z)|)/(1+\chi_{i}(1))$.
Note that since $z$ is an involution, $\chi_{i}(z)$ is an integer. If
$\chi_{i}(z)=0$, then $\chi_{i}(1)\leq n-1$ and the order of $G$ is bounded by
Jordan’s theorem (one can also obtain a bound from the main result of [12]).
If $\chi_{i}(z)$ is nonzero, then $|\chi_{i}(z)|\geq 1$ and hence $1/n\leq
2|\chi_{i}(z)|/\chi_{i}(1)$. Gluck’s bound [9] for character ratios gives
$|\chi_{i}(z)|/\chi_{i}(1)\leq C\cdot q^{-1/2}$ for some universal constant
$C$, thus $q\leq(2Cn)^{2}$. Together with the bound on the rank of $G$ this
gives an upper bound on the order of $G$ in the case when there are at least
two conjugacy classes of involutions.

Now suppose that $G$ has only one conjugacy class of involutions. If $q$ is
even, it follows from [6, Theorem 2.4.1 and Table 2.4] that $G$ contains an
elementary abelian subgroup of order $q$; a root subgroup suffices in most
cases. As we can always conjugate $t$ inside such a subgroup, it follows that
$t$ commutes with at least $q-1$ involutions and hence $q\leq n+1$ as wanted.

Finally, if $q$ is odd and $G$ has a unique conjugacy class of involutions, it
follows from [6, Table 4.5.1] that $G$ is one of the following groups:

$\mathrm{PSL}_{2}(q),\,\mathrm{PSL}_{3}(q),\,\mathrm{PSL}_{4}(q),\,\mathrm{PSU}_{3}(q),\,\mathrm{PSU}_{4}(q),\,G_{2}(q),\,{}^{2}G_{2}(q),\,{}^{3}D_{4}(q).$

If $G=\mathrm{PSL}_{2}(q)$, then the centralizer of $t$ is a dihedral group of
order $q\pm 1$, in particular, it contains at least $(q-1)/2$ involutions and
$q\leq 2n+1$ as wanted. Now, it is sufficient to prove that
$\mathrm{PSL}_{2}(q)$ lies in $G$ in all the other cases, provided that $q$ is
large enough. Indeed, we can always conjugate an involution inside
$\mathrm{PSL}_{2}(q)$ and obtain the same bound on $q$ in terms of $n$.

Recall that $\Omega_{3}(q)\leq\mathrm{SL}_{3}(q)$ and
$\Omega_{3}(q)\simeq\mathrm{PSL}_{2}(q)$ is a simple group for $q$ large
enough. Therefore $\mathrm{PSL}_{3}(q)$ contains $\mathrm{PSL}_{2}(q)$. The
group $\mathrm{PSL}_{4}(q)$ contains $\mathrm{SL}_{3}(q)$ and hence
$\mathrm{PSL}_{2}(q)$. A unitary group $\mathrm{SU}_{3}(q)$ contains
$\Omega_{3}(q)\simeq\mathrm{PSL}_{2}(q)$, hence $\mathrm{PSU}_{3}(q)$ also
contains $\mathrm{PSL}_{2}(q)$. The group $\mathrm{SU}_{4}(q)$ contains
$\mathrm{GU}_{3}(q)$, thus again $\mathrm{PSL}_{2}(q)$ can be embedded into
$\mathrm{PSU}_{4}(q)$.

As for the exceptional groups of Lie type, $G_{2}(q)$ contains
$\mathrm{SL}_{3}(q)$, see [17, Table 4.1], and hence contains
$\mathrm{PSL}_{2}(q)$. The group ${}^{2}G_{2}(q)$ contains
$\mathrm{PSL}_{2}(q)$ by [17, Theorem 4.2], and ${}^{3}D_{4}(q)$ contains
$G_{2}(q)$ by [17, Theorem 4.3]. As we showed earlier, this implies an upper
bound on $q$ in terms of $n$, hence the theorem is proved in the case when $G$
is finite.

Let $f(n)$ denote the largest size of a finite simple group, which contains an
involution commuting with at most $n$ involutions. By what we proved above,
$f(n)$ is defined correctly.

Now assume that $G$ is an infinite simple locally finite group, and let $t\in
G$ be an involution. Let $t_{1},\dots,t_{n}\in G$ be the involutions commuting
with $t$; of course, $t$ is one of them. Let $T$ be a finite subgroup of $G$
containing $t_{1},\dots,t_{n}$. Since $G$ is infinite, we may choose $T$ to be
such that $|T|>f(n)$. A simple locally finite group has a Kegel cover [11,
Corollary 4.3], hence there is a finite subgroup $H$ of $G$ and a normal
subgroup $N$ of $H$, such that $H/N$ is simple, $T\leq H$ and $T\cap N=1$.

Suppose that the order of $N$ is even. Then it contains an involution, and
hence the number of involutions in $N$ is odd. The involution $t$ lies in $H$
and acts on $N$ by conjugation, therefore there must be an involution $z\in N$
centralized by $t$. But then $z$ is be one of $t_{1},\dots,t_{n}$ and thus
must lie in $T$. This is a contradiction to $T\cap N=1$, therefore the order
of $N$ is odd.

By [16, Corollary 3.28], since the orders of $t$ and $N$ are coprime, the
centralizer of an involution $tN$ in $H/N$ is the image of the centralizer of
$t$ in $H$. It follows that a finite simple group $H/N$ has an involution
which commutes with at most $n$ involutions. By what we proved above, this
implies that the order of $H/N$ is at most $f(n)$. This is a contradiction,
since $f(n)<|T|\leq|H/N|\leq f(n)$. Therefore $G$ must be finite and the
theorem is proved. ∎

##  1 Acknowledgements

The author expresses his gratitude to A.S. Mamontov and A.V. Vasil’ev for
helpful remarks improving the exposition of this paper.

## References

  * [1] M. Aschbacher, G.M. Seitz, _Involutions in Chevalley groups over fields of even order_ , Nagoya Math. J. 63 (1976), 1–91.
  * [2] R. Brauer, K.A. Fowler, _On groups of even order_ , Ann. Math. 62:3 (1955), 565–583.
  * [3] T.C. Burness, _Simple groups, fixed point ratios and applications_ , in Local representation theory and simple groups, 267–322, EMS Ser. Lect. Math., Eur. Math. Soc., Zürich, 2018.
  * [4] B.E. Durakov, _On some groups of 2-rank 1_ , Proc. Steklov Inst. Math. (Supplementary issues) 313:1 (2021), S54–S57.
  * [5] D. Gorenstein, R. Lyons, R. Solomon, _The classification of the finite simple groups, Number 2_ (American Mathematical Society, 1994).
  * [6] D. Gorenstein, R. Lyons, R. Solomon, _The classification of the finite simple groups, Number 3_ (American Mathematical Society, 1994).
  * [7] R.M. Guralnick, G.R. Robinson, _Variants of some of the Brauer-Fowler theorems_ , J. Algebra 558 (2020), 453–484.
  * [8] R.M. Guralnick, G.R. Robinson, _Commuting involutions and elementary abelian subgroups of simple groups_ , J. Algebra 607, part A (2022), 300–314.
  * [9] D. Gluck, _Sharper character value estimates for groups of Lie type_ , J. Algebra 174 (1995), 229–266.
  * [10] B. Hartley, _A general Brauer-Fowler theorem and centralizers in locally finite groups_ , Pacific J. Math. 152:1 (1992), 101–117.
  * [11] O. Kegel, B.A.F. Wehrfritz, _Locally finite groups_ (North Holland, 1973).
  * [12] V. Landazuri, G.M. Seitz, _On the minimal degrees of projective representations of the finite Chevalley groups_ , J. Algebra 32 (1974), 418–443.
  * [13] V.D. Mazurov, E.I. Khukhro (eds.), _Unsolved problems in group theory. The Kourovka notebook, 20th edn_ Sobolev Institute of Mathematics, Novosibirsk (2022).
  * [14] V.P. Shunkov, _On periodic groups with an almost regular involution_ , Algebra and Logic 11 (1972), 260–272.
  * [15] S.P. Strunkov, _An analogue of the Brauer-Fowler theorem_ , Russian Math. Surveys 40:6 (1985), 141–142.
  * [16] M. Isaacs, _Finite group theory_ (Providence, Rhode Island, 2008).
  * [17] R.A. Wilson, _The finite simple groups_ (Springer London, 2009).

_Saveliy V. Skresanov_

_Sobolev Institute of Mathematics, 4 Acad. Koptyug avenue, Novosibirsk,
Russia_

_Email address<EMAIL_ADDRESS>