# Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs

Stefano Berardi, Makoto Tatsuta

► To cite this version:

Stefano Berardi, Makoto Tatsuta. Intuitionistic Podelski-Rybalchenko Theorem and Equivalence Between Inductive Definitions and Cyclic Proofs. 14th International Workshop on Coalgebraic Methods in Computer Science (CMCS), Apr 2018, Thessaloniki, Greece. pp.13-33, 10.1007/978-3-030-00389-0_3. hal-02044649

HAL Id: hal-02044649

https://inria.hal.science/hal-02044649

Submitted on 21 Feb 2019

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Intuitionistic Podelski-Rybalchenko Theorem and Equivalence between Inductive Definitions and Cyclic Proofs

Stefano Berardi¹ and Makoto Tatsuta²

¹ Università di Torino, Italy
stefano@di.unito.it

² National Institute of Informatics / Sokendai, Japan
tatsuta@nii.ac.jp

**Abstract.** A cyclic proof system gives us another way of representing inductive and coinductive definitions and efficient proof search. Podelski-Rybalchenko termination theorem is important for program termination analysis. This paper first shows that Heyting arithmetic HA proves Kleene-Brouwer theorem for induction and Podelski-Rybalchenko theorem for induction. Then by using this theorem this paper proves the equivalence between the provability of the intuitionistic cyclic proof system and that of the intuitionistic system of Martin-Löf's inductive definitions when both systems contain HA.

## 1 Introduction

This paper studies two subjects: intuitionistic Podelski-Rybalchenko theorem for induction, and equivalence between intuitionistic system of Martin-Löf's inductive definitions and an intuitionistic cyclic proof system.

Podelski-Rybalchenko theorem [20] states that if a transition invariant is a finite union of well-founded relations then the transition invariant is also well-founded. This gives us good sufficient conditions for analysis of program termination [20]. Intuitionistic provability of this theorem is also interesting; if we can show this theorem is provable in some intuitionistic logical system, the theorem also gives us not only termination but also an upper bound of computation steps of a given program. For this purpose, we have to replace well-foundedness in the theorem by induction principle, since well-foundedness is a property of negation of existence and induction principle can show a property of existence. We say *Podelski-Rybalchenko theorem for induction* when we replace well-foundedness by induction principle in Podelski-Rybalchenko theorem. [3] shows Podelski-Rybalchenko theorem for induction is provable in intuitionistic second-order logic. [5] shows that this theorem for induction is provable in Peano arithmetic, by using the fact that Peano arithmetic can formalize Ramsey theorem. However until now it was not known whether Podelski-Rybalchenko theorem for induction is provable in some intuitionistic first-order logic. This paper will show this theorem for induction is provable in Heyting arithmetic and answer this question.
An inductive/coinductive definition is a way to define a predicate by an expression which may contain the predicate itself. The predicate is interpreted by the least/greatest fixed point of the defining equation. Inductive/coinductive definitions are important in computer science, since they can define useful recursive data structures such as lists, trees, and streams, and useful notions such as bisimulations. Inductive definitions are important also in mathematical logic, since they increase the proof theoretic strength. Martin-Löf's system of inductive definitions given in [18] is one of the most popular systems of inductive definitions. This system has production rules for an inductive predicate, and the production rule determines the introduction rules and the elimination rules for the predicate.

[8, 11] proposed an alternative formalization of inductive definitions, called a *cyclic proof system*. A proof, called a *cyclic proof*, is defined by proof search, going upwardly in a proof figure. If we encounter the same sequent (called a *bud*) as some sequent we already passed (called a *companion*) we can stop. The induction rule is replaced by a case rule, for this purpose. The soundness is guaranteed by some additional condition, called a *global trace condition*, which can show the case rule decreases some measure of a bud from that of the companion. In general, for proof search, a cyclic proof system can find an induction formula in a more efficient way than Martin-Löf's system, since a cyclic proof system does not have to choose fixed induction formulas in advance. A cyclic proof system enables us to get efficient implementation of theorem provers with inductive definitions [7, 9, 10, 12]. A cyclic proof system can also give us another logical system for coinductive predicates, since a coinductive predicate is a dual of an inductive predicate, and sequent calculus is symmetric for this dual.

[8, 11] investigated Martin-Löf's system **LKID** of inductive definitions in classical logic for the first-order language, and the cyclic proof system **CLKID**<sup>ω</sup> for the same language, showed the provability of **CLKID**<sup>ω</sup> includes that of **LKID**, and conjectured the equivalence.

As the second subject, this paper studies the equivalence for intuitionistic logic, namely, the provability of the intuitionistic cyclic proof system, called **CLJID**<sup>ω</sup>, is the same as that of the intuitionistic system of Martin-Lof's inductive definitions, called **LJID**. This question is theoretically interesting, and answers will potentially give new techniques of theorem proving by cyclic proofs to type theories with inductive/coinductive types and program extraction by constructive proofs.

This paper first points out that the countermodel of [4] also shows the equivalence is false in general. Then this paper shows the equivalence is true under arithmetic, namely, the provability of **CLJID**<sup>ω</sup> is the same as that of **LJID**, when both systems contain Heyting arithmetic **HA**.

There are not papers that study the equivalence for intuitionistic logic or Kleene-Brouwer theorem for induction in intuitionistic first-order logic. For Podelski-Rybalchenko theorem for induction, [3] intuitionistically showed it but the paper used second-order logic.
Section 2 proves Kleene-Brouwer theorem for induction and Podelski-Rybalchenko theorem for induction. Section 3 defines LJID and CLJID<sup>ω</sup> and discuss a cyclic proof system for streams. Section 4 discusses the countermodel, defines CLJID<sup>ω</sup> + HA and LJID + HA, states the equivalence theorem, and explains ideas of the equivalence proof. Section 5 discusses proof transformation and proves the equivalence theorem. Section 6 discusses related work. We conclude in Section 7.

## 2 HA-Provable Podelski-Rybalchenko Theorem for Induction

This section will prove Podelski-Rybalchenko theorem for induction, inside Heyting arithmetic HA. First we will prove Kleene-Brouwer theorem for induction, inside HA. This is done by carefully using some double induction. This theorem is new. Next we will show induction for the set MS of monotonically-colored subsequences. Monotonically-colored subsequences are used in ordinary proof of Ramsey theorem and we will show some intuitionistic property of them. Then by applying Kleene-Brouwer theorem to a part of MS and some orders ><sub>u,Left</sub> and ><sub>u,Right</sub>, we will obtain two Kleene-Brouwer relations ><sub>KB1,r</sub> and ><sub>KB2,r</sub> and show their induction principle. These two relations are simple but necessary preparation for the next relation. Then by applying Kleene-Brouwer theorem to some lifted tree determined by ><sub>KB2,r</sub> and the relation ><sub>KB1,r</sub>, we will obtain a Kleene-Brouwer relation ><sub>KB,r</sub> and show its induction principle. This relation is a key of the proof. Then we will show that induction for decreasing transitive sequences is reduced to induction for Erdös trees with the relation ><sub>KB,r</sub>. An Erdös tree is some set of monotonically-colored sequences and implicitly used in ordinary proof of Ramsey theorem. Since Erdös trees are in the lifted tree, by combining them, finally we will prove Podelski-Rybalchenko theorem for induction.

### 2.1 Kleene-Brouwer Theorem

We will show Kleene-Brouwer theorem for induction, which states that if we have both induction principle for a lifted tree (namely ⟨u⟩ * T for some tree T) with respect to the one-step extension relation and induction principle for relations on children, then we have induction principle for the Kleene-Brouwer relation. We can prove it by refining an ordinary proof of Kleene-Brouwer theorem for orders.

We assume Heyting arithmetic HA is defined in an ordinary way with constants and function symbols 0, s, +, ×. We define x < y by ∃z.x + sz = y and x ≤ y by x = y ∨ x < y. We can assume some coding of a sequence of numbers by a number in Heyting arithmetic, because the definitions on pages 115–117 of [21] work also in HA. We write ⟨t<sub>0</sub>, ..., t<sub>n</sub>⟩ for the sequence of t<sub>0</sub>, ..., t<sub>n</sub>. We also write |t|, and (t)<sub>u</sub> for the length of the sequence t, and the u-th element of the sequence t respectively. We write * for the concatenation operation of sequences.
We write $>R$ or $>$ for a binary relation. We write $<_R$ for the binary relation of the inverse of $>R$. For notational simplicity, we say $X$ is a set in order to say there is some first-order formula $Fx$ such that $x \in X \leftrightarrow Fx$. Then we also say $t \in X$ in order to say $Ft$. We write $y <_R x \in X$ for $y <_R x \land y \in X$. We write $x \in \sigma$ when $x$ is an element of the sequence $\sigma$. We write $U^{<\omega}$ for the set of finite sequences of elements in $U$. For a set $S$ of sequences, we write $\langle u \rangle * S$ for $\{\langle u \rangle * \sigma \mid \sigma \in S\}$. For a set $U$ and a binary relation $>R$ for $U$, the induction principle for $(U, >_R)$ is defined as

$$ \begin{aligned} \mathrm{Ind}(U, >_R, F) &\equiv \forall x \in U((\forall y <_R x \in U.Fy) \rightarrow Fx) \rightarrow \forall x \in U.Fx, \\ \mathrm{Ind}(U, >_R) &\equiv \mathrm{Ind}(U, >_R, F) \quad (\text{for every formula } Fx). \end{aligned} $$

