16411 LABEL:LastPageOct. 11, 2019Nov. 30, 2020

# Clause Set Cycles and Induction

Stefan Hetzl  Vienna University of Technology
Institute of Discrete Mathematics and Geometry
<EMAIL_ADDRESS>and  Jannik Vierling

###### Abstract.

In this article we relate a family of methods for automated inductive theorem
proving based on cycle detection in saturation-based provers to well-known
theories of induction. To this end we introduce the notion of clause set
cycles—a formalism abstracting a certain type of cyclic dependency between
clause sets. We first show that the formalism of clause set cycles is
contained in the theory of $\exists_{1}$ induction. Secondly, we consider the
relation between clause set cycles and the theory of open induction. By
providing a finite axiomatization of a theory of triangular numbers with open
induction we show that the formalism of clause set cycles is not contained in
the theory of open induction. Furthermore, we conjecture that open induction
and clause set cycles are incomparable. Finally, we transfer these results to
a concrete method of automated inductive theorem proving called the n-clause
calculus.

###### Key words and phrases:

inductive theorem proving, arithmetical theories, clause logic, cyclic proofs

Supported by the Vienna Science and Technology Fund (WWTF) project VRG12-004

##  1\. Introduction

The subject of automated inductive theorem proving (AITP) aims at automating
the process of finding proofs by mathematical induction. AITP is of paramount
importance to the formal verification of software and hardware. Every non-
trivial program contains loops or recursion, hence its verification requires
some inductive reasoning. But also the development of proof assistants can
benefit from automated inductive theorem proving by providing hammers that can
discharge lemmas automatically.

It is folklore that finding proofs by induction is difficult because of the
necessity of non-analyticity of induction formulas. The non-analyticity of
induction formulas can be explained proof-theoretically by the failure of cut-
elimination in LK with an induction rule, see [HW18] for a precise statement.
A wide variety of approaches have been proposed to address this problem. Among
others there are approaches based on enhancements of saturation-based provers
[Cru17, EP19, KP13], cyclic proofs [BGP12], rippling [BSvH+93], theory
exploration [CJRS13], etc. Most of these approaches are rather technical in
nature and are thus difficult to analyze formally. Hence, most of the analyses
carried out for methods of automated inductive theorem proving are empirical
and little is known about the theoretical properties of these methods. We
believe that providing formal analyses of these methods will contribute to the
theoretical foundations of the subject and thus help in developing better
methods.

The work presented in this article continues the analysis of Kersani and
Peltier’s n-clause calculus started in the second author’s master’s thesis
[Vie18]. In [Vie18] refutations of the n-clause calculus are translated into
proofs of the sequent calculus $\mathsf{LKID}$ introduced in [BS10]. This
translation makes it possible to read off the induction formulas used by the
n-clause calculus. The analysis carried out in [Vie18] operates directly on
the n-clause calculus as originally defined in [KP13] without introducing an
intermediary abstraction. Therefore, the results obtained in [Vie18] are
complicated by inessential technical details. Furthermore, the technicalities
of the n-clause calculus made it difficult to state conjectures clearly. For
instance, the n-clause calculus imposes restrictions on the types of function
symbols. Because of these restrictions it is already difficult to express
simple properties such as for example the associativity of natural numbers. In
this article we extend the previous work by introducing an abstraction called
clause set cycles. This new formalism abstracts the inessential details of the
n-clause calculus, thus, allowing us to carry out a more systematic analysis
and to formulate more general conjectures.

The article is structured as follows. In Section 2 we will define the notion
of clause set cycle and the associated notion of refutability by a clause set
cycle. We will then situate these notions with respect to $\exists_{1}$
induction, and hence show that the formalism is inherently weak. This result
is a generalization of the main theorem (Theorem 6.27) of [Vie18]. In Section
3 we will provide a finite axiomatization for a theory of triangular numbers
with open induction. This result will then serve as the main technical result
in Section 4, where we will show that the notion of refutability by a clause
set cycle is not weaker than open induction. In Section 5 we will show that
the n-clause calculus is indeed a special case of the system of clause set
cycles and transfer the main results of sections 2 and 4 to the n-clause
calculus. We thus answer positively the conjecture of [Vie18] that there
exists a clause set that is refutable by the n-clause calculus, but that is
not refutable with open induction. As a result we situate the power of the
n-clause calculus with respect to the theories of $\exists_{1}$ induction and
open induction.

##  2\. Clause Set Cycles and $\exists_{1}$ Induction

We work in a many-sorted first-order classical logic. By a many-sorted first-
order classical logic we understand a classical first-order logic with a
finite set of sorts $\mathcal{S}$. The sorts represent universes and are
interpreted as pairwise distinct sets. Each function symbol $f$ has a type of
the form $s_{1}\times\dots\times s_{n}\to s_{n+1}$, where
$s_{1},\dots,s_{n},s_{n+1}\in\mathcal{S}$ are sorts and $n\geq 0$.
Analogously, a predicate symbol $P$ has a type of the form
$s_{1}\times\dots\times s_{n}$, again with $s_{1},\dots,s_{n}\in\mathcal{S}$
and $n\geq 0$. Let the sort $s\in\mathcal{S}$ be interpreted as the set
$U_{s}$, then a function symbol $f$ with type as above, will be interpreted as
a function that maps elements of $U_{s_{1}}\times\dots\times U_{s_{n}}$ to
elements of $U_{s_{n+1}}$. Analogously, a predicate symbol $P$ with type as
above is interpreted as a subset of $U_{s_{1}}\times\dots\times U_{s_{n}}$.
Each individual variable ranges over a fixed sort. Whenever the sort of a
variable is clear from the context, we will not mention it explicitly. Terms
and formulas are defined as usual, but function symbols and relation symbols
need to be applied to terms that agree with the type of the symbol.

Every language that we consider is supposed to contain at least the sort ${\rm
Nature}$ representing the natural numbers, with its function symbols
$\mathsf{0}:{\rm Nature}$ representing the number $0$ and $\mathsf{s}:{\rm
Nature}\to{\rm Nature}$ representing the successor function. In case the
language contains only one sort, we specify function symbols by pairs of the
form $f/n$ where $f$ is a function symbol and $n$ is a natural number
representing the arity of the symbol $f$. In the following we fix one such
language and denote it by $L$. Formulas, structures, models, truth, validity,
$\models$, $\vdash$, etc. are defined as usual.

By $\eta$ we denote a distinguished variable ranging over the sort ${\rm
Nature}$. We will call this variable $\eta$ a parameter. The parameter $\eta$
is mainly used to indicate positions on which arguments by induction take
place, that is, the parameter usually plays the role of the induction
variable. Usually the parameter $\eta$ will occur freely, in other words, it
will not be bound by quantifiers and therefore behaves similarly to a
constant. In the literature a similar concept of parameter is used, with the
difference that the parameter is usually a constant (even a Skolem constant).
In our case treating the parameter as a variable seems to be more natural,
especially when dealing with the language of induction formulas.

Let $f$ be a unary function symbol and $t$ a term. In order to save
parentheses we write $ft$ for the term $f(t)$. By $f^{n}t$ we abbreviate the
term

$\underbrace{f(f(\dots f}_{\text{$n$ times}}(t)\dots)).$

Let $n\in\mathbb{N}$, then by $\overline{n}$ we denote the term
$\mathsf{s}^{n}\mathsf{0}$. Let $t,t_{1},\dots,t_{n}$ be terms of sort ${\rm
Nature}$ and $+$ be a function symbol of type ${\rm Nature}\times{\rm
Nature}\to{\rm Nature}$ denoting the addition of natural numbers. For the sake
of readability we will use the symbol $+$ as an infix symbol. The expression
$t_{1}+t_{2}+\dots+t_{n}$ abbreviates the term
$(\dots(t_{1}+t_{2})+\dots)+t_{n}$ and $nt$ denotes the term

$\underbrace{t+t+\cdots+t}_{\text{$n$ times}}.$

[Literal, Clause, Clause set] An $L$ formula $l(\vec{x})$ is called an $L$
literal if it is an atom or the negation of an atom. An $L$ formula
$C(\vec{x})$ is said to be an $L$ clause if it of the form
$\forall\vec{y}\,\bigvee_{i=1}^{k}l_{i}$ where $l_{i}(\vec{x},\vec{y})$ with
$i\in\\{1,\dots,k\\}$ is a literal. An $L$ formula $S(\vec{x})$ is called an
$L$ clause set if it is of the form $\bigwedge_{i=1}^{m}C_{i}$ where $C_{i}$
with $i\in\\{1,\dots,m\\}$ is an $L$ clause. When the language $L$ is clear
from the context we simply say literal, clause, and clause set instead of $L$
literal, $L$ clause, and $L$ clause set.

Let $\varphi$ and $\psi$ be formulas, then by $\varphi\rightarrow\psi$ we
abbreviate the formula $\neg\varphi\vee\psi$. In order to save some
parentheses we use the standard convention that $\rightarrow$ associates to
the right and has a lower precedence than $\neg$, $\vee$, and $\wedge$. For
example, the formulas $\neg\varphi\rightarrow\psi$,
$\varphi\wedge\theta\rightarrow\psi$, $\varphi\rightarrow\theta\vee\psi$ are
to be read as $(\neg\varphi)\rightarrow\psi$,
$(\varphi\wedge\theta)\rightarrow\psi$ and
$\varphi\rightarrow(\theta\vee\psi)$, respectively. For the sake of
readability we will often not distinguish between a clause and an equivalent
formula up to negation normal form. For example if $a_{1},\dots,a_{n}$, and
$b_{1},\dots,b_{m}$ are atoms, then we also call the formula

$(a_{1}\wedge\dots\wedge a_{n})\rightarrow(b_{1}\vee\dots\vee b_{m})$

