Quantifier-free induction for lists

Abstract

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

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 [10, 21, 25], 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 develo** 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 [17,18,19,20, 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 [22] 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 [23]. In [1, 2, 12] the computability aspects of list structures are investigated.

Axiomatic theories of lists are closely related to theories of concatenation studied in logic [24, 29]. 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 [9, 13, 14, 30, 32]. In such theories there is no need to develop a coding of finite sequences [13, 24]. 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 Sect. 2, we show the two main results of this article in Sects. 3 and 4. First, in Sect. 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 Sect. 4, we show that for all $m \ge 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 Sect. 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 Sect. 2.3 we introduce some concepts on transfinite sequences, which we will use in the model theoretic constructions of Sects. 3 and 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} \rightarrow o$ and function symbols of the form $f: s_{1} \times \dots \times s_{n} \rightarrow 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} \rightarrow 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} \rightarrow 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 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$, $\lnot$, $\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} \rightarrow s_{n + 1}$ a function ; To each predicate symbol $P: s_{1} \times \dots \times s_{n} \rightarrow o$ a set . 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 Sects. 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 $\textrm{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 ${\textsf {i}}$ of elements and the sort ${\textsf {list}}$ of finite lists. Moreover, the language ${\mathcal {L}}_{0}$ contains the function symbols $nil : {\textsf {list}}$ and ${\textit{cons}}: {\textsf {i}}\times {\textsf {list}}\rightarrow {\textsf {list}}$.

Informally, the symbol $nil$ denotes the empty list and ${\textit{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 ${\textsf {list}}$. For these variables we omit the the sort annotation, that is, the “: ${\textsf {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

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

For a set of formulas $\Phi$, the theory ${\Phi }$ 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 Sect. 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 $nil$ and ${\textit{cons}}$.

Definition 2.3

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

$$\begin{aligned} nil&\ne {\textit{cons}}(x,X), \end{aligned}$$

(L0.1)

$$\begin{aligned} {\textit{cons}}(x,X)&= {\textit{cons}}(y,Y) \rightarrow x = y \wedge X = Y. \end{aligned}$$

(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 Sects. 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 \rightarrow {\mathcal {X}} \}$ of sequences of elements of ${\mathcal {X}}$ with length $\alpha$. If $a \in {\mathcal {X}}^\alpha$ and $\beta < \alpha$ then we write $a_\beta$ for $a(\beta )$, the element of a with index $\beta$. By ${\mathcal {X}}^{<\alpha }$ (${\mathcal {X}}^{\le \alpha }$) we denote the set $\bigcup _{\beta < \alpha }{\mathcal {X}}^{\beta }$ ($\bigcup _{\beta \le \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}}^{\le \alpha }$, then $|a|$ denotes the ordinal $\beta \le \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 \ge \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

$$\begin{aligned} (a \frown b)_{\gamma } :={\left\{ \begin{array}{ll} a_{\gamma } &{} \text {if }\gamma < \alpha \\ b_{\delta } &{} \text {otherwise} \end{array}\right. }, \end{aligned}$$

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

$$\begin{aligned} (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}). \end{aligned}$$

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:

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

• (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

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

If $\alpha \le \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

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

Finally, if $\alpha + \beta \le \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} \ge \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

$$\begin{aligned} (a \frown (b \frown c))_{\mu } = (b \frown c)_{\beta + \delta _{3}} = c_{\delta _{3}} = c_{\delta _{2}} = ((a \frown b) \frown c)_{\mu }. \end{aligned}$$

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$. $\square$

Observe, however, that since 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 \le \alpha$, and $a \in {\mathcal {X}}^{\alpha }$, then the sequence $a \uparrow \beta$ is given by

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

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 Sect. 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

$$\begin{aligned} \lfloor {\mathfrak {a}} \rfloor _{\xi } :={\mathfrak {a}}_{\delta ,\mu }, \end{aligned}$$

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$.

Example 2.8

Let $a = 0,2,4,6,\ldots \in {\mathbb {N}}^\omega$ be the sequence of even numbers and $b = 1,3,5,7,\ldots \in {\mathbb {N}}^\omega$ be the sequence of odd numbers. Then, e.g., $a_0 = 0$, $b_0 = 1$, and $b_1 = 3$. Let ${\mathfrak {a}} = (a,b) \in ({\mathbb {N}}^\omega )^2$. Then, in the notation of Definition 2.7, $\alpha = \omega$, $\beta = 2$, and $\lfloor {\mathfrak {a}} \rfloor = a \frown b = 0,2,4,6,\ldots 1,2,5,7,\ldots \in {\mathbb {N}}^{\omega \cdot 2}$. For, e.g., $\xi = \omega + 3$, we have $\delta = 1$ and $\mu = 3$, so $\lfloor {\mathfrak {a}} \rfloor _\xi = {\mathfrak {a}}_{\delta ,\mu } = b_\mu = 7$. Moreover, $\lfloor {\mathfrak {a}} \rfloor \uparrow 2 = 4,6,8,\ldots 1,3,5,\ldots$ and $\lfloor {\mathfrak {a}} \rfloor \uparrow \omega = b$.

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 \ge 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 ${\textsf {i}}$ and $T$ a term of sort ${\textsf {list}}$, then the term ${\textit{cons}}(t_{1}, \dots , t_{n};T)$ is defined inductively by

$$\begin{aligned}{} & {} {\textit{cons}}(;T) = T, \\{} & {} {\textit{cons}}(t_{1}, \dots , t_{n + 1};T) = {\textit{cons}}(t_{1},\dots ,t_{n},{\textit{cons}}(t_{n+1},T)). \end{aligned}$$

Definition 3.1

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

$$\begin{aligned} \left( \begin{aligned}&\bigwedge _{i = 1, \dots , m} ({\forall }{x_1,\dots ,x_{i-1}}){\varphi }({\textit{cons}}(x_{1}, \dots , x_{i-1}; nil ),\vec {z})\\&\wedge ({\forall }{X}){({\forall }{x_{1}, \dots , x_{m}}){\left( \varphi (X,\vec {z}) \rightarrow \varphi ({\textit{cons}}(x_{1},\dots ,x_{m};X),\vec {z})\right) }} \end{aligned} \right) \rightarrow ({\forall }{X}){\varphi (X,\vec {z})}. \end{aligned}$$

Let $\Phi$ be a set of formulas and $m \ge 1$, then the $m$-step induction schema ${\Phi }\text {-}\textrm{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 \ge 1$ of elements to a list results in a different list:

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 $nil \ne {\textit{cons}}(x_{1},\dots ,x_{n}; nil )$, which follows readily from (L0.1). For the induction step we assume ($\star$. For a contradiction assume

$$\begin{aligned} {\textit{cons}}(x_{1}',\dots ,x_{n}';X) = {\textit{cons}}(x_{1},\dots ,x_{n},x_{1}',\dots ,x_{n}';X). \end{aligned}$$

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

$$\begin{aligned} X = {\textit{cons}}(x_{1}',\dots ,x_{n}';X). \end{aligned}$$

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

Lemma 3.2

The theory $T_{0}+ {\textrm{Open}({\mathcal {L}}_{0})}$ proves

• (i) $X \ne {\textit{cons}}(x_{1},\dots ,x_{n};X)$ for $n \ge 1$;

• (ii) $X = nil \vee ({\exists }{x'}){({\exists }{X'}){X = {\textit{cons}}(x',X')}}$.

Proof

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

$$\begin{aligned} \underbrace{X' \ne X}_{\psi _{1}(X')} \wedge \underbrace{X' \ne {\textit{cons}}(x_{n},X)}_{\psi _{2}(X')} \wedge \dots \wedge \underbrace{X' \ne {\textit{cons}}(x_{2},\dots ,x_{n};X)}_{\psi _{n}(X')}. \end{aligned}$$

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

$$\begin{aligned} {\textit{cons}}(x_{1},\dots ,x_{n};X) \ne X, \end{aligned}$$

which contradicts the first assumption.

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

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 \ge 1$ and $\varphi (X,\vec {z})$ be a formula, then

$$\begin{aligned} \vdash I_{X}{\bigwedge _{i = 1}^{m}({\forall }{x_{1}}){\dots ({\forall }{x_{i-1}}){\varphi ({\textit{cons}}(x_{1},\dots ,x_{i-1};X),\vec {z})}}} \rightarrow I_{X\curvearrowright m}{\varphi (X,\vec {z})}. \end{aligned}$$

Proof

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

Clearly it suffices to show the following formula.

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

Remark 3.4

When the domain of the elements provably consists of a finite number of elements $n \ge 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: {\textsf {list}}\rightarrow o$.

Proposition 3.6

Let $m \ge 2$, then

$$\begin{aligned} T_{0}+ \bigcup _{1\le j < m}{\textrm{Open}({\mathcal {L}}_{A})}\text {-}\textrm{IND}_{\curvearrowright {j}} \not \vdash I_{x\curvearrowright m}{A(x)}. \end{aligned}$$

This proposition entails, in particular, that $T_{0}+ {\textrm{Open}({\mathcal {L}}_{A})} \not \vdash {\textrm{Open}({\mathcal {L}}_{A})}\text {-}\textrm{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 ${\textit{cons}}(x_{1},\dots {\textit{cons}}(x_{n}, 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 \ne {\textit{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 \le i < \omega }$. Now we define

$$\begin{aligned} {\mathcal {N}} :=\{ w \frown N_{k} \mid w \in {\mathbb {N}}^{*}, k \in {\mathbb {N}}\}. \end{aligned}$$

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 \ge 1$, then the structure $M_{1}^{m}$ interprets the sort ${\textsf {i}}$ as the natural numbers and the sort ${\textsf {list}}$ as $M_{1}^{m}({\textsf {list}}) = {\mathbb {N}}^{*} \cup {\mathcal {N}}$. Furthermore, $M_{1}^{m}$ interprets the list constructors as $nil ^{M_{1}^{m}} :=\varepsilon$ and ${\textit{cons}}^{M_{1}^{m}}(n,l) :=(n) \frown l$ and the predicate symbol $A: {\textsf {list}}\rightarrow o$ as

$$\begin{aligned} A^{M_{1}^{m}} :={\mathbb {N}}^{*} \cup \left\{ N \in {\mathcal {N}} \mid w_{N} \ne \varepsilon \text { or } m \not \mid k_{N}\right\} . \end{aligned}$$

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} = {\textit{cons}}(n_{1},\dots ,n_{k};l_{1})$.

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

Lemma 3.9

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

Proof

We start with the axiom (L0.1). We have $nil ^{M_{1}^{m}} = \varepsilon = \varnothing$. Let $n \in {\mathbb {N}}$ and $l \in M_{1}^{m}({\textsf {list}})$, then $(0,n) \in (n) \frown l = {\textit{cons}}^{M_{1}^{m}}(n,l)$. Hence, $nil ^{M_{1}^{m}} \ne {\textit{cons}}^{M_{1}^{m}}(n,l)$ and therefore $M_{1}^{m} \models$ (L0.1). Now let $n_{1}, n_{2} \in {\mathbb {N}}$ and $l_{1}, l_{2} \in M_{1}^{m}({\textsf {list}})$ and assume that ${\textit{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$ (L0.2). $\square$

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 \ge 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 \ge K$ and $m \not \mid 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}({\textsf {list}})$. If $w = \varepsilon$, then we are done by letting $K = 0$. Otherwise, we let $K = (w)_{|w| - 1} + 2$. For $k \ge 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}))$. $\square$

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

Lemma 3.11

Let $m \ge 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| \ge K$ and secondly $M_{1}^{m} \not \models E(N_{k})$ for all $k \ge K$.

Proof

The case where $X \notin Var (E)$ is trivial. Let $E(X)$ be $u(X) = v(X)$. If $X \in Var (u)$ and $Var (v) = \varnothing$, then there is $w \in {\mathbb {N}}^{*}$ and $l' \in M_{1}^{m}({\textsf {list}})$ such that $M_{1}^{m} \models u(l) = w \frown l$ for all $l \in M_{1}^{m}({\textsf {list}})$ and $M_{1}^{m} \models v = l'$. If $|w| > |l'|$, then we are done by letting $K = 0$. Otherwise, if $|w| \le |l'|$ we consider the prefix of $l'$. If $w$ is not a prefix of $l'$, then again we are done by letting $K = 0$. If $w$ is the prefix of $l'$, then $l' = w \frown l^{\prime \prime }$ for some $l^{\prime \prime } \in {\mathbb {N}}^{\le |l'|}$. We have $l^{\prime \prime } \in M_{1}^{m}({\textsf {list}})$, since $M_{1}^{m}({\textsf {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}({\textsf {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}({\textsf {list}})$ with $l_{0} \ne l^{\prime \prime }_{0}$. Hence, it suffices to let $K = l^{\prime \prime }_{0} + 1$.

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

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

Lemma 3.12

Let $m \ge 2$, then $M_{1}^{m} \models \bigcup _{1 \le j < m }{\textrm{Open}({\mathcal {L}}_{A})}\text {-}\textrm{IND}_{\curvearrowright {j}}$.

Proof

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

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

Let $l \in M_{1}^{m}({\textsf {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 ($*$ and ($\star$).

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| \ge K$ and $M_{1}^{m} \not \models E_{i}(N_{k})$ for all $k \ge 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' \ge K$ such that for all $k \in {\mathbb {N}}$ with $k \ge K'$ and $m \not \mid 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| \ge j$), we obtain $K^{\prime \prime } \ge 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 \not \mid 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' \in {\mathbb {N}}^{*}$ with $|w'| \ge K$, then by the above, for $i = 0, \dots , j -1$, we have $M_{1}^{m} \models \psi (w')$ 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')$. In the first part of the proof we have already shown that $M_{1}^{m} \models \varphi (w')$. 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$ we obtain $M_{1}^{m} \models \varphi ( w' \frown (l \uparrow |w| ))$ for all $w' \in {\mathbb {N}}^{*}$. In particular, we have $M_{1}^{m} \models \varphi (l)$. $\square$

Lemma 3.13

Let $m \ge 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

$$\begin{aligned} M_{1}^{m} \models A({\textit{cons}}(x_{1},\dots ,x_{j-1}; nil ))\text { for }j = 1, \dots , m. \end{aligned}$$

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

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

Hence, $M_{1}^{m} \models A(X) \rightarrow A({\textit{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({\textit{cons}}(x_{1},\dots ,x_{m};X))$. However, we also have $N_{0} \not \in A^{M_{1}^{m}}$ because $w_{N_0} = \varepsilon$ and $k_{N_0} = 0$. Hence, $M_{1}^{m} \not \models I_{x\curvearrowright m}{A(x)}$. $\square$

Proof of Proposition 3.6

An immediate consequence of Lemmas 3.9 and 3.12, and Lemma 3.13. $\square$

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 $\textrm{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 \ge 2$, then

$$\begin{aligned} T_{0}+ \bigcup _{1 \le j < m}{\forall _{1}\textrm{Clause}({\mathcal {L}}_{A})}\text {-}\textrm{IND}_{\curvearrowright {j}} \not \vdash I_{x\curvearrowright m}{A(x)}. \end{aligned}$$

This conjecture is particularly interesting for the methods presented in [15, 16, 25]. 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 \ge 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 : {\textsf {list}}\times {\textsf {list}}\rightarrow {\textsf {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

$$\begin{aligned} nil \frown Y&= Y, \end{aligned}$$

(L1.1)

$$\begin{aligned} {\textit{cons}}(x,X) \frown Y&= {\textit{cons}}(x,X \frown Y). \end{aligned}$$

(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}+ {\textrm{Open}({\mathcal {L}}_{1})}$ proves the following formulas

• (i) $X \frown nil = X$,

• (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). $\square$

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

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

Let $\Gamma$ be a set of formulas, then the theory ${\Gamma }$ 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}+ {\textrm{Open}({\mathcal {L}}_{1})}$ proves

$$\begin{aligned} Y \frown {\textit{cons}}(x, nil ) = Z \frown {\textit{cons}}(x, nil ) \rightarrow Y = Z. \end{aligned}$$

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 = nil$ we assume $nil \frown {\textit{cons}}(x, nil ) = Z \frown {\textit{cons}}(x, nil )$ and we have to show that $Z = nil$. First of all, by (L1.1) we obtain ${\textit{cons}}(x, nil ) = Z \frown {\textit{cons}}(x, nil )$. By Lemma 3.2 we can consider two cases. If $Z = nil$, then we are done. Otherwise, there are $z'$ and $Z'$ such that $Z = {\textit{cons}}(z',Z')$. Thus

$$\begin{aligned} {\textit{cons}}(x, nil )&= {\textit{cons}}(z',Z') \frown {\textit{cons}}(x, nil )\\&=_{\mathrm{(L1.2)}} {\textit{cons}}(z',Z' \frown {\textit{cons}}(x, nil )). \end{aligned}$$

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

$$\begin{aligned} Y \frown {\textit{cons}}(x, nil ) = Z \frown {\textit{cons}}(x, nil ). \end{aligned}$$

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

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

$$\begin{aligned} ({\forall }{X}){\left( X = nil \vee ({\exists }{X'}){({\exists }{x'}){X = {\textit{cons}}(x',X')}}\right) }. \end{aligned}$$

Lemma 4.5

$\textrm{CA} + {\forall _{1}({\mathcal {L}})} \vdash {\textrm{Open}({\mathcal {L}})}$.

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, nil ,\vec {z})}$, $({\forall }{Y}){\varphi ( nil ,Y,\vec {z})}$, and

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

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 $\textrm{CA}$ we can consider two cases. If $Y = nil$, then we are done by the assumption. Otherwise, there are $y'$ and $Y'$ such that $Y = {\textit{cons}}(y',Y')$. By the induction hypothesis, we obtain $\varphi (X, Y', \vec {z})$. Hence, by the third assumptions, we have $\varphi ({\textit{cons}}(x,X), {\textit{cons}}(y',Y'), \vec {z})$, that is, $\varphi ({\textit{cons}}(x,X), Y, \vec {z})$. $\square$

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})}$ proves

$$\begin{aligned} Y \frown X = Z \frown X \rightarrow Y = Z. \end{aligned}$$

Proof

We proceed by induction on $X$ in the formula

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

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

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

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

$$\begin{aligned} (Y \frown {\textit{cons}}(x, nil )) \frown X = (Z \frown {\textit{cons}}(x, nil )) \frown X. \end{aligned}$$

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

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

$$\begin{aligned} T_{1}+ \bigcup _{m \in {\mathbb {N}}}{\textrm{Open}({\mathcal {L}}_{1})}\text {-}\textrm{IND}_{\curvearrowright {m+1}} \not \vdash Y \frown X = X \rightarrow Y = nil . \end{aligned}$$

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} \ne \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 Sect. 3 we have already mentioned that, in order to construct a model of $T_{0}+ {\textrm{Open}({\mathcal {L}}_{0})}$ 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 ${\textsf {i}}$ as the set ${\mathbb {N}}$ and the sort ${\textsf {list}}$ as the set ${\mathfrak {L}}$ given by

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

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

$$\begin{aligned}{} & {} nil ^{M_{2}} :=\varepsilon ,\\{} & {} {\textit{cons}}^{M_{2}}(n,l) :=n \frown l,\\{} & {} l_{1} \frown ^{M_{2}} l_{2} :=l_{1} \frown l_{2}. \end{aligned}$$

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 $nil ^{M_{2}}$, ${\textit{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 $nil ^{M_{2}}$, ${\textit{cons}}^{M_{2}}(\cdot ,\cdot )$, and $\cdot \frown ^{M_{2}} \cdot$. We have $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 \le \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

$$\begin{aligned} m_{\gamma }' :={\left\{ \begin{array}{ll} (n) \frown m_{0} &{} \quad \text {if }\gamma = 0,\\ m_{\gamma } &{} \quad \text {otherwise} \end{array}\right. } \end{aligned}$$

Now observe that $(n) \frown \lfloor (m_{\gamma })_{\gamma< \beta } \rfloor = \lfloor ( m'_{\gamma })_{\gamma < \beta } \rfloor$ and clearly $m'_{\gamma } \in {\mathcal {N}}$, for all $\gamma < \beta$. Hence, ${\textit{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 \le \alpha _{2}$ and $w' \frown N_{k} \in {\mathcal {N}}$ such that $1 + \delta = \alpha _{2}$ and $l_{2} = w' \frown N_{k} \frown \lfloor ({\mathfrak {a}}_{2,1 + \gamma })_{\gamma < \delta } \rfloor$. Therefore, we have

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

Since $w_{1} \frown w' \frown N_{k} \in {\mathcal {N}}$ and $\alpha _{1} + \alpha _{2} < \omega ^{2}$ we have $l_{1} \frown l_{2} \in {\mathfrak {L}}$. $\square$

Next we show that $M_{2}$ satisfies the basic axioms of the list constructors $nil$ and ${\textit{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, since every element of ${\mathcal {N}}$ has length $\omega$, there is some ordinal $\alpha < \omega ^{3}$ such that $l \in {\mathbb {N}}^{\alpha }$. Hence, ${\textit{cons}}^{M_{2}}(n,l) \in {\mathbb {N}}^{1 + \alpha }$. Therefore ${\textit{cons}}^{M_{2}}(n,l) \ne nil ^{M_{2}} = \varepsilon = \varnothing$. Thus $M_{2}\models$ (L0.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$ (L0.2). Now let $l \in {\mathfrak {L}}$. We have $nil ^{M_{2}} \frown l = \varepsilon \frown l = l$. Hence, $M_{2}\models$ (L1.1). Now let $n \in {\mathbb {N}}$, $l, l' \in {\mathfrak {L}}$. Then we have

$$\begin{aligned} {\textit{cons}}^{M_{2}}(n,l) \frown ^{M_{2}} l' = ((n) \frown l) \frown l' = (n) \frown (l \frown l') = {\textit{cons}}^{M_{2}}(n,l \frown ^{M_{2}} l'). \end{aligned}$$

Thus, $M_{2}\models$ (L1.2). $\square$

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 ${\textsf {list}}$ terms as follows.

Lemma 4.11

Let $t(X,\vec {y})$ be a ${\mathcal {L}}_{1}$ ${\textsf {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

$$\begin{aligned} 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}. \end{aligned}$$

Proof

We proceed by induction on the structure of the term $t$. If $t$ is $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 ${\textit{cons}}(u,t')$, 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' \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 \dots \frown l_{n' -1}' \frown X \frown l_{n'}'$. Hence,

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

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

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 \ge 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

$$\begin{aligned} 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}. \end{aligned}$$

By the symmetry of equality we can assume $n_{1} \le n_{2}$ without loss of generality. Since $M_{2}\not \models E(X)$ we either have $n_{1} \ne n_{2}$ or $l_{i}^{1} \ne 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

$$\begin{aligned} 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}. \end{aligned}$$

Hence, we have $M_{2}\not \models E((n) \frown l)$, for all $n \in {\mathbb {N}}$ and $l \in {\mathfrak {L}}$. So in this case it suffices to take $N = 0$. Now consider the case where there exists $j \in \{0, \dots , n_{1}\}$ such that $l_{j}^{1} \ne 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 }| \ge 1$, or $|l_{j_{0}}^{1\prime }| \ge 1$, $|l_{j_{0}}^{2\prime }| = 0$, or $|l_{j_{0}}^{1'}| \ge 1$, $|l_{j_{0}}^{2'}| \ge 1$ and $(l_{j_{0}}^{1'})_{0} \ne (l_{j_{0}}^{2'})_{0}$. Hence, by left cancellation of concatenation, we obtain

$$\begin{aligned}{} & {} 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}} \\{} & {} \quad =l_{j_{0}}^{2\prime } \frown X \frown \dots \frown l_{n_{2}-1}^{2} \frown X \frown l_{n_{2}}. \end{aligned}$$

If $l_{j_{0}}^{1'} = \varepsilon$ and $l_{j_{0}}^{2'} \ne \varepsilon$, then for $n \ne (l_{j_{0}}^{2})_{0}$, we have $M_{2}\not \models E((n) \frown l)$ for all $l \in {\mathfrak {L}}$. So in this case we take $N = (l_{j_0}^2)_0 + 1$ The case where $l_{j_{0}}^{1'} \ne \varepsilon$ and $l_{j_{0}}^{2'} = \varepsilon$ is symmetric. Finally, in the case that $l_{j_{0}}^{1'}, l_{j_{0}}^{2'} \ne \varepsilon$ with $(l_{j_{0}}^{1'})_{0} \ne (l_{j_{0}}^{2'})_{0}$, we trivially have $M_{2}\not \models E(l)$ for all $l \in {\mathfrak {L}}$. So it suffices to take $N=0$. $\square$

As an immediate consequence of the previous lemma, we obtain the following result, which essentially says that for a non-standard element $\lambda$ a ${\textsf {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 \ge N$.

Proof

First by applying Lemma 4.12 we obtain $m_{0}$ such that $M \not \models E((m) \frown l)$ for all $m \ge 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 '$ for some $\lambda ' \in {\mathfrak {L}}$. Since $(\lambda \uparrow n_0 + k)_{0} = m_{0} + k \ge m_{0}$ for $k \in {\mathbb {N}}$, we have $M_{2}\not \models E(\lambda \uparrow n)$ for all $n \ge n_{0}$. $\square$

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

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

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

Proof

Clearly, it suffices to consider the ${\textsf {list}}$-equations of $\varphi$, since the ${\textsf {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 \ge n_{0}$ and $i = 1, \dots , k$. Since we have $M_{2} \models E(X)$ for the other ${\textsf {list}}$-atoms of $\varphi$, we obtain $M_{2} \models \varphi (\lambda \uparrow n) \leftrightarrow \varphi ((n))$ for $n \ge n_{0}$. $\square$

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

Proposition 4.15

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

Proof

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

Let $\lambda \in {\mathfrak {L}}$. If $\lambda \in {\mathbb {N}}^{*}$, then a straightforward induction making use of ($*$ and ($\star$ 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 \ge n_{0}$. In particular, we thus have

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

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$ 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 )$. $\square$

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} \ne \varnothing$. Hence, by Proposition 4.15 we are done. $\square$

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 \le i \le 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 \ge 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}}^{{{\textsf {list}}}}\varphi$ for $\varphi$ is given by

$$\begin{aligned}{} & {} \left( \begin{aligned} \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},{\textit{cons}}(x_{1},\dots ,x_{j-1}; 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 ({\textit{cons}}(\vec {x}^{p_{1}};X_{1}), \dots , {\textit{cons}}(\vec {x}^{p_{m}};X_{m}), \vec {z})\right) }}} \end{aligned} \right) \\{} & {} \quad \rightarrow ({\forall }{\vec {X}}){\varphi (\vec {X})}. \end{aligned}$$

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

Conjecture 4.17

$T_{1}+ {\textrm{Open}({\mathcal {L}}_{1})}\text {-}\textrm{IND}^{{{\textsf {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})}$ 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 \ge 1}{\textrm{Open}({\mathcal {L}}_{1})}\text {-}\textrm{IND}_{\curvearrowright {m}}$ does not prove

$$\begin{aligned} X = nil \vee ({\exists }{x'}){({\exists }{X'}){X = X' \frown {\textit{cons}}(x', nil )}}. \end{aligned}$$

Proof

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

Clearly, the formula $X = nil \vee ({\exists }{x'}){({\exists }{X'}){X = X' \frown {\textit{cons}}(x', 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 Sect. 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 [25, 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 Sect. 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 Sect. 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 Sect. 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 Conjecture 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 Sect. 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 [11, 26].