For a set $U$ a set $T$ is called a tree of $U$ if $T \subseteq U^{<\omega}$ and $T$ is nonempty and closed under prefix operations. Note that the empty sequence is a prefix of any sequence. As a graph, the set of nodes is $T$ and the set of edges is $\{(x, y) \in T^2 \mid y = x * \langle u \rangle\}$. We call a set $T \subseteq U^{<\omega}$ a lifted tree of $U$ when there are a tree $T' \subseteq U^{<\omega}$ and $r \in U$ such that $T = \langle r \rangle * T'$. We define LiftedTree($T, U$) as a first-order formula that means $T$ is a lifted tree of $U$.

For $x, y \in U^{<\omega}$ we define the one-step extension relation $x >_{\mathrm{ext}} y$ if $y = x * \langle u \rangle$ for some $u$. For a set $T \subseteq U^{<\omega}$ and $\sigma \in U^{<\omega}$, we define $T_\sigma$ as $\{\rho \in T \mid \rho = \sigma * \rho'\}$. Note that $T_\sigma$ is a subset of $T$. For a nonempty sequence $\sigma$, we define first($\sigma$) and last($\sigma$) as the first and the last element of $\sigma$ respectively.

The next lemma shows induction implies $x \not\supseteq x$. The proof is in [6].

**Lemma 2.1** If $\mathbf{HA} \vdash \mathrm{Ind}(U, >)$, then $\mathbf{HA} \vdash \forall x, y \in U(y < x \rightarrow y \neq x)$.

**Definition 2.2 (Kleene-Brouwer Relation)** For a set $U$, a lifted tree $T$ of $U$, and a set of binary relations $>u$ on $U$ for every $u \in U$, we define the Kleene-Brouwer relation $>_{\mathrm{KB}}$ for $T$ and $\{(>u) \mid u \in U\}$ as follows: for $x, y \in T$, $x >_{\mathrm{KB}} y$ if (1) $x = z * \langle u, u_1 \rangle * w_1$, $y = z * \langle u, u_2 \rangle * w_2$, and $u_1 >_u u_2$ for some $z, u, u_1, w_1, u_2, w_2$, or (2) $y = x * z$ for some $z \neq \langle \rangle$.

When $(>u)$ is some fixed $(>)$ for all $u$, for simplicity we call the relation $(>_{\mathrm{KB}})$ the Kleene-Brouwer relation for $T$ and $>$.

Note that $(>_{\mathrm{KB}})$ is a relation on $T$. This Kleene-Brouwer relation is slightly different from ordinary Kleene-Brouwer order for the following points: it creates a relation instead of an order, it uses a set of relations indexed by an element, and it is defined for a lifted tree instead of a tree (in order to use indexed relations).

The next theorem shows induction principle for the Kleene-Brouwer relation.

**Theorem 2.3 (Kleene-Brouwer Theorem for Induction)** If $\mathbf{HA} \vdash \mathrm{LiftedTree}(T, U)$, $\mathbf{HA} \vdash \mathrm{Ind}(T, >_{\mathrm{ext}})$ and $\mathbf{HA} \vdash \forall u \in U.\mathrm{Ind}(U, >_u)$, then $\mathbf{HA} \vdash \mathrm{Ind}(T, >_{\mathrm{KB}})$.

*Proof.* By induction on $(T, >_{\mathrm{ext}})$ with the induction principle $\mathrm{Ind}(T, >_{\mathrm{ext}})$, we will show $\forall \sigma \in T.\mathrm{Ind}(T_\sigma, >_{\mathrm{KB}})$. After we prove it, we can take $\sigma$ to be $\langle \rangle$ to show the theorem, since $T_\sigma = T$.
Fix $\sigma \in T$ in order to show Ind($T_\sigma$, $>_{KB}$). Note that we can use induction hypothesis for every $\sigma * \langle u \rangle \in T$:

$$ \mathrm{Ind}(T_{\sigma*\langle u \rangle}, >_{KB}). \qquad (1) $$

Assume

$$ \forall x \in T_{\sigma}((\forall y <_{KB} x \in T_{\sigma}.Fy) \rightarrow Fx) \qquad (2) $$

in order to show $\forall x \in T_\sigma.Fx$. For simplicity we write $F(X)$ for $\forall x \in X.Fx$. Let $Gu \equiv F(T_{\sigma*\langle u \rangle})$. By Ind($U$, $>_{last(\sigma)}$) we will show the following claim.

Claim: $\forall u \in U.Gu$.

Fix $u \in U$ in order to show $Gu$.

By IH for $v$ with $>_{last(\sigma)}$ we have

$$ v <_{last(\sigma)} u \rightarrow F(T_{\sigma*\langle v \rangle}). \qquad (3) $$

We can show

$$ \forall x \in T_{\sigma*\langle u \rangle}((\forall y <_{KB} x \in T_{\sigma*\langle u \rangle}.Fy) \rightarrow (\forall y <_{KB} x \in T_{\sigma}.Fy)) \qquad (4) $$

as follows. Fix $x \in T_{\sigma*\langle u \rangle}$, assume

$$ \forall y <_{KB} x \in T_{\sigma*\langle u \rangle}.Fy \qquad (5) $$

and assume $y <_{KB} x \in T_\sigma$ in order to show $Fy$. By definition of $>_{KB}$, we have $y \in T_{\sigma*\langle v \rangle}$ for some $v <_{last(\sigma)} u$, or $y \in T_{\sigma*\langle u \rangle}$. In the first case, $Fy$ by (3). In the second case, $Fy$ by (5). Hence we have shown (4).

Combining (4) with (2), we have

$$ \forall x \in T_{\sigma*\langle u \rangle}((\forall y <_{KB} x \in T_{\sigma*\langle u \rangle}.Fy) \rightarrow F(x)). \qquad (6) $$

By IH (1) for $\sigma * \langle u \rangle$, we have Ind($T_{\sigma*\langle u \rangle}$, $>_{KB}$), namely,

$$ \forall x \in T_{\sigma*\langle u \rangle}((\forall y <_{KB} x \in T_{\sigma*\langle u \rangle}.Fy) \rightarrow Fx) \rightarrow \forall x \in T_{\sigma*\langle u \rangle}.Fx. \qquad (7) $$

By (7)(6), $F(T_{\sigma*\langle u \rangle})$. Hence we have shown the claim.

If $y <_{KB} \sigma \in T_\sigma$, we have $y \in T_{\sigma*\langle u \rangle}$ for some $u$, since $y <_{KB} \sigma$ implies $y \neq \sigma$ by definition of KB and Lemma 2.1 for $>u$. By the claim, $Fy$. Hence

$$ \forall y <_{KB} \sigma \in T_{\sigma}.Fy. \qquad (8) $$

By letting $x := \sigma$ in (2), we have $(\forall y <_{KB} \sigma \in T_\sigma.Fy) \rightarrow F\sigma$. By (8), $F\sigma$. Combining it with the claim, $\forall x \in T_\sigma.Fx$. $\square$

## 2.2 Proof Ideas for Podelski-Rybalchenko Theorem for Induction

In this subsection we will explain proof ideas of Theorem 2.15.

A sequence $u_1 >_R u_2 >_R u_3 >_R \dots$ is called *transitive* when $u_i >_R u_j$ for any $i < j$. We say the edge from $u$ to $v$ is of color $R$ when $u >_R v$. A sequence is called *monotonically-colored* when for any element there is a color such that the edge from the element to any element after it in the sequence has the same color.
**Definition 2.4** For a set $U$ and a relation $>$ for $U$, we define the set $\text{DS}(U, >)$ of decreasing sequences as $\{\langle x_0, \dots, x_{n-1} \rangle \mid n \ge 0, x_i \in U, \forall i < n - 1. (x_i > x_{i+1})\}$.

We define the set $\text{DT}(U, >)$ of decreasing transitive sequences by $\{\langle x_0, \dots, x_{n-1} \rangle \mid n \ge 0, x_i \in U, \forall i (\forall j \le n - 1. (i < j \rightarrow x_i > x_j))\}$.

We define $>_{R_1 \cup \dots \cup R_k}$ as the union of $>_{R_i}$ for all $1 \le i \le k$. We define $>_{R_1+\dots+R_k}$ as the disjoint union of $>_{R_i}$ for all $1 \le i \le k$. (Whenever we use it, we implicitly assume the disjointness is provable in **HA**.)

We define $\text{Monoseq}_{R_1, \dots, R_k}(x)$ to hold when $x = \langle x_0, \dots, x_{n-1} \rangle \in \text{DT}(U, >_{R_1+\dots+R_k})$ and $\forall i < n - 1. (\forall j \le n - 1. (i < j \rightarrow \bigwedge_{1 \le l \le k} (x_i >_{R_l} x_{i+1} \rightarrow x_i >_{R_l} x_j)))$. Note that $n$ may be 0.

We define $\text{MS}$ as $\{x \in \text{DT}(U, >_{R_1+\dots+R_k}) \mid \text{Monoseq}_{R_1, \dots, R_k}(x)\}$.

$\text{MS}$ is the set of monotonically-colored finite sequences. Note that $\text{MS}_{\langle r \rangle}$ is a subset of $\text{MS}$ (by taking $T$ and $\sigma$ to be $\text{MS}$ and $\langle r \rangle$ in our notation $T_\sigma$) and a lifted tree of $U$ for any $r \in U$.

We will show Podelski-Rybalchenko theorem for induction stating that if a transition invariant $>_{\Pi}$ is a finite union of relations $>_{\pi}$ such that each $\text{Ind}(>_{\pi}^n)$ is provable for some $n$, and each $(>_{\pi})$ is decidable, then $\text{Ind}(>_{\Pi})$ is provable.

First each $\text{Ind}(>_{\pi})$ is obtained by $\text{Ind}(>_{\pi}^n)$. Next by the decidability of each $(>_{\pi})$, we can assume all of $(>_{\pi})$ are disjoint to each other. For simplicity, we explain the idea of our proof for well-foundedness instead of induction principle.

Assume the relation $>_{\Pi}$ has some infinite decreasing transitive sequence

$$u_1 >_{\Pi} u_2 >_{\Pi} u_3 >_{\Pi} \dots$$

in order to show contradiction.

The set $\text{MS}$ will be shown to be well-founded with the one-step extension relation. For a decreasing transitive sequence $x$ of $U$, a lifted tree $T \in U^{<\omega}$ is called an Erdös tree of $x$ when the elements of $x$ are the same as elements of $T$, every element of $T$ is monotonically-colored, and the edges from a parent to its children have different colors. Let $\text{ET}$ be a function that returns an Erdös tree of a given decreasing transitive sequence. Then we consider

$$\text{ET}(\langle u_1 \rangle), \text{ET}(\langle u_1, u_2 \rangle), \text{ET}(\langle u_1, u_2, u_3 \rangle), \dots$$

Define $\text{MS}_{\langle r \rangle}$ as the set of sequences beginning with $r$ in $\text{MS}$. Define $>_{\text{KB}_1,r}$ as the Kleene-Brouwer relation for the lifted tree $\text{MS}_{\langle r \rangle}$ and some left-to-right-decreasing relation on children of the lifted tree. Define $>_{\text{KB}_2,r}$ as the Kleene-Brouwer relation for the lifted tree $\text{MS}_{\langle r \rangle}$ and some right-to-left-decreasing relation on children of the lifted tree. By Kleene-Brouwer theorem, $(>_{\text{KB}_1,r})$ and $(>_{\text{KB}_2,r})$ are well-founded. Define $\text{ET}_2(\langle u_1, \dots, u_n \rangle)$ as the $(>_{\text{KB}_2,u_1})$-sorted sequence of elements in $\text{ET}(\langle u_1, \dots, u_n \rangle)$. Then consider

$$\text{ET}_2(\langle u_1 \rangle), \text{ET}_2(\langle u_1, u_2 \rangle), \text{ET}_2(\langle u_1, u_2, u_3 \rangle), \dots$$

Define $>_{\text{KB},r}$ as the Kleene-Brouwer relation for $>_{\text{KB},r}$ and the set of $(>_{\text{KB}_2,r})$-sorted finite sequences of elements in $\text{MS}_{\langle r \rangle}$. This definition is a key
idea. By this definition, we can show the most difficult step in this proof:

$$ \mathrm{ET2}(\langle u_1 \rangle) >_{\mathrm{KB},u_1} \mathrm{ET2}(\langle u_1, u_2 \rangle) >_{\mathrm{KB},u_1} \mathrm{ET2}(\langle u_1, u_2, u_3 \rangle) >_{\mathrm{KB},u_1} \dots $$

Since $(>_{\mathrm{KB},u_1})$ is well-founded by Kleene-Brouwer theorem, we have contradiction. Hence we have shown $u_1 >_{\Pi} u_2 >_{\Pi} u_3 >_{\Pi} \dots$ terminates.

In general we need classical logic to derive induction principle from well-foundedness, but the idea we have explained will work well for showing induction principle in intuitionistic logic.

## 2.3 Proof of Podelski-Rybalchenko Theorem for Induction

This subsection gives a proof of Podelski-Rybalchenko Theorem for Induction.

The next lemma shows that induction principle for each relation implies induction principle for monotonically-colored sequences. This lemma can be proved by refining Lemma 6.4 (1) of [3] from second-order logic to first-order logic. The proof is given in [6].

**Lemma 2.5** If $HA \vdash \mathrm{Ind}(\mathrm{DT}(U, >_{R_i}), >_{\mathrm{ext}})$ for all $1 \le i \le k$, then $HA \vdash \forall r \in U. \mathrm{Ind}(\mathrm{MS}_{\langle r \rangle}, >_{\mathrm{ext}})$.

Next we create Kleene-Brouwer relations $>_{\mathrm{KB1},r}$ and $>_{\mathrm{KB2},r}$ for monotonically-colored sequences beginning with $r$. Then we consider the set of $(>_{\mathrm{KB2},r})$-sorted finite sequences of monotonically-colored finite sequences beginning with $r$. It is a lifted tree. Then, by induction principle for MS, the lifted tree is well-founded with the one-step extension relation. The Kleene-Brouwer relation for the lifted tree and $>_{\mathrm{KB1},r}$ gives us $>_{\mathrm{KB},r}$ for the lifted tree. Since an Erdös tree is in the lifted tree, this will later show induction principle for Erdös trees.

**Definition 2.6** For $u \in U$, we define $>_{u,\mathrm{Left}}$ for $U$ by: $u_1 >_{u,\mathrm{Left}} u_2$ if $u >_{R_j} u_1$, $u >_{R_l} u_2$, and $j < l$ for some $j, l$.

We define $>_{\mathrm{KB1},r}$ for $\mathrm{MS}_{\langle r \rangle}$ as the KB relation for $\mathrm{MS}_{\langle r \rangle} \subseteq U^{<\omega}$ and $(>_{u,\mathrm{Left}}) \subseteq U^2$ for all $u \in U$.

For $u \in U$, we define $>_{u,\mathrm{Right}}$ for $U$ by: $u_1 >_{u,\mathrm{Right}} u_2$ if $u_1 <_{u,\mathrm{Left}} u_2$.

We define $>_{\mathrm{KB2},r}$ for $\mathrm{MS}_{\langle r \rangle}$ as the KB relation for $\mathrm{MS}_{\langle r \rangle} \subseteq U^{<\omega}$ and $(>_{u,\mathrm{Right}}) \subseteq U^2$ for all $u \in U$.

We define $>_{\mathrm{KB},r}$ for $\mathrm{DS}(\mathrm{MS}_{\langle r \rangle}, >_{\mathrm{KB2},r})_{\langle\langle r \rangle\rangle}$ as the KB relation for $\mathrm{DS}(\mathrm{MS}_{\langle r \rangle}, >_{\mathrm{KB2},r})_{\langle\langle r \rangle\rangle} \subseteq \mathrm{MS}_{\langle r \rangle}^{<\omega}$ and $>_{\mathrm{KB1},r}$.

$>_{u,\mathrm{Left}}$ is the left-to-right-decreasing order of children of $u$ in some ordered tree of $U$ in which the edge label $R_i$ is put to an edge $(x, y)$ such that $x >_{R_i} y$, each parent has at most one child of the same edge label, and children are ordered by their edge labels with $R_1 < \dots < R_k$. Similarly $>_{u,\mathrm{Right}}$ is the right-to-left-decreasing order of children of $u$ in the ordered tree.
**Definition 2.7** For $u \in U \subseteq N$, finite $T \subseteq MS$ such that $\forall \rho \in T. \forall v \in \rho.(v >_{R_1+...+R_k} u)$, and for $\sigma \in T$, we define the function insert by:

$$ \text{insert}(u, T, \sigma) = \text{insert}(u, T, \sigma * \langle v \rangle) \text{ if last}(\sigma) >_{R_i} u, v = \mu v.(\sigma * \langle v \rangle \in T \wedge \text{last}(\sigma) >_{R_i} v), \\ T \cup \{\sigma * \langle u \rangle\} \text{ otherwise,} $$

where $\mu v.F(v)$ denotes the least element $v$ with the natural number order such that $F(v)$. Formally insert($u, T, \sigma$) = $T'$ is an abbreviation of some **HA**-formula $G(u, T, \sigma, T')$. It is the same for ET below.