a clause, because its negation normal form is the clause
$\bigvee_{i=1}^{n}\neg a_{i}\vee\bigvee_{i=1}^{m}b_{i}$. We usually present a
concrete clause set $\bigwedge_{i=1}^{n}C_{i}$ as the list of clauses $C_{1}$,
…, $C_{n}$. Similarly, we will usually present the axioms of a theory as a
list of formulas. We are now ready to define the notion of clause set cycles
and the related notion of refutability by a clause set cycle. An $L$ clause
set $S(\eta)$ is called an $L$ clause set cycle if it satisfies the following
conditions

$\displaystyle S(\mathsf{s}\eta)$ $\displaystyle\models S(\eta),$ (1)
$\displaystyle S(\mathsf{0})$ $\displaystyle\models\bot.$ (2)

Note that clause set cycles do not operate in some background theory. However,
a clause set cycle may contain clauses without free variables and these
clauses act as a background theory. A clause set cycle has a natural
interpretation as an argument by infinite descent, which we will later explain
in terms of induction. Before that, we introduce the notion of refutation by a
clause set cycle. A refutation by a clause set cycle consists of a clause set
cycle and a case distinction. We say that an $L$ clause set $R(\eta)$ is
refuted by an $L$ clause set cycle $S(\eta)$ if there exists a natural number
$n$ such that

$\displaystyle R(\mathsf{s}^{n}\eta)$ $\displaystyle\models S(\eta),$ (3)
$\displaystyle R(\overline{k})$ $\displaystyle\models\bot,\ \text{for all
$k\in\\{0,\dots,n-1\\}$}.$ (4)

If the language is clear from the context we simply speak of clause set cycles
and of clause sets refuted by a clause set cycle. Let us consider an example
in order to clarify the notions of clause set cycle and refutation by a clause
set cycle. Let $\mathsf{P}$ and $\mathsf{Q}$ be unary predicate symbols over
the sort ${\rm Nature}$ and let $R(\eta)$ be the clause set consisting of the
clauses

$\displaystyle\mathsf{Q}(\eta),$ $\displaystyle\neg\mathsf{Q}(\mathsf{0}),$
$\displaystyle\forall x\,(\mathsf{Q}(\mathsf{s}x)\rightarrow\mathsf{P}(x)),$
$\displaystyle\neg\mathsf{P}(\mathsf{0}),$ $\displaystyle\forall
x\,(\mathsf{P}(\mathsf{s}x)\rightarrow\mathsf{P}(x)).$

Our goal is to refute the clause set $R(\eta)$ by a clause set cycle.

First we claim that
$S(\eta)\coloneqq\mathsf{P}(\eta)\wedge\neg\mathsf{P}(\mathsf{0})\wedge\forall
x\,(\mathsf{P}(\mathsf{s}x)\rightarrow\mathsf{P}(x))$ is a clause set cycle.
We start by showing that $S(\mathsf{0})\models\bot$. Observe that
$S(\mathsf{0})=P(\mathsf{0})\wedge\neg P(\mathsf{0})\wedge\forall
x\,(\mathsf{P}(\mathsf{s}x)\rightarrow\mathsf{P}(x))$. Hence we have
$S(\mathsf{0})\models\bot$. It remains to show that $S(\mathsf{s}\eta)\models
S(\eta)$. Since $S(\mathsf{s}\eta)=P(\mathsf{s}\eta)\wedge\neg
P(0)\wedge\forall x\,(\mathsf{P}(\mathsf{s}x)\rightarrow\mathsf{P}(x))$, it
suffices to show that $S(\mathsf{s}\eta)\models\mathsf{P}(\eta)$. We have
$S(\mathsf{s}\eta)\models P(\mathsf{s}\eta)$ and
$S(\mathsf{s}\eta)\models\forall
x\,(\mathsf{P}(\mathsf{s}x)\rightarrow\mathsf{P}(x))$, hence
$S(\mathsf{s}\eta)\models\mathsf{P}(\mathsf{s}\eta)\rightarrow\mathsf{P}(\eta)$
and by modus ponens we obtain $S(\mathsf{s}\eta)\models P(\eta)$. Hence
$S(\eta)$ is a clause set cycle.

Now we claim that $R(\eta)$ is refuted by the clause set cycle $S(\eta)$. It
suffices to show the entailments $R(\mathsf{0})\models\bot$ and
$R(\mathsf{s}\eta)\models S(\eta)$. By definition of $R(\eta)$ we have
$R(\eta)\models\mathsf{Q}(\eta)$ and
$R(\eta)\models\neg\mathsf{Q}(\mathsf{0})$, hence
$R(\mathsf{0})\models\mathsf{Q}(\mathsf{0})$ and
$R(\mathsf{0})\models\neg\mathsf{Q}(\mathsf{0})$. Therefore
$R(\mathsf{0})\models\bot$. For the second entailment we have
$R(\mathsf{s}\eta)\models\mathsf{Q}(\mathsf{s}\eta)$ and
$R(\mathsf{s}\eta)\models\forall
x\,(\mathsf{Q}(\mathsf{s}x)\rightarrow\mathsf{P}(x))$, thus
$R(\mathsf{s}\eta)\models\mathsf{Q}(\mathsf{s}\eta)\rightarrow\mathsf{P}(\eta)$.
Hence $R(\mathsf{s}\eta)\models\mathsf{P}(\eta)$. We thus have
$R(\mathsf{s}\eta)\models S(\eta)$. Hence $R(\eta)$ is refuted by the clause
set cycle $S(\eta)$ as claimed. The cycles introduced in [KP13] by Kersani and
Peltier are parameterized by two natural numbers $i\geq 0$ and $j\geq 1$, that
control the argument by infinite descent. The number $i$—the offset—is the
number at which the argument by infinite descent stops, and $j$—the step—is
the number by which the descent proceeds. Our clause set cycles do not have
such parameters and therefore appear somewhat restrictive. Let us now
demonstrate how to formulate the concepts of step and offset for clause set
cycles. Let $S(\eta)$ be an $L$ clause set and $i,j\in\mathbb{N}$ with $j\geq
1$. We say that $S(\eta)$ is an $L$ clause set cycle with offset $i$ and step
$j$ if

$\displaystyle S(\overline{k+i})$ $\displaystyle\models\bot,\ \text{for
$k=0,\dots,j-1$ and,}$ $\displaystyle S(\mathsf{s}^{i+j}\eta)$
$\displaystyle\models S(\mathsf{s}^{i}\eta).$

An $L$ clause set $R(\eta)$ is refuted by the clause set cycle $S(\eta)$ with
offset $i$ and step $j$ if there exists a natural number $n$ such that

$\displaystyle R(\overline{k})$ $\displaystyle\models\bot,\ \text{for
$k=0,\dots,n-1$},$ $\displaystyle R(\mathsf{s}^{n}\eta)$ $\displaystyle\models
S(\mathsf{s}^{i}\eta).$

We can now show that clause set cycles simulate clause set cycles with offset
and step.

######  Proposition 1.

Let $R(\eta)$ be an $L$ clause set. If $R(\eta)$ is refuted by an $L$ clause
set cycle $S(\eta)$ with offset $i$ and step $j$, then $R(\eta)$ is refuted by
an $L$ clause set cycle.

######  Proof 2.1.

It is straightforward to see that the offset $i$ is inessential, by letting
$T(\eta)\coloneqq S(\mathsf{s}^{i}\eta)$ because the $L$ clause set $T(\eta)$
clearly is a clause set cycle with offset $0$ and step $j$ and refutes
$R(\eta)$ with offset $0$ and step $j$. In order to show that an arbitrary
step $j$ is inessential as well, we let

$U(\eta)\coloneqq\bigvee_{l=0}^{j-1}T(\mathsf{s}^{l}\eta).$

We will show that $U$ is a clause set cycle. To show that $U$ satisfies (1),
it suffices to observe that by the assumption, we have
$T(\overline{k})\models\bot$ for $k=0,\dots,j-1$. Therefore
$U(\mathsf{0})\models\bot$. In order to show that $U$ satisfies (2), we need
to consider two cases. First let $l\in\\{0,\dots,j-2\\}$, then we have
$T(\mathsf{s}^{l+1}\eta)\models T(\mathsf{s}^{l+1}\eta)$, which implies
$T(\mathsf{s}^{l}\mathsf{s}\eta)\models U(\eta)$. Now let $l=j-1$, then we
have $T(\mathsf{s}^{j}\eta)\models T(\eta)$ by the assumption and, thus,
$T(\mathsf{s}^{l}\mathsf{s}\eta)\models U(\eta)$. Therefore, $U$ is a clause
set cycle and $R$ is refuted by $U$.

Clause set cycles thus abstract parameters such as offset and step width and
therefore simplify a formal analysis.

Let $\psi(x,\vec{z})$ be a formula where $x$ is a variable of sort ${\rm
Nature}$, then the structural induction axiom $I_{x}{\psi}$ is defined by

$I_{x}{\psi}\coloneqq\forall\vec{z}\,(\psi(\mathsf{0},\vec{z})\rightarrow\forall
x\,(\psi(x,\vec{z})\rightarrow\psi(\mathsf{s}x,\vec{z}))\rightarrow\forall
x\,\psi(x,\vec{z})).$

By an $\exists_{1}$ formula we understand a formula of the form
$\exists\vec{x}\,\varphi(\vec{x},\vec{y})$, where $\varphi$ is quantifier-
free. The notion of $\forall_{1}$ formulas is defined dually to $\exists_{1}$
formulas. We will now introduce the two theories of induction that are of
interest for the study of the formalism of clause set cycles. The theories
$I\exists_{1}(L)$ and $I\mathrm{Open}(L)$ are given by

$\displaystyle
I\exists_{1}(L)\coloneqq\\{I_{x}{\psi}\mid\text{$\psi(x,\vec{z})$ is an
$\exists_{1}$, $L$ formula with $x:{\rm Nature}$}\\},$ $\displaystyle
I\mathrm{Open}(L)\coloneqq\\{I_{x}{\psi}\mid\text{$\psi(x,\vec{z})$ is a
quantifier-free, $L$ formula with $x:{\rm Nature}$}\\}.$

Whenever the language $L$ is clear from the context or irrelevant, we will
write $I\exists_{1}$, $I\mathrm{Open}$ instead of $I\exists_{1}(L)$,
$I\mathrm{Open}(L)$. Let $\varphi(x)$ be a formula with $x$ of sort ${\rm
Nature}$, then we say that $\varphi$ is inductive if
$\vdash\varphi(\mathsf{0})$ and $\varphi(x)\vdash\varphi(\mathsf{s}x)$.

Let us now consider how the notions of clause set cycles and refutability by a
clause set cycle relate to provability in theories of induction. Let $S(x)$ be
a clause set cycle, then by (1), (2), and by the completeness of first-order
logic, we obtain $\vdash\neg S(\mathsf{0})$ and $\neg S(x)\vdash\neg
S(\mathsf{s}x)$. In other words, the formula $\neg S(x)$ is inductive. Since
$S$ is a clause set, $S$ is logically equivalent to a $\forall_{1}$ formula,
hence $\neg S(x)$ is logically equivalent to an $\exists_{1}$ formula.
Therefore, we have:

######  Proposition 2.

Let $S(x)$ be a clause set cycle, then we have $I\exists_{1}\vdash\neg S(x)$.

Intuitively a refutation by a clause set cycle consists of a clause set cycle
and a case distinction. The case distinction with $n\in\mathbb{N}$ cases can
be formalized as follows:

$C_{n}(x)\coloneqq\left(\bigvee_{i=0}^{n-1}x=\overline{i}\right)\vee\exists
y\,x=\mathsf{s}^{n}(y).$

Since $C_{n}$ is clearly inductive and logically equivalent to an
$\exists_{1}$ formula, the formula $C_{n}$ is provable with $\exists_{1}$
induction. So we have:

######  Lemma 3.

Let $n\in\mathbb{N}$, then $I\exists_{1}\vdash C_{n}$.

Let now $R(x)$ be a clause set refuted by a clause set cycle $S(x)$. Then
there exists a natural number $n\in\mathbb{N}$ such that $R$ and $S$ satisfy
the conditions (3) and (4). We thus have

$\displaystyle\vdash\neg R(\overline{i}),\ i=0,1,\dots,n-1,$ (5)
$\displaystyle\neg S(x)\vdash\neg R(\mathsf{s}^{n}(x)).$ (6)

By the Lemma above we can proceed in $I\exists_{1}$ by case distinction on the
variable $x$. If $x=\overline{i}$, then we obtain $\neg R(x)$ by (5).
Otherwise if $x=\mathsf{s}^{n}(x^{\prime})$ for some $x^{\prime}$, then by
Proposition 2 and (6) we have $\neg R(\mathsf{s}^{n}(x^{\prime}))$, thus $\neg
R(x)$. We therefore obtain:

######  Theorem 4.

If a clause set $R(x)$ is refuted by a clause set cycle, then

$I\exists_{1}\vdash\neg R(x).$

Refutability by a clause set cycle is thus contained in the theory of
$\exists_{1}$ induction. Therefore, methods for AITP that are based on clause
set cycles can not prove statements that require induction on formulas with
two or more quantifier alternations. This limitation is due to clause set
cycles operating on clause sets instead of some larger set of formulas.
Similar limitations may apply to other AITP methods that extend saturation-
based provers by induction mechanisms that involve only clauses.

##  3\. Open Induction and Triangular numbers

In this section we will provide a finite, universal axiomatization of a theory
of triangular numbers with open induction. This finite axiomatization of the
theory of triangular numbers will be used in Section 4, to show that there
exists a clause set that is refutable by a clause set cycle but that is not
refutable by open induction. The result presented in this section is a
generalization of the finite axiomatization for multiplication-free arithmetic
with open induction provided by Shoenfield in [Sho58].

Let $n\in\mathbb{N}$, then by $\triangle_{n}$ we denote the $n$-th triangular
number $\sum_{i=0}^{n}i=n(n+1)/2$. By $L_{\triangleright}$ we denote the one-
sorted first-order language consisting of the function symbols $\mathsf{0}/0$,
$\mathsf{s}/1$, $\mathsf{p}/1$, $+/2$, and the binary predicate symbol
$\triangleright$. The predicate symbol $\triangleright$ will be written in
infix notation. By $T_{\triangleright}$ we denote the theory axiomatized by

$\displaystyle\forall x\,\mathsf{s}x$ $\displaystyle\neq\mathsf{0}.$
($\mathrm{A1}$) $\displaystyle\mathsf{p}\mathsf{0}$
$\displaystyle=\mathsf{0}.$ ($\mathrm{A2}$) $\displaystyle\forall
x\,\mathsf{p}\mathsf{s}x$ $\displaystyle=x.$ ($\mathrm{A3}$)
$\displaystyle\forall x\,x+\mathsf{0}$ $\displaystyle=x.$ ($\mathrm{A4}$)
$\displaystyle\forall x\,\forall y\,x+\mathsf{s}y$
$\displaystyle=\mathsf{s}(x+y).$ ($\mathrm{A5}$) $\displaystyle{\mathsf{0}}$
$\displaystyle\ \triangleright\ {\mathsf{0}}.$ ($\mathrm{A6}$)
$\displaystyle\forall x\,\forall y\,({x}\ \triangleright\ {y}$
$\displaystyle\rightarrow{\mathsf{s}x}\ \triangleright\ {\mathsf{s}x+y}).$
($\mathrm{A7}$) $\displaystyle\forall x\,\forall y\,({\mathsf{s}x}\
\triangleright\ {\mathsf{s}x+y}$ $\displaystyle\rightarrow{x}\ \triangleright\
{y}).$ ($\mathrm{A8}$) $\displaystyle\forall x\,\forall y\,\forall z\,({x}\
\triangleright\ {y}\wedge{x}\ \triangleright\ {z}$ $\displaystyle\rightarrow
y=z).$ ($\mathrm{A9}$)

The standard model for this theory is denoted by
$\mathbb{N}^{\triangleright}$. The model $\mathbb{N}^{\triangleright}$
interprets the symbols $\mathsf{0},\mathsf{s},\mathsf{p},+$ in the natural
way. The predicate symbol $\triangleright$ is interpreted as the graph of the
triangle function i.e. the function associating with each natural number $n$
the triangular number $\triangle_{n}$.

######  Lemma 5.

The theory $T_{\triangleright}+I\mathrm{Open}(L_{\triangleright})$ proves the
following formulas

$\displaystyle\forall x\,(x\neq\mathsf{0}$ $\displaystyle\rightarrow
x=\mathsf{s}\mathsf{p}x).$ ($\mathrm{B1}$) $\displaystyle\forall x\,x+y$
$\displaystyle=y+x.$ ($\mathrm{B2}$) $\displaystyle\forall x\,\forall
y\,\forall z\,(x+y)+z$ $\displaystyle=x+(y+z).$ ($\mathrm{B3}$)
$\displaystyle\forall x\,\forall y\,\forall z\,(x+y=x+z$
$\displaystyle\rightarrow y=z).$ ($\mathrm{B4}$)

The axiom ($\mathrm{A9}$) is not redundant for the axiomatization of the
theory $T_{\triangleright}+I\mathrm{Open}(L_{\triangleright})$. This can be
seen by taking the standard interpretation of the symbols $\mathsf{0}$,
$\mathsf{s}$, $\mathsf{p}$, $+$ and by interpreting $\triangleright$ as the
set $\\{(n,\triangle_{n})\mid n\in\mathbb{N}\\}\cup\\{(n,\triangle_{n}+1)\mid
n\in\mathbb{N}\\}$. By $T_{\triangleright}^{I}$ we denote the theory
$T_{\triangleright}+\mathrm{B1}+\mathrm{B2}+\mathrm{B3}+\mathrm{B4}$. Our
axiomatization of the theory $T_{\triangleright}^{I}$ is not minimal, because
($\mathrm{A3}$) can be derived from the other axioms. Another simple but
important observation is that for every formula $\varphi(y)$ of the language
$L_{\triangleright}$ we have

$T_{\triangleright}^{I}\vdash\varphi(\mathsf{s}\mathsf{p}x)\leftrightarrow(x=\mathsf{0}\wedge\varphi(\mathsf{s}\mathsf{0}))\vee(x\neq\mathsf{0}\wedge\varphi(x)).$
(7)

We will now show that every formula in $T_{\triangleright}^{I}$ is equivalent
to some formula that is “simple” in the following sense. We call a term or a
formula simple if it does not contain the symbol $\mathsf{p}$. In the theory
$T_{\triangleright}^{I}$ simple terms have a convenient equivalent
representation.

######  Lemma 6.

Let $t(x_{1},\dots,x_{n})$ be a simple term, then there exist
$m_{1},\dots,m_{n},k\in\mathbb{N}$ such that $T_{\triangleright}^{I}\vdash
t=m_{1}x_{1}+\dots+m_{n}x_{n}+\overline{k}$.

######  Proof 3.1.

The term $t$ can be rewritten with $\eqref{A:4}$, $\eqref{A:5}$,
$\eqref{B:2}$, and $\eqref{B:3}$ into the form
$m_{1}x_{1}+\dots+m_{n}x_{n}+\overline{k}$.

Whenever we are working in the context of the theory $T_{\triangleright}^{I}$
we will often and implicitly assume that a simple term is of the form
$m_{1}x_{1}+\dots+m_{n}x_{n}+\overline{k}$.

######  Proposition 7.

Let $\varphi$ be a formula, then there exists a simple formula $\psi$ such
that $T_{\triangleright}^{I}\vdash\varphi\leftrightarrow\psi$.

######  Proof 3.2.