For $x \in \text{DT}(U, >_{R_1+...+R_k}) - \{\langle \rangle\}$, we define $\text{ET}(x) \subseteq \text{MS}$ by

$$ \text{ET}(\langle u \rangle) = \{\langle u \rangle\}, \\ \text{ET}(x * \langle u \rangle) = \text{insert}(u, \text{ET}(x), \langle \text{first}(x) \rangle) \text{ if } x \neq \langle \rangle. $$

Note that insert($u, T, \sigma$) adds a new element $u$ to the set $T$ at some position below $\sigma$ to obtain a new set. $\text{ET}(x)$ is an Erdös tree obtained from the decreasing transitive sequence $x$.

The next lemma (1) states a new element is inserted at a leaf. It is proved by induction on the number of elements in $T$. The claim (2) states that edges from a parent to its children have different colors. It is proved by induction on the length of $x$.

**Lemma 2.8** (1) For $u \in U$, $T \subseteq MS$, and $\sigma \in T$, if $u \notin \rho$ for all $\rho \in T$, $\sigma = \langle x_0, \dots, x_{n-1} \rangle$, $x_i >_{R_j} x_{i+1}$ implies $x_i >_{R_j} u$ for all $i < n-1$, and insert($u, T, \sigma$) = $T'$, then there is some $\rho \in T_\sigma$ such that $\rho * \langle u \rangle \in MS$, $T' = T + \{\rho * \langle u \rangle\}$, and $\rho * \langle u \rangle$ is a maximal sequence in $T'$.