We start with an important observation that we shall repeatedly use throughout
the proof. Let $t$ be a term containing the symbol $\mathsf{p}$. Now we work
in the theory $T_{\triangleright}^{I}$. Then by using ($\mathrm{A5}$),
($\mathrm{B3}$), and ($\mathrm{B4}$), it is possible to permute the symbol
$\mathsf{s}$ in the term $\mathsf{s}(t)$ inwards until it is directly above an
occurrence of the symbol $\mathsf{p}$.

The proof consists of three main steps. First, we eliminate occurrences of
$\mathsf{p}$ in the left-hand arguments of triangle atoms. After that, we
eliminate in the resulting formula all occurrences of $\mathsf{p}$ in right-
hand arguments of triangle atoms without introducing $\mathsf{p}$ to left-hand
arguments of triangle atoms. Finally, we eliminate the symbol $\mathsf{p}$
from equational atoms without introducing $\mathsf{p}$ to the triangle atoms.

Let $\psi$ be a formula. We will now show that there exists a formula
$\psi^{\prime}$ such that
$T_{\triangleright}^{I}\vdash\psi\leftrightarrow\psi^{\prime}$ and moreover
$\psi^{\prime}$ does not contain an occurrence of the symbol $\mathsf{p}$ in
the left-hand arguments of triangle atoms. We start by defining a measure on
formulas that will make the argument more apparent. Let us define
$\\#_{1}^{n}(\psi)$ to be the number of triangle atoms in $\psi$ having
exactly $n$ occurrences of $\mathsf{p}$ in their left-hand argument. We
furthermore let

$N_{1}^{\psi}\coloneqq\max\\{n\in\mathbb{N}\mid\\#_{1}^{n}(\psi)\neq 0\\}.$

Now we can define the measure
$\\#_{1}(\psi)\coloneqq(N_{1}^{\psi},\\#_{1}^{N_{1}^{\psi}}(\psi))$. We
proceed by induction on the measure $\\#_{1}(\psi)$ with respect to the
natural order on pairs of natural numbers. If $\\#_{1}(\psi)=(0,m)$ for some
$m\in\mathbb{N}$, then $\psi$ does not contain the symbol $\mathsf{p}$ in the
left-hand side argument of its triangle atoms. Therefore $\psi$ is already the
desired formula. Otherwise if $N_{1}^{\psi}\neq 0$, then
$\\#_{1}(\psi)=(N_{1}^{\psi},\\#_{1}^{N_{1}^{\psi}}(\psi))$ with
$\\#_{1}^{N_{1}^{\psi}}(\psi)\neq 0$. Hence there exists a triangle atom
$\varphi\coloneqq{t_{1}}\,\triangleright\,{t_{2}}$ of $\psi$ having exactly
$N_{1}^{\psi}$ occurrences of $\mathsf{p}$ in its left-hand argument. Let
$\varphi^{\prime}\coloneqq{\mathsf{s}(t_{1})}\,\triangleright\,{\mathsf{s}(t_{1})+t_{2}}$,
then by ($\mathrm{A7}$) and ($\mathrm{A8}$) we have
$T_{\triangleright}^{I}\vdash\varphi\leftrightarrow\varphi^{\prime}$. Obtain a
$T_{\triangleright}^{I}$ equivalent atom $\varphi^{\prime\prime}$ from
$\varphi^{\prime}$ by permuting in the left-hand argument $\mathsf{s}(t_{1})$
the symbol $\mathsf{s}$ inwards, as described above, until it is directly
above an occurrence of $\mathsf{p}$. Now apply (7) to $\varphi^{\prime\prime}$
in order to obtain a $T_{\triangleright}^{I}$ equivalent formula
$\varphi^{\prime\prime\prime}$. Note that $\varphi^{\prime\prime\prime}$ has
four atoms—two equational atoms and two triangle atoms. The triangle atoms
both contain exactly $N_{1}^{\psi}-1$ occurrences of $\mathsf{p}$ in their
left-hand arguments. Let $\psi^{\prime}$ be obtained from $\psi$ by replacing
$\varphi$ by $\varphi^{\prime\prime\prime}$. We then have
$T_{\triangleright}^{I}\vdash\psi^{\prime}\leftrightarrow\psi$. If
$N_{1}^{\psi^{\prime}}=N_{1}^{\psi}$, then by the above we have
$\\#_{1}^{N_{1}^{\psi^{\prime}}}(\psi^{\prime})=\\#_{1}^{N_{1}^{\psi}}(\psi^{\prime})=\\#_{1}^{N_{1}^{\psi}}(\psi)-1$.
Hence, $\\#_{1}(\psi^{\prime})<\\#_{1}(\psi)$. Otherwise we have
$N_{1}^{\psi^{\prime}}<N_{1}^{\psi}$ and therefore
$\\#_{1}(\psi^{\prime})<\\#_{1}(\psi)$. In any case we have
$\\#_{1}(\psi^{\prime})<\\#_{1}(\psi)$, thus we obtain the desired formula by
applying the induction hypothesis to $\psi^{\prime}$.

By the previous step we can now assume that we work with formulas that do not
contain $\mathsf{p}$ in the left-hand arguments of triangle atoms. We will now
eliminate all the occurrences of $\mathsf{p}$ in right hand arguments of
triangle atoms. To accomplish this we proceed as in the first step by defining
$\\#_{2}^{n}(\psi)$, $N_{2}^{\psi}$, and $\\#_{2}(\psi)$ in analogy to
$\\#_{1}^{n}(\psi)$, $N_{1}^{\psi}$, and $\\#_{1}(\psi)$ for a formula $\psi$.
For a formula $\psi$ without $\mathsf{p}$ in the left-hand arguments of
triangle atoms we proceed by induction on $\\#_{2}(\psi)$ as in the first
step. If $N_{2}^{\psi}=0$, then $\psi$ does not contain $\mathsf{p}$ its
triangle atoms. Thus $\psi$ is the desired formula. Otherwise if
$N_{2}^{\psi}\neq 0$, then $\\#_{2}^{N_{2}^{\psi}}(\psi)\neq 0$, that is,
there exists an atom $\varphi\coloneqq{t_{1}}\,\triangleright\,{t_{2}}$ of
$\psi$ with exactly $N_{2}^{\psi}$ occurrences of $\mathsf{p}$ in $t_{2}$. We
let
$\varphi^{\prime}\coloneqq{\mathsf{s}(t_{1})}\,\triangleright\,{\mathsf{s}(t_{1}+t_{2})}$.
Then $T_{\triangleright}^{I}\vdash\varphi\leftrightarrow\varphi^{\prime}$.
Since $t_{1}$ is assumed to be free of $\mathsf{p}$, the term
$\mathsf{s}(t_{1}+t_{2})$ contains $N_{2}^{\psi}$ occurrences of $\mathsf{p}$.
Now we proceed in analogy to the first step by moving the outermost
$\mathsf{s}$ inwards, thus allowing us to eliminate one occurrence of
$\mathsf{p}$ by making use of the equivalence $\eqref{equiv:1}$. We therefore
obtain a formula $\psi^{\prime}$ with
$T_{\triangleright}^{I}\vdash\psi\leftrightarrow\psi^{\prime}$ and
$\\#_{2}(\psi^{\prime})<\\#_{2}(\psi)$.

We can now assume that formulas we work with do not contain $\mathsf{p}$ in
their triangle atoms. It remains to show that we can eliminate the occurrences
of $\mathsf{p}$ from equational atoms without introducing triangle atoms
containing $\mathsf{p}$. Let $\psi$ be a formula, then we define
$\\#_{3}^{n}(\psi)$ to be the number of equational atoms of $\psi$ containing
exactly $n$ occurrences of $\mathsf{p}$. We moreover define $N_{3}^{\psi}$ and
$\\#_{3}(\psi)$ in analogy to $N_{1}^{\psi}$ and $\\#_{1}(\psi)$. The
induction base is again trivial. For the induction step, we have
$N_{3}^{\psi}\neq 0$ and $\\#_{3}^{N_{3}^{\psi}}(\psi)\neq 0$. Therefore there
exists an equational atom $\varphi\coloneqq(t_{1}=t_{2})$ in $\psi$ with
exactly $N_{3}^{\psi}$ occurrences of $\mathsf{p}$. We proceed similarly to
the previous two steps above, by first replacing an the atom $\varphi$ by the
$T_{\triangleright}^{I}$ equivalent atom
$\mathsf{s}(t_{1})=\mathsf{s}(t_{2})$, then moving $s$ inwards, and finally
applying the equivalence (7). Let $\psi^{\prime}$ be the resulting formula. It
is easy to see that this does not introduce triangle atoms containing
$\mathsf{p}$ and moreover we have $\\#_{3}(\psi^{\prime})<\\#_{3}(\psi)$. We
can thus apply the induction hypothesis in order to obtain the desired
formula.

At this point the reader might wonder why the authors chose to include a
function symbol for the predecessor function and go through the technicalities
of eliminating the symbol $\mathsf{p}$ from formulas instead of providing
additional axioms. The idea is to work with purely universal axiomatizations
so that one can in particular apply Herbrand’s theorem. In order to avoid the
symbol $\mathsf{p}$ we would have to include an axiom containing an
existential quantifier such as $\forall x\,\exists y\,((x=\mathsf{0}\wedge
y=\mathsf{0})\vee(x\neq\mathsf{0}\wedge x=\mathsf{s}(y)))$. As a consequence,
we would later run into similar technicalities when dealing with the this
existential quantifier. In fact, the function symbol $\mathsf{p}$ is just a
Skolem function introduced for the axiom given above.

We have now everything at hand to start with the model theoretic
considerations of the theory $T_{\triangleright}^{I}$. In the following we fix
an arbitrary model $\mathcal{M}$ of the theory $T_{\triangleright}^{I}$. Our
aim is to show that $\mathcal{M}$ is also a model of open induction over the
language $L_{\triangleright}$. By $\mathbf{0}$, $\mathbf{S}$, $\mathbf{P}$,
$\boldsymbol{+}$, and $\blacktriangleright$ we denote the respective
interpretations of the symbols $\mathsf{0}$, $\mathsf{s}$, $\mathsf{p}$, $+$,
and $\triangleright$ in the model $\mathcal{M}$. We start with a few simple
observations about the structure of the model $\mathcal{M}$. Let
$a,b\in\mathcal{M}$, then we define $a\prec b$ if there exists $n\geq 1$ such
that $\mathbf{S}^{n}a=b$. Accordingly we define $a\preceq b$ if $a\prec b$ or
$a=b$. We say that $a$ and $b$ are comparable (in symbols $a\sim b$), if
$a\preceq b$ or $b\preceq a$. It is not hard to see that the relation
$\preceq$ is a partial order and that $\sim$ is an equivalence relation. Let
$a$ be an element of $\mathcal{M}$, then by $[a]$ we denote the equivalence
class of $a$ under $\sim$. It is easy to see that $\preceq$ is total on $[a]$.
Hence classes of comparable elements together with $\preceq$ form chains. Let
us now look a bit more closely at these chains. As a simple consequence of
($\mathrm{B4}$) we have $\forall x\,x+\overline{k}\neq x$ for all $k\geq 1$.
Therefore the chains of comparable elements are infinite. Consider now the
class of elements comparable with $\mathbf{0}$ and let $a$ be an element
comparable with $\mathbf{0}$. Then by ($\mathrm{A1}$) we have
$a=\mathbf{S}^{m}\mathbf{0}$ for some natural number $m$, that is,
$\mathbf{0}$ is the least element of this chain. The chain of elements
comparable with $\mathbf{0}$ thus looks as follows:

$\mathbf{0}\prec\mathbf{S}^{1}\mathbf{0}\prec\mathbf{S}^{2}\mathbf{0}\prec\mathbf{S}^{3}\mathbf{0}\prec\dots.$

This chain is isomorphic to the chain of natural numbers with $\leq$ and the
addition. This is why we will call the elements comparable with $\mathbf{0}$,
the standard elements (of $\mathcal{M}$). Elements that do not belong to this
chain are called non-standard elements (of $\mathcal{M}$).

Before we have a look at the structure of a chains of non-standard elements
let us summarize some basic properties of $\mathcal{M}$.

######  Lemma 8.

Let $a,b$ be elements of $\mathcal{M}$

  1. (1)

If $a$ is a non-standard element, then $\mathbf{P}a$ is a non-standard
element.

  2. (2)

If $a$ is a non-standard element and $m\in\mathbb{N}$, then
$a=\mathbf{S}^{m}\mathbf{P}^{m}a$.

  3. (3)

The element $a\boldsymbol{+}b$ is a standard element if and only if $a$ and
$b$ are standard elements.

######  Proof 3.3.

For (1) let $a$ be a non-standard element of $\mathcal{M}$, then
$a\neq\mathbf{0}$. Thus by ($\mathrm{B1}$) the element $\mathbf{P}a$ is also a
non-standard element.

For (2) if $a$ is non-standard, then $a\neq 0$ and by ($\mathrm{B1}$) we have
$a=\mathbf{S}\mathbf{P}a$. By (1) the element $\mathbf{P}a$ is non-standard,
so we have $\mathbf{P}=\mathbf{S}\mathbf{P}(\mathbf{P}a)$ thus
$a=\mathbf{S}^{2}\mathbf{P}^{2}a$ and so on.

For (3) consider now an element of the form $a\boldsymbol{+}b$. If $a$ and $b$
are both standard elements, then it is clear that $a\boldsymbol{+}b$ is a
standard element. Now suppose that $a\boldsymbol{+}b$ is a standard element
and suppose without loss of generality that $a$ is not a standard element.
Then there exists $m\in\mathbb{N}$ such that
$\mathbf{S}^{m}\mathbf{0}=a\boldsymbol{+}b=b\boldsymbol{+}a=b\boldsymbol{+}\mathbf{S}^{m+1}\mathbf{P}^{m+1}a$.
By ($\mathrm{A3}$) we obtain $\mathbf{0}=\mathbf{S}\mathbf{P}^{m+1}a$ which
contradicts ($\mathrm{A1}$). Hence $a$ must also be a standard element.

Let us now consider the chain of elements comparable with a non-standard
element $a$ of $\mathcal{M}$. Let $n,m$ be natural numbers with $n<k$, then by
Lemma 8 we have $\mathbf{S}^{n}\mathbf{P}^{k}a=\mathbf{P}^{k-n}a$. Hence we
have $\mathbf{P}^{k}a\prec\mathbf{P}^{k-n}a$. Let $b$ be comparable with $a$,
then either $a=\mathbf{S}^{m}b$ or $b=\mathbf{S}^{m}a$ i.e.
$b=\mathbf{P}^{m}a$ or $b=\mathbf{S}^{m}a$ for some natural number $m$. The
chain thus has the following structure:

$\dots\prec\mathbf{P}^{3}a\prec\mathbf{P}^{2}a\prec\mathbf{P}^{1}a\prec
a\prec\mathbf{S}^{1}a\prec\mathbf{S}^{2}a\prec\mathbf{S}^{3}a\prec\dots.$

The chain of elements comparable with $a$ is isomorphic to the integers with
the order $<$.

We define the language $L_{\triangleright}(\mathcal{M})$ to be the extension
of the language $L_{\triangleright}$ by a constant symbol $a$ for every
element $a$ of $\mathcal{M}$. We let the $L_{\triangleright}$ structure
$\mathcal{M}$ interpret $L_{\triangleright}(\mathcal{M})$ formulas by
interpreting for every element $a$ of $\mathcal{M}$ the constant $a$ as
itself. The language $L_{\triangleright}(\mathcal{M})$ will be especially
convenient when we need to insert elements of $\mathcal{M}$ into
$L_{\triangleright}$ terms and $L_{\triangleright}$ formulas. Let $\varphi(x)$
be an $L_{\triangleright}(\mathcal{M})$ formula. We call an element $a$ of
$\mathcal{M}$ a solution of $\varphi$ if $\varphi(a)$ is true in
$\mathcal{M}$. Similarly we call $\varphi$ valid in $\mathcal{M}$ if
$\varphi(a)$ is true in $\mathcal{M}$ for all elements $a$ of $\mathcal{M}$.
In the following we will show the crucial observation that simple atomic
formulas are either valid in $\mathcal{M}$ or have only finitely many pairwise
comparable solutions.

######  Proposition 9.

Let $\varphi(x,\vec{y})$ be a simple atomic formula, $\vec{b}$ a vector of
elements of $\mathcal{M}$, then either $\varphi(x,\vec{b})$ is valid in
$\mathcal{M}$ or $\varphi(x,\vec{b})$ has only finitely many pairwise
comparable solutions.

######  Proof 3.4.

Depending on the form of $\varphi$ we need to distinguish between two cases.
If $\varphi$ is of the form $s=t$, then clearly $\varphi(x,\vec{b})$ is
equivalent in $\mathcal{M}$ to $mx+c=nx+d$ for some $c,d\in\mathcal{M}$. The
claim then follows from Lemma 1 in [Sho58]. If $\varphi$ is of the form
${s}\,\triangleright\,{t}$, then $\varphi(x,\vec{b})$ is equivalent in
$\mathcal{M}$ to ${mx+c}\ \blacktriangleright{nx+d}$ for some
$n,m\in\mathbb{N}$ and $c,d\in\mathcal{M}$. We need to consider two cases:

  * •

For $m=0$, we assume that there are at least two comparable solutions $e$ and
$\mathbf{S}^{p}e$ of $\varphi(x,\vec{b})$ with $p>0$. We have ${c}\
\blacktriangleright{ne+d}$ and ${c}\ \blacktriangleright{n\mathbf{S}^{p}e+d}$.
Therefore by ($\mathrm{A9}$) we have $ne+d=n\mathbf{S}^{p}e+d$. By
($\mathrm{B2}$) and ($\mathrm{A5}$) we obtain
$ne+d=\mathbf{S}^{np}\mathbf{0}\boldsymbol{+}ne+d$. By ($\mathrm{B4}$) we then
have $\mathbf{0}=\mathbf{S}^{np}\mathbf{0}$. Hence we clearly have $n=0$. Thus
$ne+d=d$, and therefore ${c}\ \blacktriangleright{d}$ is true in
$\mathcal{M}$. Because of that ${c}\ \blacktriangleright{nx+d}$ is valid in
$\mathcal{M}$.

  * •

For $m>0$, we will show that there are at most two comparable solutions of
$\varphi(x,\vec{b})$. We proceed indirectly and assume that there are at least
three pairwise comparable solutions $e$, $\mathbf{S}^{p_{1}}e$, and
$\mathbf{S}^{p_{2}}e$ of $\varphi(x,\vec{b})$ with $0<p_{1}<p_{2}$. Since $e$
is a solution we have ${me\boldsymbol{+}c}\
\blacktriangleright{ne\boldsymbol{+}d}$. Let $i\in\\{1,2\\}$, then iterating
($\mathrm{A7}$) and straightforward rewriting we have

${\mathbf{S}^{p_{i}m}(me+c)}\
\blacktriangleright{\mathbf{S}^{\triangle_{p_{i}m}}\mathbf{0}+p_{i}m(me+c)+ne+d}.$

Since $\mathbf{S}^{p_{i}}e$ is a solution of $\varphi(x,\vec{b})$ we have
${m(\mathbf{S}^{p_{i}}e)+c}\ \blacktriangleright{n(\mathbf{S}^{p_{i}}e)+d}$.
Therefore by ($\mathrm{A5}$), ($\mathrm{A9}$), ($\mathrm{B2}$) and
($\mathrm{B4}$) we obtain

$\mathbf{S}^{\triangle_{p_{i}m}}\mathbf{0}+p_{i}m(me+c)=\mathbf{S}^{np_{i}}\mathbf{0}.$

Thus the element $me+c$ is a standard element of $\mathcal{M}$. Therefore
there exists $k\in\mathbb{N}$ such that $me+c=\mathbf{S}^{k}\mathbf{0}$. We
thus have
$\mathbf{S}^{\triangle_{p_{i}m}}\mathbf{0}+p_{i}m\mathbf{S}^{k}\mathbf{0}=\mathbf{S}^{np_{i}}\mathbf{0}$.
Hence by ($\mathrm{A1}$) and because $\mathbf{S}$ is injective we obtain

$\triangle_{p_{i}m}+p_{i}mk=np_{i}.$

Hence $m^{2}p_{1}+m+2mk=2n=m^{2}p_{2}+m+2mk$. But since $m\neq 0$, this
contradicts the assumption that $p_{1}<p_{2}$.

We are now ready to show that $\mathcal{M}$ is a model of open induction over
the language $L_{\triangleright}$. The proof is analogous to the proof given
in [Sho58]. For the sake of completeness we outline the main steps of the
proof.

######  Theorem 10.

Let $\mathcal{M}$ be a model of $T_{\triangleright}^{I}$, then $\mathcal{M}$
is a model of $I\mathrm{Open}(L_{\triangleright})$.

######  Proof 3.5.

Let $\theta(x,\vec{z})$ be a quantifier-free $L_{\triangleright}$ formula. We
have to show that $\mathcal{M}\models I_{x}{\theta(x,\vec{z})}$. By
Proposition 7 we can assume without loss of generality that $\theta$ is a
simple formula. Let $\vec{b}$ be a vector of elements of $\mathcal{M}$ and let
$\theta^{\prime}(x)\coloneqq\theta(x,\vec{b})$. Assume that
$\theta^{\prime}(\mathbf{0})$ is true in $\mathcal{M}$ and
$\theta^{\prime}(x)\rightarrow\theta^{\prime}(\mathbf{S}(x))$ is valid in
$\mathcal{M}$. Let $a$ be an arbitrary element of $\mathcal{M}$. If $a$ is a
standard element, then $a=\mathbf{S}^{m}\mathbf{0}$ for some natural number
$m$. So by applying the induction step repeatedly, starting with
$\theta^{\prime}(\mathbf{0})$, we obtain $\theta^{\prime}(a)$.

Now let us consider the case when $a$ is non-standard. Consider the atoms from
which $\theta^{\prime}(x)$ is built. By Proposition 9 there are two types of
atoms: those that are valid in $\mathcal{M}$, and those that have at most
finitely many (two) pairwise comparable solutions. Valid atoms are true in
$\mathcal{M}$ regardless of the choice of $x$, so we need to consider only the
remaining atoms. By successively letting $x$ be $a$, $\mathbf{P}^{1}a$,
$\mathbf{P}^{2}a$, and so on, we will eventually exhaust all the solutions
($\preceq a$) of any invalid atom of $\theta^{\prime}(x)$. In other words, by
choosing $n\in\mathbb{N}$ large enough, the element $\mathbf{P}^{n}a$
falsifies all the invalid atoms. The same technique works for standard
elements, starting at $\mathbf{0}$ and successively considering
$\mathbf{S}^{1}\mathbf{0}$, $\mathbf{S}^{2}\mathbf{0}$, and so forth. Now by
taking $m\in\mathbb{N}$ large enough so that both $\mathbf{P}^{m}a$ and
$\mathbf{S}^{m}\mathbf{0}$ falsify all the invalid atoms, we observe that
$\theta^{\prime}(\mathbf{S}^{m}\mathbf{0})$ and
$\theta^{\prime}(\mathbf{P}^{m}a)$ have the same truth value in $\mathcal{M}$.
Therefore, since $\theta^{\prime}(\mathbf{S}^{m}\mathbf{0})$ is true in
$\mathcal{M}$, also $\theta^{\prime}(\mathbf{P}^{m}a)$ is true. Since
$\mathbf{S}^{m}\mathbf{P}^{m}a=a$, we can simply apply the induction step $m$
times to find that $\theta^{\prime}(a)$ is true in $\mathcal{M}$.

The finite, universal axiomatizability of
$T_{\triangleright}+I\mathrm{Open}(L_{\triangleright})$ now follows
immediately from Theorem 10, completeness of first-order logic, and from Lemma
5.

######  Theorem 11.

Let $\varphi$ be a formula, then
$T_{\triangleright}+I\mathrm{Open}(L_{\triangleright})\vdash\varphi$ if and
only if $T_{\triangleright}^{I}\vdash\varphi$.

##  4\. Clause Set Cycles and Open Induction

In Section 2 we have shown that refutability by a clause set cycle is
contained in the theory of $\exists_{1}$ induction. The next obvious question
to ask is whether refutability by a clause set cycle is also contained in the
theory of open induction. In this section we will provide a negative answer to
that question by making use of the finite axiomatizability of the theory of
triangular numbers with open induction shown in Section 3. In order to provide
such a negative answer it suffices to provide a clause set which is refutable
by a clause set cycle, but that is not refutable by open induction. A
candidate clause set is readily found. We denote by $S_{\triangleright}(\eta)$
the clause set consisting of the clauses ($\mathrm{A4}$) – ($\mathrm{A7}$) and
the clause $\forall y\,\neg{\eta}\,\triangleright\,{y}$. Let us denote by
$L_{\triangleright}^{\prime}$ the language of the clause set
$S_{\triangleright}$. The clause set $S_{\triangleright}$ expresses that the
triangle function is not total.

######  Lemma 12.

The clause set $S_{\triangleright}(\eta)$ is refutable by a clause set cycle.

######  Proof 4.1.

By the soundness of first-order logic it suffices to show that

$\displaystyle S_{\triangleright}(\mathsf{0})\vdash\bot,$ (8) and
$\displaystyle S_{\triangleright}(\mathsf{s}(\eta))\vdash
S_{\triangleright}(\eta).$ (9)

For (8) we have
$S_{\triangleright}(\mathsf{0})\vdash{\mathsf{0}}\,\triangleright\,{\mathsf{0}}$
and $S_{\triangleright}(\mathsf{0})\vdash\forall
y\,\neg{\mathsf{0}}\,\triangleright\,{y}$. Hence
$S_{\triangleright}(\mathsf{0})\vdash\bot$. For (4.2) we assume
$S_{\triangleright}(\mathsf{s}(\eta))$. The clauses of $S_{\triangleright}$
not having free variables occur in $S_{\triangleright}(\mathsf{s}(\eta))$,
hence we only need to show that
$S_{\triangleright}(\mathsf{s}(\eta))\vdash\forall
y\,\neg{\eta}\,\triangleright\,{y}$. Let $y$ be arbitrary, then obtain
$S_{\triangleright}(\mathsf{s}(\eta))\vdash\neg{\mathsf{s}(\eta)}\,\triangleright\,{\mathsf{s}(\eta)+y}$.
By the contrapositive of ($\mathrm{A7}$) we have
$\neg{\eta}\,\triangleright\,{y}$. Therefore the clause set
$S_{\triangleright}$ is a clause set cycle. Since a clause set cycle is
trivially refuted by itself, we are done.

It now remains to show that $S_{\triangleright}$ cannot be refuted by open
induction. In order to be able to make use of Theorem 11, we will now
reformulate the clause set $S_{\triangleright}$ in terms of a theory of
triangular numbers. In the following we denote by
$T_{\triangleright}^{\prime}$ the theory axiomatized by the formulas
($\mathrm{A4}$) – ($\mathrm{A7}$).

######  Lemma 13.

$I\mathrm{Open}(L_{\triangleright}^{\prime})\vdash\neg
S_{\triangleright}(\eta)$ if and only if
$T_{\triangleright}^{\prime}+I\mathrm{Open}(L_{\triangleright}^{\prime})\vdash\forall
x\,\exists y\,{x}\,\triangleright\,{y}$.

######  Proof 4.2.

We have the following chain of equivalences.

$\displaystyle I\mathrm{Open}(L_{\triangleright}^{\prime})\vdash\neg
S_{\triangleright}(\eta)$ $\displaystyle\Leftrightarrow
I\mathrm{Open}(L_{\triangleright}^{\prime})\vdash\neg(\eqref{A:4}\wedge\dots\wedge\eqref{A:7:1}\wedge\forall
y\,\neg{\eta}\,\triangleright\,{y})$ $\displaystyle\Leftrightarrow
I\mathrm{Open}(L_{\triangleright}^{\prime})\vdash\neg(\eqref{A:4}\wedge\dots\wedge\eqref{A:7:1}\wedge\neg\exists
y\,{\eta}\,\triangleright\,{y})$ $\displaystyle\Leftrightarrow
I\mathrm{Open}(L_{\triangleright}^{\prime})\vdash\eqref{A:4}\wedge\dots\wedge\eqref{A:7:1}\rightarrow\exists
y\,{\eta}\,\triangleright\,{y}$ $\displaystyle\Leftrightarrow
I\mathrm{Open}(L_{\triangleright}^{\prime})\vdash\eqref{A:4}\wedge\dots\wedge\eqref{A:7:1}\rightarrow\forall
x\,\exists y\,{x}\,\triangleright\,{y}$

By the deduction theorem we thus have
$I\mathrm{Open}(L_{\triangleright}^{\prime})\vdash\neg
S_{\triangleright}(\eta)$ if and only if
$T_{\triangleright}^{\prime}+I\mathrm{Open}(L_{\triangleright}^{\prime})\vdash\forall
x\,\exists y\,{x}\,\triangleright\,{y}$.

In order to complete the negative answer it clearly suffices to show that
$T_{\triangleright}+I\mathrm{Open}(L_{\triangleright})\not\vdash\forall
x\,\exists y\,{x}\,\triangleright\,{y}$.

######  Proposition 14.

$T_{\triangleright}+I\mathrm{Open}(L_{\triangleright})\not\vdash\forall
x\,\exists y\,{x}\,\triangleright\,{y}$.

######  Proof 4.3.

We proceed indirectly and assume that
$T_{\triangleright}+I\mathrm{Open}(L_{\triangleright})\vdash\forall x\,\exists
y\,{x}\,\triangleright\,{y}$. By Theorem 11 we then also have
$T_{\triangleright}^{I}\vdash\forall x\,\exists y\,{x}\,\triangleright\,{y}$.
Since $T_{\triangleright}^{I}$ is a universal theory we can apply Herbrand’s
theorem to obtain terms $t_{1}(x),\dots,t_{k}(x)$ such that

$T_{\triangleright}^{I}\vdash\bigvee_{i=1}^{k}{x}\,\triangleright\,{t_{i}(x)}.$

Clearly $\mathbb{N}^{\triangleright}$ is a model of $T_{\triangleright}^{I}$
and the triangle function $\triangleright^{\mathbb{N}^{\triangleright}}$ is
quadratic. Since the terms $t_{i}(x)$, with $i=1,\dots,k$ describe linear
functions in $\mathbb{N}^{\triangleright}$, there exists $m\in\mathbb{N}$ such
that

$\mathbb{N}^{\triangleright}\not\models\bigvee_{i=1}^{k}{\overline{m}}\,\triangleright\,{t_{i}(\overline{m})}.$

Contradiction!

We would like to point out that it seems possible to obtain the result of
Proposition 14 by an alternative argument that relies on an interpretation of
the theory $T_{\triangleright}+I\mathrm{Open}(L_{\triangleright})$ in the
subtheory $I\Delta_{0}$ of Peano arithmetic. The idea is to interpret
individuals of $T_{\triangleright}+I\mathrm{Open}(L_{\triangleright})$ as
“unary” numbers, that is, finite sequences of “1”s. In particular $\mathsf{0}$
would be interpreted as the empty sequence, $\mathsf{s}$ as the function that
appends a “1” to a finite sequence, $+$ as the function that concatenates two
finite sequences, and $\triangleright$ as a $\Delta_{0}$ formula that defines
the graph of the “unary” triangle function. Since $I\Delta_{0}$ codes finite
sequences the translation outlined above is indeed an interpretation. By
Parikh’s theorem the provably total functions of $I\Delta_{0}$ on “unary”
elements have a linear growth rate, whereas the “unary” triangle function has
a quadratic growth rate. Hence, the translation of $\forall x\,\exists
y\,{x}\,\triangleright\,{y}$ is not provable in $I\Delta_{0}$ and therefore
the formula $\forall x\,\exists y\,{x}\,\triangleright\,{y}$ is not provable
in $T_{\triangleright}+I\mathrm{Open}(L_{\triangleright})$. All the notions
necessary to develop the argument outlined above can be found in standard
textbooks on first-order arithmetic such as [HP17].

######  Corollary 15.

The clause set $S_{\triangleright}(\eta)$ is refutable by a clause set cycle
and $I\mathrm{Open}(L_{\triangleright}^{\prime})\not\vdash\neg
S_{\triangleright}(\eta)$.

To summarize we thus have shown the following theorem.

######  Theorem 16.

There exists a language $L$, and an $L$ clause set $S(x)$ refutable by clause
set cycles such that $I\mathrm{Open}(L)\not\vdash\neg S(x)$.

Since refutability by a clause set cycle is not contained in open induction,
the next obvious question to ask is whether every clause set that is refutable
with open induction is also refutable by a clause set cycle. We believe that
this is not the case. Intuitively, this can be explained by the following two
points: first clause set cycles do not allow for any free variables and
secondly clause set cycles only allow for existential quantification. These
two shortcomings of clause set cycles can be demonstrated by the following
example. We assume the usual right recursive definition of the addition from
which we want to prove the sentence $\varphi\equiv\forall x\,x+(x+x)=(x+x)+x$.
To prove $\varphi$ with open induction, we first prove by open induction on
the variable $y$ the inductive formula $\psi(x)\equiv\forall
y\,x+(x+y)=(x+x)+y$. The “lemma” $\psi$ can now be used to prove $\varphi$ by
instantiating the universally quantified variable $y$ by $x$. In this example
both ideas mentioned above came into play, that is, the “lemma” $\psi$
contains a free variable and it contains a universal quantifier that is
actually used to prove $\varphi$.

######  Conjecture 17.

There exists a language $L$, and an $L$ clause set $S(x)$ such that
$I\mathrm{Open}(L)\vdash\neg S(x)$ but $S(x)$ is not refutable by a clause set
cycle.

##  5\. The $n$-Clause Calculus: A Case Study

In this section we will use the notion of clause set cycle in order to derive
results about a concrete approach for AITP—the n-clause calculus. The n-clause
calculus is a formalism for AITP that was introduced by Kersani and Peltier in
[KP13]. This calculus enhances the superposition calculus [BG94], [NR01]—a
refinement of resolution-paramodulation calculi—by a cycle detection
mechanism. This mechanism detects a certain type of cyclic dependencies
between the clauses that are derived during the saturation process. Such a
cyclic dependency represents an argument by infinite descent and, therefore,
represents an unsatisfiable subset of the derived clauses. Once such a cycle
is detected the refutation is terminated. The n-clause calculus operates on a
syntactically restricted fragment of the logical formalism presented in
Section 2. The languages in this section are assumed to contain at least one
other sort, say $\iota$, besides the sort ${\rm Nature}$ of natural numbers.
Furthermore, the languages should not contain any other function symbols of
range ${\rm Nature}$ besides $\mathsf{0}$ and $\mathsf{s}$. By an n-clause we
understand a clause of the form $\forall\vec{x}\,(N(\eta,\vec{x})\vee
C(\vec{x}))$, where $N(\eta,\vec{x})$ is a disjunction of literals of the form
$\eta\neq t(\vec{x})$ and $C$ is a disjunction of literals of the form
$t\bowtie s$ where $\bowtie\ \in\\{=,\neq\\}$, and $t,s$ are terms of sort
other than ${\rm Nature}$. The formula $N$ is called the constraint part of
the n-clause. An n-clause set is a conjunction of n-clauses. For the sake of
readability we will sometimes identify an n-clause set with the set of its
conjuncts. The notion of “cycles” of the n-clause calculus is based on the
descent operator $\downarrow_{j}$ with $j\in\mathbb{N}$. Let $i\in\mathbb{N}$,
and $\mathcal{C}=\forall\vec{x}\,(N(\eta,\vec{x})\vee C(\vec{x}))$ an n-clause
with $N=\bigvee_{j=1}^{k}\eta\neq t_{j}$. Then we define
$\mathcal{C}{\downarrow_{i}}\coloneqq\forall\vec{x}\,(N(\eta,\vec{x}){\downarrow_{i}}\vee
C(\vec{x}))$ where
$N{\downarrow_{i}}\coloneqq\bigvee_{j=1}^{k}\eta\neq\mathsf{s}^{i}(t_{j})$.
For an n-clause set $S=\bigwedge_{j=1}^{m}\mathcal{C}_{j}$ we define
$S{\downarrow_{i}}\coloneqq\bigwedge_{j=1}^{m}\mathcal{C}_{j}{\downarrow_{i}}$.
Intuitively, the $\downarrow_{j}$ operation allows us to express that $\eta$
is replaced by its $j$-th predecessor. The following lemma states a crucial
property of the $\downarrow_{j}$ operator.

######  Lemma 18.

Let $S(\eta)$ be clause set and $j\geq 0$, then we have
$S{\downarrow_{j}}(\mathsf{s}^{j}\eta)\vdash S(\eta)$.

The converse of the above entailment does not hold. However it holds in a
theory that provides at least the injectivity of the successor function.

######  Lemma 19.

Let $S(\eta)$ be a clause set and $j\geq 0$, then

$\forall x\,\forall y\,(\mathsf{s}x=\mathsf{s}y\rightarrow x=y),S(\eta)\vdash
S{\downarrow_{j}}(\mathsf{s}^{j}\eta).$

We can now introduce the notions of cycle and of refutability by a cycle. For
the sake of brevity we consider a simplified variant of the n-clause calculus
defined in [KP13]. Only one of the simplifications imposed by us restricts the
power of the formalism. The cycles presented in [KP13] rely on a decidable
entailment relation $\sqsupseteq$ between clauses such that
$\mathcal{C}\sqsupseteq\mathcal{D}$ implies
$\mathcal{C}\models_{{\mathrm{KP}}}\mathcal{D}$, where $\models_{\mathrm{KP}}$
is the entailment for the “Kersani-Peltier” standard semantics as presented in
[KP13]. Whenever the original formalism requires
$\mathcal{C}\sqsupseteq\mathcal{D}$, we require that
$\mathcal{C}\models\mathcal{D}$. On the one hand the relation $\models$ is not
decidable, but on the other hand the relation $\models$ allows us to use the
completeness of first-order logic. The latter would not be possible with
$\sqsupseteq$ because this relation relies on standard semantics for which the
completeness theorem does not hold. According to [KP13] the relation
$\sqsupseteq$ is intended to abstract decidable relations such as syntactic
equality or subsumption that also satisfy our stronger requirement. Hence our
restriction does not rule out any practically relevant instance of the
n-clause calculus. Finally, our restriction does not limit the generality of
Corollary 23 below, since a similar argument could be used, assuming a
suitable choice of $\sqsupseteq$. Let $R(\eta)$ be an n-clause set. A triple
$(i,j,S(\eta))$ with $i,j\in\mathbb{N}$, $j>0$ and $S\subseteq R$ is a cycle
for $R$ if $S\vdash\eta\neq\overline{k}$ for $k=i,\dots,i+j-1$ and $S\vdash
S{\downarrow_{j}}$. We say that $R$ is refuted by a cycle if there exists a
cycle $(i,j,S)$ for $R$ and $R\vdash\eta\neq\overline{k}$, for
$k=0,\dots,i-1$. A cycle $(i,j,S(\eta))$ for a clause set $R(\eta)$ is similar
to an argument by induction with an offset $i$ and a step with $j$.
Accordingly, the conditions $S\vdash n\neq\overline{k}$ for $k=i,\dots,i+j-1$
correspond to the $j$ base cases, whereas the condition $S\vdash
S{\downarrow_{j}}$ corresponds to the step case.

Cycles of the n-clause calculus are thus structurally similar to clause set
cycles. As announced in Section 1 we will show that clause set cycles are an
abstraction of the cycles of the n-clause calculus. In order to show that
every n-clause set refutable by a cycle is also refuted by a clause set cycle
it essentially remains to show that the argument by induction with offset $i$
and step $j$ can be turned into an argument by structural induction.

######  Proposition 20.

Let $R$ be an n-clause set refuted by a cycle, then $R$ is refuted by a clause
set cycle.

######  Proof 5.1.

Let $(i,j,S(\eta))$ be a cycle refuting $R$. Consider the formula

$T(\eta)\coloneqq\bigvee_{k=0}^{j-1}S(\mathsf{s}^{k+i}\eta).$

It is not difficult to see that $T(\eta)$ is logically equivalent to a clause.
Since $S$ is a cycle, we have $S(\eta)\vdash\eta\neq\overline{i+k}$ for
$k=0,\dots,j-1$. Therefore by instantiating $\eta$ by $\overline{i+k}$ we
obtain $S(\overline{i+k})\vdash\bot$ for $k=0,\dots,j-1$. Hence we have
$T(\mathsf{0})\vdash\bot$.

Let $k\in\\{0,\dots,j-2\\}$, then we clearly have
$S(\mathsf{s}^{k+i+1}\eta)\vdash T(\eta)$. Now let $k=j-1$. Since $S$ is a
cycle, we have $S\vdash S{\downarrow_{j}}$. Thus by Lemma 18 we obtain
$S(\mathsf{s}^{i+j}\eta)\vdash S(\mathsf{s}^{i}\eta)$. Therefore
$T(\mathsf{s}\eta)\vdash T(\eta)$. Thus, by the soundness of first-order logic
$T(\eta)$ is a clause set cycle. Since $S\subseteq R$ we have $R\vdash S$ and
therefore $R(\mathsf{s}^{i}\eta)\vdash T(\eta)$. Now let $k=0,\dots,i-1$, then
since $R\vdash n\neq\overline{k}$ we have $R(\overline{k})\vdash\bot$.
Therefore, by the soundness of first-order logic $R$ is refuted by the clause
set cycle $T$.

By the above proposition the notion of refutation of an n-clause set by a
cycle is also not stronger than $\exists_{1}$ induction. In the following we
will show that an analogue of Theorem 16 also holds for the n-clause calculus.
Let $L$ be the language consisting of the two sorts ${\rm Nature}$, $\iota$,
the function symbols $\mathsf{0}:{\rm Nature}$, $\mathsf{s}:{\rm
Nature}\to{\rm Nature}$, $+:{\rm Nature}\times\iota\to\iota$, $c:\iota$, and
the predicate symbol $\triangleright:{\rm Nature}\times\iota$. We will again
use the predicate symbol $\triangleright$ as an infix symbol. Let $S(\eta)$ be
the $L$ n-clause set consisting of the following n-clauses.

$\displaystyle\mathsf{0}\ $ $\displaystyle\triangleright\ c,$ (C1)
$\displaystyle\forall x\,\forall y\,({x}\,\triangleright\,{y}$
$\displaystyle\rightarrow{\mathsf{s}(x)}\,\triangleright\,{\mathsf{s}(x)+y}),$
(C2) $\displaystyle\forall x\,\forall y\,(\eta=x$
$\displaystyle\rightarrow\neg{x}\,\triangleright\,{y}).$ (C3)

######  Lemma 21.

The n-clause set $S(\eta)$ is refuted by a cycle.

######  Proof 5.2.

By resolving the clauses (C1) and (C3), we obtain $S\vdash\eta\neq\mathsf{0}$.
Resolving the clauses (C2) and (C3) yields
$\eta=\mathsf{s}(x)\rightarrow\neg{x}\,\triangleright\,{y}$. Hence we have
$S\vdash S{\downarrow_{1}}$. Thus the triple $(0,1,S(\eta))$ is a cycle for
$S(\eta)$. Therefore $S(\eta)$ is refuted by a cycle.

Let us now investigate whether $S(\eta)$ can be refuted by open induction.

######  Proposition 22.

$I\mathrm{Open}(L)\not\vdash\neg S(\eta)$.

######  Proof 5.3.

Assume that $I\mathrm{Open}(L)\vdash\neg S(\eta)$. Let $L^{\prime}$ be the
one-sorted language obtained from $L$ by replacing the sort $\iota$ by the
sort ${\rm Nature}$. We then have $I\mathrm{Open}(L^{\prime})\vdash\neg
S(\eta)$. By replacing the constant $c$ by $\mathsf{0}$, we obtain

$I\mathrm{Open}(L_{\triangleright}^{\prime})\vdash\neg S[c/\mathsf{0}](\eta).$

This implies $I\mathrm{Open}(L_{\triangleright}^{\prime})\vdash\neg
S_{\triangleright}(\eta)$, thus, contradicting Corollary 15.

By Lemma 21 and Proposition 22 we thus have:

######  Corollary 23.

There exists a language $L$ and an $L$ n-clause set $S(\eta)$ refuted by a
cycle such that $I\mathrm{Open}\not\vdash\neg S(\eta)$.

##  6\. Conclusion

We have introduced the concept of clause set cycles and the notion of
refutability by a clause set cycle. Clause set cycles abstract the analogous
concepts of cycle and refutability by a cycle of the n-clause calculus. The
main advantage of clause set cycles is their semantic nature, which makes them
independent of any inference system. This independence of an inference system
allows for a more general analysis of the properties of this type of cycle.

We have explained clause set cycles in terms of theories of induction. We
first have shown that refutability by a clause set cycle is contained in the
theory of $\exists_{1}$ induction. On the other hand refutation by a clause
set cycle is not contained in the theory of open induction and we even
conjecture that open induction is incomparable with the refutability by a
clause set cycle. Finally, we have transferred these results to the n-clause
calculus. The results allow us to formally situate the strength of a variant
of the n-clause calculus with respect to induction, where we formerly only had
empirical evidence. The formal results described in this article improve our
understanding of the strength of the approaches for AITP based on clause set
cycles and help to direct further research.

As mentioned in the introduction, the analysis of clause set cycles is part of
a research program which aims at studying methods for automated inductive
theorem proving in order to improve the theoretical foundations of this
subject. One of the next questions to consider is how clause set cycles can be
extended to handle multiple parameters, how this extension would impact the
power of the formalism, and how the addition of parameters can be explained
from the perspective of induction. Another question to consider is how the
enhancement of superposition by structural induction presented by Cruanes in
[Cru17] is related to clause set cycles. A further topic of interest are
approaches to AITP based on cyclic sequent calculi such as the calculus
introduced by Brotherston and Simpson in [BS10]. For instance the inductive
theorem prover “Cyclist” [BGP12] is based on the cut-free fragment of this
cyclic calculus. Recently Das [Das20] has shown that in the context of
arithmetic the logical consequences of cyclic proofs containing only
$\Sigma_{n}$ formulas are contained in the theory $I\Sigma_{n+1}$. In the
setting of arithmetic this result already gives us an upper bound for provers
such as “Cyclist”, however this bound may be improved by taking into account
the cut-freeness of the proofs output by “Cyclist”.

## Acknowledgments

The authors would like to thank the anonymous reviewers whose insightful
feedback has helped to improve this paper.

## References

  * [BG94] Leo Bachmair and Harald Ganzinger.  Rewrite-based Equational Theorem Proving with Selection and Simplification.  Journal of Logic and Computation, 4(3):217–247, 06 1994.
  * [BGP12] James Brotherston, Nikos Gorogiannis, and Rasmus L. 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 Berlin Heidelberg, 2012.
  * [BS10] James Brotherston and Alex Simpson.  Sequent calculi for induction and infinite descent.  Journal of Logic and Computation, 21(6):1177–1216, 10 2010.
  * [BSvH+93] Alan Bundy, Andrew Stevens, Frank van Harmelen, Andrew Ireland, and Alan Smaill.  Rippling: A heuristic for guiding inductive proofs.  Artificial Intelligence, 62(2):185 – 253, 1993.
  * [CJRS13] 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 Berlin Heidelberg, 2013.
  * [Cru17] 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 International Publishing, 2017.
  * [Das20] Anupam Das.  On the logical complexity of cyclic arithmetic.  Logical Methods in Computer Science, Volume 16, Issue 1, January 2020.
  * [EP19] M. Echenim and N. Peltier.  Combining induction and saturation-based theorem proving.  Journal of Automated Reasoning, pages 1–42, Mar 2019.
  * [HP17] Petr Hájek and Pavel Pudlák.  Metamathematics of first-order arithmetic, volume 3.  Cambridge University Press, 2017.
  * [HW18] Stefan Hetzl and Tin Lok Wong.  Some observations on the logical foundations of inductive theorem proving.  Logical Methods in Computer Science, Volume 13, Issue 4, April 2018.
  * [KP13] 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 Berlin Heidelberg, 2013.
  * [NR01] Robert Nieuwenhuis and Albert Rubio.  Chapter 7 - paramodulation-based theorem proving.  In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, Handbook of Automated Reasoning, pages 371 – 443. North-Holland, Amsterdam, 2001.
  * [Sho58] J. R. Shoenfield.  Open sentences and the induction axiom.  Journal of Symbolic Logic, 23(1):7–12, 1958.
  * [Vie18] Jannik Vierling.  Cyclic superposition and induction.  Master’s thesis, Technische Universität Wien, Austria, 2018.

AITP

    automated inductive theorem proving
  *[AITP]: automated inductive theorem proving