(2) If $\sigma * \langle u, u_1 \rangle * \rho_1, \sigma * \langle u, u_2 \rangle * \rho_2 \in \text{ET}(x)$, $u >_{R_i} u_1$, and $u >_{R_i} u_2$, then $u_1 = u_2$.

**Definition 2.9** For $x \in \text{DT}(U, >_{R_1+...+R_k}) - \{\langle \rangle\}$, we define

$$ \text{ET2}(x) = \langle x_0, \dots, x_{n-1} \rangle $$

where $\{x_0, \dots, x_{n-1}\} = \text{ET}(x)$ and $\forall i < n-1.(x_i >_{\text{KB2,first}(x)} x_{i+1})$.

Note that $>_{\text{KB2,first}(x)}$ is a total order on $\text{ET}(x)$ by Lemma 2.8 (2). $\text{ET2}(x)$ is the decreasing sequence of all nodes in the Erdös tree $\text{ET}(x)$ ordered by $>_{\text{KB2,first}(x)}$.

The next lemma shows $\text{ET2}$ is monotone. It is the key property of reduction in Lemma 2.11.

**Lemma 2.10 HA** $\vdash \forall r \in U. \forall x, y \in \text{DT}(U, >_{R_1+...+R_k})_{\langle r \rangle}. (x >_{\text{ext}} y \rightarrow \text{ET2}(x) >_{\text{KB},r} \text{ET2}(y))$.

*Proof.* Fix $r \in U$ and $x, y \in \text{DT}(U, >_{R_1+...+R_k})_{\langle r \rangle}$ and assume $x >_{\text{ext}} y$. Let $y = x * \langle u \rangle$. Then $\text{ET}(y) = \text{insert}(u, \text{ET}(x), \langle r \rangle)$. By Lemma 2.8 (1), we have $\sigma$ such that $\text{ET}(y) = \text{ET}(x) + \{\sigma * \langle u \rangle\}$. Then we have two cases:

Case 1. $\text{last}(\text{ET2}(x)) >_{\text{KB2},r} \sigma * \langle u \rangle$.
Then ET2(y) = ET2(x) * ⟨σ * ⟨u⟩⟩. By definition, ET2(x) ><sub>KB,r</sub> ET2(y).
Case 2. σ * ⟨u⟩ ><sub>KB2,r</sub> τ for some τ ∈ ET2(x).

Let $\rho$ be the next element of $\sigma * \langle u \rangle$ in ET2(y). Then ET2($x$) = $\alpha * \langle \rho \rangle * \beta$
and ET2($y$) = $\alpha * \langle \sigma * \langle u \rangle, \rho \rangle * \beta$. By definition of ET2, $\sigma * \langle u \rangle >_{\text{KB2,r}} \rho$. Since
$\sigma * \langle u \rangle$ is maximal in ET(y) by Lemma 2.8 (1), there is no $\alpha \neq \langle \rangle$ such that
$\sigma * \langle u \rangle * \alpha = \rho$. Hence $\sigma * \langle u \rangle <_{\text{KB1,r}} \rho$. Hence ET2($x$) >_{\text{KB,r}} ET2(y). □

The next lemma shows that induction for decreasing transitive sequences is
reduced to induction for Erdös trees with ><sub>KB,r</sub>.

**Lemma 2.11 HA** * $\vdash$ $\forall r \in U.\mathrm{Ind}(\mathrm{ET2}(\mathrm{DT}(U, >_{R_1+\dots+R_k})_{\langle r \rangle}), >_{\mathrm{KB},r})$ *implies*
**HA** * $\vdash$ $\mathrm{Ind}(\mathrm{DT}(U, >_{R_1+\dots+R_k}), >_{\mathrm{ext}})$.

*Proof Sketch.* In order to show Ind(DT(*U*, >*R*<sub>1</sub>+...+*R*<sub>*k*</sub>), ><sub>ext</sub>) for *F*, define
*G*<sub>*y*</sub> ≡ ∀*z* ∈ DT(*z* ≠ ⟨⟩ → ET2(*z*) = *y* → *F*z) and use Ind(ET2(DT(*U*, >*R*<sub>1</sub>+...+*R*<sub>*k*</sub>))_{⟨*r*⟩}, ><sub>KB,r</sub>) for *G* and Lemma 2.10. The proof is in [6]. □

The next lemma shows induction holds when we restrict the universe. The
proof is in [6].

**Lemma 2.12 HA** * $\vdash$ Ind(*U*, >) *and* **HA** * $\vdash$ V $\subseteq$ U *imply* **HA** $\vdash$ Ind(*V*, >).

The next lemma shows induction is implied from induction for decreasing
sequences. The proof is in [6].

**Lemma 2.13 HA** * $\vdash$ Ind(DS(*U*, >), ><sub>ext</sub>) *implies* **HA** * $\vdash$ Ind(*U*, >).

The next lemma shows induction for a power of a relation implies induction
for the relation. The proof is in [6].

**Lemma 2.14 HA** * $\vdash$ Ind(*U*, ><sup>*n*</sup>) *implies* **HA** * $\vdash$ Ind(*U*, >).

Define

$$
\begin{align*}
\mathrm{Trans}(U, >_R) &\equiv \forall xyz \in U (x >_R y \land y >_R z \rightarrow x >_R z), \\
\mathrm{Decide}(U, >_R) &\equiv \forall xy \in U (x >_R y \lor \neg(x >_R y)).
\end{align*}
$$

The next theorem states that if some powers of relations >$_{R_i}$ have induction
principle, >$_{R_i}$ are decidable and their union is transitive, then the union has
induction principle. This theorem is the same as Theorem 6.1 in [5] except HA
and the decidability condition Decide($U$, >$_{R_i}$).

**Theorem 2.15 (Podelski-Rybalchenko Theorem for Induction) If**
**HA** * $\vdash$ Ind(*U*, ><sub>*R*<sub>1</sub></sub>), **HA** * $\vdash$ Decide(*U*, ><sub>*R*<sub>1</sub></sub>), ..., **HA** * $\vdash$ Ind(*U*, ><sub>*R*<sub>*k*</sub></sub>), **HA** * $\vdash$*
Decide(*U*, ><sub>*R*<sub>*k*</sub></sub>), and **HA** * $\vdash$ Trans(*U*, ><sub>*R*<sub>1</sub>+...+*R*<sub>*k*</sub></sub>), then Ind(*U*, ><sub>*R*<sub>1</sub>+...+*R*<sub>*k*</sub></sub>).

*Proof.* We will discuss in **HA**.

By Lemma 2.14, we can replace $n_i$ by 1 and obtain Ind($U$, >$_{R_i}$). In order to
obtain disjoint relations, we define >$_{R'_1}$ as >$_{R_1}$ and >$_{R'_{i+1}}$ as (>$_{R_{i+1}}$) - (>$_{R'_1}$)
- ... - (>$_{R'_i}$). Then (>$_{R'_1}$), ..., (>$_{R'_k}$) are disjoint and $\forall xy \in U(x >_{R_1} \cup \dots \cup R_k)$
$y \to x >_{R'_1 + \dots + R'_k} y$) by Decide($U$, >$_{R_i}$) for $1 \le i \le k$. Since (>$_{R'_i}$) $\subseteq$ (>$_{R_i}$),
Ind($U, >_{R_i}$). For simplicity, from now on we write $>_{R_i}$ for $>_{R'_i}$ in this proof. We will show Ind($U, >_{R_1+...+R_k}$).

From Ind($U, >_{R_i}$), by replacing induction on elements by induction on sequences, we have Ind(DT($U, >_{R_i}$), $>_{ext}$) for $1 \le i \le k$. By Lemma 2.5, we have $\forall r \in U.Ind(MS_{\langle r \rangle}, >_{ext})$. Apparently $\forall u \in U.Ind(U, >_{u,Left})$. By taking $U$ to be $U$, $T$ to be $MS_{\langle r \rangle}$, and $>_{u}$ to be $>_{u,Left}$ in Theorem 2.3 for $>_{KB1,r}$, we have $\forall r \in U.Ind(MS_{\langle r \rangle}, >_{KB1,r})$. By Theorem 2.3 for $>_{KB2,r}$, we have $\forall r \in U.Ind(MS_{\langle r \rangle}, >_{KB2,r})$ similarly. By replacing induction on elements by induction on sequences, we have $\forall r \in U.Ind(DS(MS_{\langle r \rangle}, >_{KB2,r}), >_{ext})$. Since DS(MS_{\langle r \rangle}, >_{KB2,r})_{\langle\langle r \rangle\rangle}$ is a subset of DS(MS_{\langle r \rangle}, >_{KB2,r}), from Lemma 2.12, we have $\forall r \in U.Ind(DS(MS_{\langle r \rangle}, >_{KB2,r})_{\langle\langle r \rangle\rangle}, >_{ext})$. By taking $T$ to be DS(MS_{\langle r \rangle}, >_{KB2,r})_{\langle\langle r \rangle\rangle}, U$ to be $MS_{\langle r \rangle}$, and ($>_{u}$) to be ($>_{KB1,r}$) in Theorem 2.3 for $>_{KB,r}$, we have $\forall r \in U.Ind(DS(MS_{\langle r \rangle}, >_{KB2,r})_{\langle\langle r \rangle\rangle}, >_{KB,r}$). This is a key step of this proof. Since ET2(DT($U, >_{R_1+...+R_k}$)_{\langle r \rangle}) $\subseteq$ DS(MS_{\langle r \rangle}, >_{KB2,r})_{\langle\langle r \rangle\rangle}$, by Lemma 2.12, we have $\forall r \in U.Ind(ET2(DT($U, >_{R_1+...+R_k}$)_{\langle r \rangle}), >_{KB,r})$. By Lemma 2.11, Ind(DT($U, >_{R_1+...+R_k}$), $>_{ext}$). By Trans($U, >_{R_1+...+R_k}$), DT($U, >_{R_1+...+R_k}$) is DS($U, >_{R_1+...+R_k}$). Hence we have Ind(DS($U, >_{R_1+...+R_k}$), $>_{ext}$). From Lemma 2.13, by replacing induction on sequences by induction on elements, we have Ind($U, >_{R_1+...+R_k}$). $\square$

# 3 Cyclic Proofs

## 3.1 Intuitionistic Martin-Löf's Inductive Definition System LJID

We define an intuitionistic Martin-Löf's inductive definition system, called LJID.

The language of LJID is determined by a first-order language with inductive predicate symbols. The logical system LJID is determined by production rules for inductive predicate symbols. These production rules mean that the inductive predicate denotes the least fixed point defined by these production rules.

We assume the first order terms $t, u, ...$. We assume $\forall x$ and $\exists y$ are less tightly connected than other logical connectives. To save space, we sometimes write $Pxy$ and $Fxy$ for $P(x, y)$ and $F(x, y)$.

For example, the production rules of the inductive predicate symbol $N$ are

$$ \frac{N}{N0} \qquad \frac{Nx}{Nsx} $$

These production rules mean that $N$ denotes the smallest set closed under $0$ and $s$, namely the set of natural numbers.

The inference rules of LJID contains the introduction rules and the elimination rules for inductive predicates, determined by the production rules. These rules describe that the predicate actually denotes the least fixed point. In particular, the elimination rule describes the induction principle.

For example, the above production rules give the introduction rules

$$ \frac{\Gamma \vdash N}{\Gamma \vdash N0} \qquad \frac{\Gamma \vdash Nx}{\Gamma \vdash Nsx} $$
<figure><img src="image_2.png" /><figcaption>Fig. 1. Inference Rules</figcaption></figure>

and the elimination rule

$$ \frac{\Gamma \vdash F0 \quad \Gamma, Fx \vdash Fsx}{\Gamma, Nt \vdash Ft} $$

This elimination rule describes mathematical induction principle.

The inference rules are given in Figure 1 where for (P<sub>i</sub> R) we assume the production rule

$$ \frac{Q_1 \vec{u}_1 \quad \dots \quad Q_n \vec{u}_n \quad P_1 \vec{t}_1 \quad \dots \quad P_m \vec{t}_m}{P \vec{t}} $$

and for (Ind P<sub>j</sub>) we assume a predicate F<sub>i</sub> for each P<sub>i</sub> and the minor premises are defined as

$$ \Gamma, Q_{i1} \vec{u}_{i1}, \dots, Q_{in_i} \vec{u}_{in_i}, F_1 \vec{t}_{i1}, \dots, F_{im_i} \vec{t}_{im_i} \vdash F_i \vec{t}_i $$

for each production rule

$$ \frac{Q_{i1} \vec{u}_{i1} \quad \dots \quad Q_{in_i} \vec{u}_{in_i} \quad P_1 \vec{t}_{i1} \quad \dots \quad P_{im_i} \vec{t}_{im_i}}{P_i \vec{t}_i} $$

Note that the antecedents and the succedents are sets and the succedent is empty or a formula.

The system **LJID** is the same as the system obtained from classical Martin-Löf's inductive definition system **LKID** defined in [11] by restricting every sequent to intuitionistic sequents and replacing (→L), (∨R), and (Ind P<sub>j</sub>) accordingly. The provability of the system **LJID** is the same as that of the natural deduction system given in [18].
## 3.2 Cyclic Proof System CLJID<sup>ω</sup>

An intuitionistic cyclic proof system, called **CLJID**<sup>ω</sup>, is defined as the system obtained from classical cyclic proof system **CLKID**<sup>ω</sup> defined in [11] by restricting every sequent to intuitionistic sequents and replacing (→L) and (∨R) in the same way as **LJID**. Note that the global trace condition in **CLJID**<sup>ω</sup> is the same as that in **CLKID**<sup>ω</sup> (Definition 5.5 of [11]).

Namely, the inference rules of **CLJID**<sup>ω</sup> are obtained from **LJID** by replacing (IndP<sub>j</sub>) by

$$ \frac{\text{case distinctions}}{\Gamma, P\vec{u} \vdash \Delta} \quad (\text{CaseP}) $$

where the case distinctions are

$$ \Gamma, \vec{u} = \vec{t}, Q_1 \vec{u}_1, \dots, Q_n \vec{u}_n, P_1 \vec{t}_1, \dots, P_m \vec{t}_m \vdash \Delta $$

for each production rule

$$ \frac{Q_1 \vec{u}_1 \quad \dots \quad Q_n \vec{u}_n \quad P_1 \vec{t}_1 \quad \dots \quad P_m \vec{t}_m}{P \vec{t}} $$

A cyclic proof in **CLJID**<sup>ω</sup> is defined by (1) allowing a bud as an open assumption and requiring a companion for each bud, (2) requiring the global trace condition.

The global trace condition [10, 8] is the condition that for every infinite path in the infinite unfolding of a given cyclic proof, there is a trace that passes main formulas of case rules infinitely many times. The global trace condition ensures that when we think some measure by counting case rules, the measure of a bud is smaller than that of the companion. For example, in the next example the companion (a) uses $Px0y$, but the bud (a) uses $Px0y$ where $x$ is $x'$ and $x' < x$, so their actual meanings are different even though they are of the same form. The global trace condition guarantees the soundness of a cyclic proof system.

An example of a cyclic proof (trivial steps are omitted) is as follows:

$$ \frac{\frac{(a)Px0y \vdash x = y}{Px'0y' \vdash x' = y'} \quad (\text{Subst})}{\frac{\overline{Px'0y', x = sx', y = sy' \vdash x' = y'}}{\overline{Px'0y', x = sx', y = sy' \vdash sx' = sy'}} \quad (\text{Wk})} \quad (\text{Case P}) $$

where the mark (a) denotes the bud-companion relation, and the production rules are

$$ \frac{Pxyz}{P0yy} \qquad \frac{P(sx)y(sz)}{P(sx)y(sz)} $$

Note that the predicate P is addition on natural numbers and the proof is, essentially, deriving the arithmetic identity $x + 0 = x$.

We call an atomic formula an inductive atomic formula when its predicate symbol is an inductive predicate symbol.
### 3.3 Cyclic Proofs for Coinductive Predicates

This subsection shows how we can use a cyclic proof system to formalize coinductive predicates. Since a coinductive predicate is a dual of an inductive predicate, and sequent calculus is symmetric for this dual, we can construct a cyclic proof system for coinductive predicates. For example, for stream predicates we can define a cyclic proof system $\mu\nuLK$ from $\mathbf{CLKID}^\omega$ as follows:

(1) Add function symbols head, tail, and the pair $\langle\cdot, \cdot\rangle$ with the axioms $\langle x, y\rangle = \langle x', y'\rangle \rightarrow x = x' \wedge y = y'$ and $x = \langle\text{head } x, \text{tail } x\rangle$, and a coinductive predicate symbol $P$ with its coproduction rule

$$ \frac{Qyx \ P x}{P \langle y, x \rangle} \ co $$

which means $P$ is defined coinductively by this rule. Note that $P$ represents the set of streams $\langle x_0, \langle x_1, \langle x_2, \langle \dots \rangle \rangle \rangle$ such that $Q(x_i, \langle x_{i+1}, \langle x_{i+2}, \langle \dots \rangle \rangle)$ for all $i$.

(2) Add the inference rules $(P R)$ and (Case $P$) in the same way as $\mathbf{CLKID}^\omega$, namely,

$$ \frac{\Gamma, t = \langle y, x \rangle, Qyx, P x \vdash \Delta}{\Gamma, P t \vdash \Delta} \quad (\text{Case } P) $$

$$ \frac{\Gamma \vdash Qyx, \Delta \quad \Gamma \vdash P x, \Delta}{\Gamma \vdash P \langle y, x \rangle, \Delta} \quad (P R) $$

(3) We call an atomic formula a coinductive atomic formula when its predicate symbol is a coinductive predicate symbol. We define a cotrace as a sequence of coinductive atomic formulas in the succedents of a path such that two atomic formulas are related by an inference rule in a similar way to a trace defined in [11]. The global trace and cotrace condition is the condition that for every infinite path in the infinite unfolding of a given cyclic proof, the path contains either a trace that passes main formulas of case rules infinitely many times, or a cotrace that passes main formulas of rules $(P R)$ infinitely many times.

(4) A cyclic proof is a preproof that satisfies the global trace and cotrace condition.

Example. We define the bit stream predicate $\text{BS}$ by the following coproduction rules:

$$ \frac{\text{Bit } y \quad \text{BS } x}{\text{BS} \langle y, x \rangle} \ co $$

where $\text{Bit}$ is an ordinary predicate symbol with the axiom $\text{Bit } x \leftrightarrow x = 0 \lor x = 1$. The inference rules from this production rule are:

$$ \frac{\Gamma \vdash \text{Bit } y, \Delta \quad \Gamma \vdash \text{BS } x, \Delta}{\Gamma \vdash \text{BS} \langle y, x \rangle, \Delta} \quad (\text{BS } R) $$

$$ \frac{\Gamma, t = \langle y, x \rangle, \text{Bit } y, \text{BS } x \vdash \Delta}{\Gamma, \text{BS } t \vdash \Delta} \quad (\text{Case BS}) $$

Then we can show $x = \langle 0, x \rangle \vdash \text{BS } x$, namely, the zero stream is a bit stream, as follows (trivial steps are omitted):

$$ \frac{x = \langle 0, x \rangle \vdash \text{Bit } 0 \quad (a) \ x = \langle 0, x \rangle \vdash \text{BS } x}{x = \langle 0, x \rangle \vdash \text{BS} \langle 0, x \rangle \quad (a) \ x = \langle 0, x \rangle \vdash \text{BS } x} \quad (\text{BS } R) $$
where (a) denotes the bud-companion relation.

The cyclic proof system $\mu\nu$LK is sound for the standard model.

**Theorem 3.1** If a sequent is provable in $\mu\nu$LK, then it is true in the standard model where a coinductive predicate is interpreted as the greatest fixed point that satisfies the coproduction rules.

*Proof sketch.* We add an ordinary predicate symbol $\tilde{Q}$ with the axiom $\tilde{Q}yx \leftrightarrow \neg Qyx$ and add an inductive predicate symbols $\tilde{P}$ with the production rules

$$ \frac{\tilde{Q}(\text{head } x)(\text{tail } x)}{\tilde{P}x} \qquad \frac{\tilde{P}(\text{tail } x)}{\tilde{P}x} $$

In the standard model, $P$ is the greatest solution of the equation

$$ P x \leftrightarrow \exists y x'(x = \langle y, x' \rangle \land Q y x' \land P x') $$

and $\tilde{P}$ is the least solution of the equation

$$ \tilde{P} x \leftrightarrow \tilde{Q}(\text{head } x)(\text{tail } x) \lor \tilde{P}(\text{tail } x). $$

By putting $\neg$ on both sides of the equation for $P$ and taking $y$ and $x'$ to be head $x$ and tail $x$, we can show $\neg P$ is a solution of the equation for $\tilde{P}$. Hence $\tilde{P}x \to \neg P x$ is true. In the same say by putting $\neg$ on both sides of the equation for $\tilde{P}$, and using $x = \langle \text{head}x, \text{tail}x \rangle$, we can show $\neg \tilde{P}$ is a solution of the equation for $P$. Hence $\neg \tilde{P}x \to P x$ is true. Therefore $\tilde{P}x \leftrightarrow \neg P x$ is true.

We define a transformation $(\neg)$ for a sequent and a proof, in order to replace $P$ by $\tilde{P}$. For a sequent $J$, we define $J^-$ by replacing $P$ by $\neg \tilde{P}$ and then moving an atomic formula $\neg \tilde{P}t$ of the antecedent to $\tilde{P}t$ of the succedent and moving an atomic formula $\neg \tilde{P}t$ of the succedent to $\tilde{P}t$ of the antecedent.

Given a cyclic proof $\pi$, we define $\pi^-$ by replacing each sequent $J$ by $J^-$ and then replacing $(P R)$ by

$$ \frac{\Gamma^- \vdash Q y x', \Delta^-}{\Gamma^-, \tilde{Q} y x' \vdash \Delta^- \quad \Gamma^-, \tilde{P} x' \vdash \Delta^-} \quad \text{(Case } \tilde{P}) \quad \text{(trivial steps are omitted)} $$

and replacing (Case $P$) by

$$ \frac{\Gamma^-, x = \langle y, x' \rangle, Q y x' \vdash \tilde{P} x', \Delta^-}{\Gamma^-, x = \langle y, x' \rangle \vdash \tilde{Q} y x', \tilde{P} x', \Delta^-} \quad (\tilde{P} R) \\ \frac{\Gamma^-, x = \langle y, x' \rangle \vdash \tilde{Q} y x', \tilde{P} x, \Delta^-}{\Gamma^-, x = \langle y, x' \rangle \vdash \tilde{P} x, \Delta^-} \quad (\tilde{P} R) \\ \frac{\Gamma^-, x = \langle y, x' \rangle \vdash \tilde{P} x, \Delta^-}{\Gamma^- \vdash \tilde{P} x, \Delta^-} \quad \text{(trivial steps are omitted)} $$

Then a cotrace in $\pi$ corresponds to a trace in $\pi^-$. Hence $\pi^-$ is a cyclic proof of $J^-$ in $\text{CLKID}^\omega$ when $\pi$ is a cyclic proof of $J$ in $\mu\nu$LK. By the soundness of $\text{CLKID}^\omega$, $J^-$ is true in the standard model. Since $\tilde{P}x \leftrightarrow \neg P x$ is true, $J$ is true in the standard model where $P$ is interpreted as the greatest fixed point. $\square$
# 4 Equivalence between LJID and CLJID<sup>ω</sup>

This section studies the equivalence between CLJID<sup>ω</sup> and LJID.

## 4.1 Countermodel and Addition of Heyting Arithmetic

This subsection gives a countermodel and adds arithmetic to the logical systems.

The counterexample given in [4] also shows that the equivalence between CLJID<sup>ω</sup> and LJID does not hold in general, because the proof of the statement H in [4] is actually in CLJID<sup>ω</sup>, and LJID does not prove H since LKID does not prove H. This gives us the following theorem (it is not new in the sense [4] immediately implies it).

**Theorem 4.1** There are some signature and some set of production rules for which the provability of CLJID<sup>ω</sup> is not the same as that of LJID.

There is a possibility of the equivalence under some conditions. We will show the equivalence holds by adding arithmetic to both systems.

We add arithmetic to both LJID and CLJID<sup>ω</sup>.

**Definition 4.2** CLJID<sup>ω</sup> + HA and LJID + HA are defined to be obtained from CLJID<sup>ω</sup> and LJID by adding Heyting arithmetic. Namely, we add constants and function symbols 0, s, +, ×, the inductive predicate symbol N, the productions for N, and Heyting axioms:

$$ \begin{array}{l} \overline{N0} \qquad \frac{Nx}{Nsx} \quad \vdash Nx \to sx \neq 0, \quad \vdash Nx \wedge Ny \to sx = sy \to x = y, \\ \vdash Nx \to x + 0 = x, \quad \vdash Nx \wedge Ny \to x + sy = s(x + y), \\ \vdash Nx \to x \times 0 = 0, \quad \vdash Nx \wedge Ny \to x \times sy = x \times y + x. \end{array} $$

## 4.2 Equivalence Theorem

In this subsection we state the equivalence theorem and explains proof ideas.

First we assume a new inductive predicate symbol P' for each inductive predicate symbol P and define the production rules of P' in the same way as [5].

**Definition 4.3** We define the production rule of P'

$$ \frac{Q_1 \vec{u}_1 \dots Q_n \vec{u}_n \quad v > v_1 \quad P'_1 \vec{t}_1 v_1 \dots \quad v > v_m \quad P'_m \vec{t}_m v_m \quad Nv}{P' \vec{t} v} $$

for each production rule of P

$$ \frac{Q_1 \vec{u}_1 \dots Q_n \vec{u}_n \quad P_1 \vec{t}_1 \dots P_m \vec{t}_m}{P \vec{t}} $$

where v, v₁, ..., v_m are fresh variables.
We write **LJID** + **HA** + $(\Sigma, \Phi)$ for the system **LJID** + **HA** with the signature $\Sigma$ and the set $\Phi$ of production rules. Similarly we write $\text{CLJID}^{\omega} + \text{HA} + (\Sigma, \Phi)$. For simplicity, in $\Phi$ we write only $P$ for the set of production rules for $P$. We define $\Sigma_N = \{0, s, +, \times, <, N\}$ and $\Phi_N = \{N\}$. We write $P''$ for $(P')'$.

The next theorem shows the equivalence of **LJID** + **HA** and $\text{CLJID}^{\omega} + \text{HA}$ with signatures.

**Theorem 4.4 (Equivalence of LJID + HA and CLJID<sup>ω</sup> + HA)** Let $\Sigma = \Sigma_N \cup \{\vec{Q}, \vec{P}, \vec{P}'\}$ and $\Phi = \Phi_N \cup \{\vec{P}, \vec{P}'\}$. Then the probability of $\text{CLJID}^{\omega} + \text{HA} + (\Sigma, \Phi)$ is the same as that of $\text{LJID} + \text{HA} + (\Sigma, \Phi)$.

We explain our ideas of proofs of this theorem. [5] shows the equivalence between classical systems by using classical Podelski-Rybalchenko theorem for induction. This proof goes well even if we replace classical systems by intuitionistic systems except that we have to replace classical Podelski-Rybalchenko theorem for induction by intuitionistic Podelski-Rybalchenko theorem for induction. Since we proved intuitionistic Podelski-Rybalchenko theorem for induction in Theorem 2.15, by combining them, we can show the equivalence between **LJID** and $\text{CLJID}^{\omega}$.

# 5 Proof Transformation

This section gives the proof of the equivalence. More detailed discussions are given in [6]. We define proof transformation from $\text{CLJID}^{\omega} + \text{HA}$ to $\text{LJID} + \text{HA}$. First we will define stage numbers and path relations, and then define proof transformation using them.

For notational convenience, we assume a cyclic proof $\Pi$ in this section. Let the buds in $\Pi$ be $J_{1i}$ ($i \in I$) and the companions be $J_{2j}$ ($j \in K$). Assume $f: I \to K$ such that the companion of a bud $J_{1i}$ is $J_{2,f(i)}$.

## 5.1 Stage Numbers for Inductive Definitions

In this subsection, we define and discuss stage transformation.

We introduce a stage number to each inductive atomic formula so that the argument of the formula comes into the inductive predicate at the stage of the stage number. This stage number will decrease by a progressing trace. A proof in $\text{LJID} + \text{HA}$ will be constructed by using the induction on stage numbers.

First we give stage transformation of an inductive atomic formula. We assume a fresh inductive predicate symbol $P'$ for each inductive predicate symbol $P$ and we call it a *stage-number inductive predicate symbol*. $P'(\vec{t}, v)$ means that the element $\vec{t}$ comes into $P$ at the stage $v$. We transform $P(\vec{t})$ into $\exists v P'(\vec{t}, v)$. We call a variable $v$ a *stage number of $\vec{t}$* when $P'(\vec{t}, v)$. $P(\vec{t})$ and $\exists v P'(\vec{t}, v)$ will become equivalent by inference rules introduced by the transformation of production rules. We call $P'(\vec{t}, v)$ a *stage-number inductive atomic formula*.

Secondly we give stage transformation of a production rule. We transform the production of $P$ into the production of $P'$ given in Definition 4.3.
Next we give the stage transformation of a sequent. For given fresh variables $\vec{v}$, we transform a sequent $J$ into $J_{\vec{v}}^\circ$ defined as follows. We define $\Gamma^\bullet$ as the set obtained from $\Gamma$ by replacing $P(\vec{t})$ by $\exists v P'(\vec{t}, v)$. For fresh variables $\vec{v}$, we define $(\Gamma)_{\vec{v}}^\circ$ as the sequent obtained from $\Gamma^\bullet$ by replacing the $i$-th element of the form $\exists v P'(\vec{t}, v)$ in the sequent $\Gamma^\bullet$ by $P'(\vec{t}, v_i)$. We define $(\Gamma \vdash \Delta)^\bullet$ by $\Gamma^\bullet \vdash \Delta^\bullet$, and define $(\Gamma \vdash \Delta)_{\vec{v}}^\circ$ by $(\Gamma)_{\vec{v}}^\circ \vdash \Delta^\bullet$.

We write $(a_i)_{i \in I}$ for the sequence of elements $a_i$ where $i$ varies in $I$. We extend the notion of proofs by allowing open assumptions. We write $\Gamma \vdash_{\mathrm{CLJID}^\omega+\mathrm{HA}} \Delta$ with assumptions $(J_i)_{i \in I}$ when there is a proof with assumptions $(J_i)_{i \in I}$ and the conclusion $\Gamma \vdash \Delta$ in $\mathrm{CLJID}^\omega + \mathrm{HA}$.

**Definition 5.1** In a path $\pi$ in a proof, we define Ineq($\pi$) as the set of the forms $v > v'$ and $v = v'$ for any stage numbers $v, v'$ eliminated by every case distinction in $\pi$.

The proof of the next proposition gives *stage transformation* of a proof into a proof of the stage transformation of the conclusion of the original proof. We write $\Pi^\circ$ for the stage transformation of $\Pi$.

**Proposition 5.2 (Stage Transformation)** For any fresh variables $\vec{v}$, if $\Gamma \vdash_{\mathrm{CLJID}^\omega+\mathrm{HA}} \Delta$ with assumptions $(\Gamma_i \vdash \Delta_i)_{i \in I}$ without any buds, then for some fresh variables $(\vec{v}_i)_{i \in I}$ we have $(\Gamma)_{\vec{v}}^\circ \vdash_{\mathrm{CLJID}^\omega+\mathrm{HA}} \Delta^\bullet$ with assumptions (Ineq($\pi_i$), $(\Gamma_i)_{\vec{v}_i}^\circ \vdash \Delta_i^\bullet$) with any buds, where $\pi_i$ is the path from the conclusion to the assumption $(\Gamma_i)_{\vec{v}_i}^\circ \vdash \Delta_i^\bullet$.

## 5.2 Path Relation

In this section, we will introduce path relations and discuss them.

We assume a subproof $\Pi_j$ of $\Pi$ such that it does not have buds, its conclusion is $J_{2j}$ and its assumptions are $J_{1i}$ ($i \in I_j$).

For $J$ in $\Pi_j^\circ$, we define $\tilde{J}$ as $\langle v_1, \dots, v_k \rangle$ where $J$ is $\Gamma_{v_1 \dots v_k}^\circ \vdash \Delta^\bullet$.

For a path $\pi$ from the conclusion to an assumption in $\Pi_j^\circ$, we write $\tilde{\pi}$ for the corresponding path in $\Pi$. We extend this notation to a finite composition of $\pi$'s. By the correspondence ($\tilde{\gamma}$), a stage-number inductive atomic formula in $\Pi_j^\circ$ corresponds to an inductive atomic formula in $\Pi$, and a path, a trace, and a progressing trace in $\Pi_j^\circ$ correspond to the same kind of objects in $\Pi$.

**Definition 5.3** For a finite composition $\pi$ of paths in $\{\Pi_j^\circ \mid j \in K\}$ such that $\tilde{\pi}$ is a path in the infinite unfolding of $\Pi$, we define the *path relation* $\succ_{\pi}$ by

$$x \succ_{\pi} y \equiv |x| = |\tilde{J}_2| \wedge |y| = |\tilde{J}_1| \wedge \bigwedge_{F(q_1, q_2)} (x)_{q_2} > (y)_{q_1} \wedge \bigwedge_{G(q_1, q_2)} (x)_{q_2} = (y)_{q_1}$$

where $J_1$ and $J_2$ are the top and bottom sequents of $\pi$ respectively, $\tilde{J}_1$ and $\tilde{J}_2$ are those of the path $\tilde{\pi}$, $F(q_1, q_2)$ is that there is some progressing trace from
the q₂-th atomic formula in $\tilde{J}_2$ to the q₁-th atomic formula in $\tilde{J}_1$, $G(q_1, q_2)$ is
that there is some non-progressing trace from the q₂-th atomic formula in $\tilde{J}_2$ to
the q₁-th atomic formula in $\tilde{J}_1$.

We define $B_1$ as the set of paths from conclusions to assumptions in $\Pi_j^\circ$ ($j \in K$). We define $B$ as the set of finite compositions of elements in $B_1$ such that if $\pi \in B$ then $\tilde{\pi}$ is a path in the infinite unfolding of $\Pi$.

**Definition 5.4** For $\pi \in B$, define $x \succ_{\pi} y$ by

$$x \succ_{\pi} y \equiv (x)_0 = j \wedge (y)_0 = f(i) \wedge (x)_1 \succ_{\pi} (y)_1,$$

where $J_{1i}$ is the top sequent of $\tilde{\pi}$, and $J_{2j}$ is the bottom sequent of $\tilde{\pi}$.

Note that $(\cdot)_0$ and $(\cdot)_1$ are operations for a number that represents a sequence of numbers defined in Section 3. The first element is a companion number.

**Lemma 5.5** $\{>_{\pi} | \pi \in B\}$ is finite.

*Proof.* Define $C_n$ as $\{>_{\pi_1 \dots \pi_m} | m \le n, \pi_i \in B_1\}$. Since $>_{\pi}$ is a relation on $N \times N \leq^p$ where $p$ is the maximum number of inductive atomic formulas in the antecedents of $\Pi$, there is $L$ such that $|C_n| \le L$ for all $n$. Then we have the least $n$ such that $C_{n+1} = C_n$. Then $|\{>_{\pi} | \pi \in B\}| = |C_n|$. $\square$

The next lemma is the only lemma that uses the global trace condition.

**Lemma 5.6** For all $\pi \in B$, there is $n > 0$ such that $\vdash_{\text{HA}} \text{Ind}(U, >_{\pi}^n)$.

We define $>_{\Pi}$ as $\bigcup\{>_{\pi} | \pi \in B\}$. Note that $>_{\Pi}$ is transitive, since the top sequent of $\pi_1$ is the bottom sequent of $\pi_2$ by the first element, and $((>_{\pi_1}) \circ (>_{\pi_2})) \subseteq (>_{\pi_1 \pi_2})$.

## 5.3 Proof Transformation

This section gives proof transformation.

The next lemma shows we can replace (Case) rules of $\mathbf{CLJID}^{\omega} + \mathbf{HA}$ by
(Ind) rules of $\mathbf{LJID} + \mathbf{HA}$.

**Lemma 5.7** If there is a proof with some assumptions and without any buds in $\mathbf{CLJID}^{\omega} + \mathbf{HA}$, then there is a proof of the same conclusions with the same assumptions in $\mathbf{LJID} + \mathbf{HA}$.

The next is a key lemma and shows each bud in a cyclic proof is provable in $\mathbf{LJID} + \mathbf{HA}$, which is proved by using Theorem 2.15.

**Lemma 5.8** For every bud $J$ of a proof in $\mathbf{CLJID}^{\omega} + \mathbf{HA}$ and fresh variables $\vec{v}$, $(J) \stackrel{\circ}{\rightarrow} v$ is provable in $\mathbf{LJID} + \mathbf{HA}$.

The next is the main proposition stating that a cyclic proof is transformed into an $(\mathbf{LJID} + \mathbf{HA})$-proof with stage-number inductive predicates.
**Proposition 5.9** If a sequent *J* is provable in **CLJID**<sup>ω</sup> + **HA** + (Σ<sub>*N*</sub> ∪ {**P**′}, Φ<sub>*N*</sub> ∪ {**P**}}), then *J* is provable in **LJID** + **HA** + (Σ<sub>*N*</sub> ∪ {N', **P**}, **P**'}, Φ<sub>*N*</sub> ∪ {**P**}, **P**'})} where N', **P**' are the stage-number inductive predicates of *N*, **P**.

The next shows conservativity for stage-number inductive predicates.

**Proposition 5.10 (Conservativity of N' and P'')** Let Σ = Σ<sub>N</sub> ∪ {Q̄, P̄, P̄'}, Φ = Φ<sub>N</sub> ∪ {P̄, P̄'}, Σ' = Σ ∪ {N', P̄''}, and Φ' = Φ ∪ {N', P̄''}. Then LJID + HA + (Σ', Φ') is conservative over LJID + HA + (Σ, Φ).

**Proof of Theorem 4.4.** (1) **LJID** + **HA** + (Σ, Φ) to **CLJID**<sup>ω</sup> + **HA** + (Σ, Φ).

For this claim, we can obtain a proof from the proof of Lemma 7.5 in [11] by
restricting every sequent into intuitionistic sequents and replacing **LKID**+(Σ, Φ)
and **CLKID**<sup>ω</sup> + (Σ, Φ) by **LJID** + (Σ, Φ) and **CLJID**<sup>ω</sup> + (Σ, Φ) respectively.

(2) CLJID<sup>ω</sup> + HA + (Σ, Φ) to LJID + HA + (Σ, Φ).

Let Σ' = Σ ∪ {N', $\overline{P''}$} and Φ' = Φ ∪ {N', $\overline{P''}$}. Assume *J* is provable in **CLJID**<sup>ω</sup> + **HA** + (Σ, Φ). By Proposition 5.9, *J* is provable in **LJID** + **HA** + (Σ', Φ'). By Proposition 5.10, *J* is provable in **LJID** + **HA** + (Σ, Φ). □

**6 Related Work**

The conjecture 7.7 in [11] (also in [8]) is that the provability of **LKID** is the
same as that of **CLKID**<sup>ω</sup>. In general, the equivalence was proved to be false
in [4], by showing a counterexample. However, if we restrict both systems to
only the natural number inductive predicate and add Peano arithmetic to both
systems, the equivalence was proved to be true in [22], by internalizing a cyclic
proof in ACA<sub>0</sub> and using some results in reverse mathematics. [5] proved that if
we add Peano arithmetic to both systems, **CLKID**<sup>ω</sup> and **LKID** are equivalent,
namely the equivalence is true under arithmetic, by showing arithmetical Ramsey
theorem and Podelski-Rybalchenko theorem for induction.

This paper shows that similar results as shown in [5] hold for intuitionistic
logic, namely, the provability of **LJID** is the same as that of **CLJID**<sup>ω</sup> if we add
Heyting arithmetic to both systems.

The results of this paper immediately give another proof to the equivalence
under arithmetic for classical logic shown in [5] by using the fact Γ ⊢<sub>CLKID<sup>ω</sup>+PA</sub> Δ implies E, Γ,¬Δ ⊢<sub>CLJID<sup>ω</sup>+HA</sub> for some finite set E of excluded middles.

By taking $\overline{Q}$ and $\overline{P}$ to be empty in Theorem 4.4, we have conservativity of
$\mathbf{CLJID}^{\omega} + \mathbf{HA}$ over $\mathbf{LJID} + \mathbf{HA}$ with only the inductive predicate $N$, which
answers the question (iv) in Section 7 of [22].

[17] presented the first logical system for inductive/coinductive predicates.
[19] also gave a similar system. They are both based on a finite system with unfold
and fold, and limited to propositional logic. [23] showed the completeness of the
system by using a cyclic proof system but it is also limited to propositional logic.
[15, 2] investigated cyclic proof systems for inductive/coinductive predicates. [14,
1] also used cyclic proof systems for inductive/coinductive predicates to show
some completeness results. But these systems are all limited to propositional
logic.
# 7 Conclusion

We have first shown intuitionistic Podelski-Rybalchenko theorem for induction in HA, and we have secondly shown the provability of the intuitionistic cyclic proof system is the same as that of the intuitionistic system of Martin-Lof's inductive definitions when both systems contain HA. We have also constructed a cyclic proof system $\mu\nu$LK for stream predicates.

One future work would be to construct a cyclic proof system for coinductive predicates in a general way and show the equivalence between the cyclic proof system and other logical systems for coinductive predicates.

# References

1. B. Afshari and G. Leigh, Cut-free Completeness for Modal Mu-Calculus, In: *Proceedings of LICS 2017* (2017) 1–12.

2. D. Baelde, A. Doumane, and A. Saurin, Infinitary Proof Theory: the Multiplicative Additive Case, In: Proceedings of 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), LIPIcs 62 (2016) 42:1–42:17.

3. S. Berardi and S. Steila, An intuitionistic version of Ramsey's Theorem and its use in Program Termination, *Annals of Pure and Applied Logic* **166** (2015) 1382–1406.

4. S. Berardi and M. Tatsuta, Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proof System, In: *Proceedings of FoSSaCS 2017*, LNCS 10203 (2017) 301–317.

5. S. Berardi and M. Tatsuta, Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic, In: *Proceedings of Thirty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2017)* (2017) 1–12.

6. S. Berardi and M. Tatsuta, Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic, arXiv:1712.03502, 2017.

7. J. Brotherston, Cyclic Proofs for First-Order Logic with Inductive Definitions, In: *Proceedings of TABLEAUX 2005*, 2005.

8. J. Brotherston, Sequent calculus proof systems for inductive definitions, PhD. thesis, University of Edinburgh, 2006.

9. J. Brotherston, R. Bornat and C. Calcagno, Cyclic Proofs of Program Termination in Separation Logic, In: *Proceedings of POPL 2008*, 2008.

10. J. Brotherston, D. Distefano and R.L. Petersen, Automated Cyclic Entailment Proofs in Separation Logic, In: *Proceedings of CADE-23*, 2011.

11. J. Brotherston and A. Simpson, Sequent calculi for induction and infinite descent, *Journal of Logic and Computation* **21** (6) (2011) 1177–1216.

12. J. Brotherston, N. Gorogiannis and R.L. Petersen, A Generic Cyclic Theorem Prover, In: *Proceedings of APLAS 2012*, 2012.

13. A. Doumane, D. Baelde, L. Hirschi, and A. Saurin, Towards completeness via proof search in the linear time $\mu$-calculus, In: *Proceedings of LICS 2016* (2016) 377–386.

14. A. Doumane, Constructive completeness for the linear-time $\mu$-calculus, In: *Proceedings of LICS 2017* (2017) 1–12.
15. J. Fortier and L. Santocanale, Cuts for circular proofs: semantics and cut-elimination, In: Proceedings of Computer Science Logic 2013 (CSL 2013), LIPIcs 23 (2013) 248–262.

16. C.G. Jockusch, Jr, Ramsey's theorem and recursion theory, Journal of Symbolic Logic 37(2) (1972) 268–280.

17. D. Kozen, Results on the propositional mu-calculus, Theoretical Computer Science 27 (1983) 333-354.

18. P. Martin-Löf, Haupstatz for the intuitionistic theory of iterated inductive definitions, In: Proceedings of the Second Scandinavian Logic Symposium, North-Holland, (1971) 179-216.

19. D. Niwiński and I. Walukiewicz, Games for the μ-calculus, Theoretical Computer Science 163 (1997) 99-116.

20. A. Podelski and A. Rybalchenko, Transition Invariants, In: Proceedings of 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 32-41 (2004).

21. J.R. Shoenfield, Mathematical Logic, Addison-Wesley, 1967.

22. A. Simpson, Cyclic Arithmetic is Equivalent to Peano Arithmetic, In: Proceedings of FoSSaCS 2017 (2017) 283–300.

23. I. Walukiewicz, Completeness of Kozens axiomatisation of the propositional μ-calculus, Information and Computation 157 (2000) 142-182.