Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs
Stefano Berardi Makoto Tatsuta
cs.LO

=10000 =10000

#1



ℋ
𝒰
ℛ
ℳ
𝒟
codom
id




 s



dom
codom




→
































































































































































                                

























































































#1#1
Candidates




root
true
sortll
sortll
avl
sortavl

NC
PI
DPI
SL
#1SLA#1
null
pred 
Z
ML
NML
true
false
mod 
P_S
P_N




nll



SLRD_btw
BTW
Loc




Connected
Eststablished
Valued



nil
=_def
#1∞_#1
Stores
SVars
Val
MSO
Sep
THeaps
Root
TGraph



⟺
⟹
⟸
Norm
Noshare
Roots
Forest
Var
Range
Cell
Tree
Switch
All

tree



#1 
#1#1
#1#1

Node
LL
DSN
DCL
LS
ls

FPV
lfp
IsHeap

  ≡  
null

emp
if 
 then 
 else 
while 
 do 
cons
dispose
Vars
Locs
States
Heaps
FV
true
false
Dom
abort
New
W
Pair
Lh
lh
Elem
EEval

PEval
HEval
Eval
Domain
Exec
Store
Heap
Storecode
Heapcode
Lesslh
Addseq
Separate
Result
Lookup
ChangeStore
ChangeHeap
—*
#1[-1.5pt[#1]-1.5pt]

#1#1












Explicit Induction Is Not Equivalent to Cyclic Proofs]Explicit Induction is Not Equivalent to Cyclic Proofs for Classical Logic with Inductive Definitions

Stefano Berardi]Stefano Berardia 
Makoto Tatsuta]Makoto Tatsutab

aUniversità di Torino
bNational Institute of Informatics / Sokendai, Tokyo 



A cyclic proof system, called CLKID-omega, gives us another way of
representing inductive definitions and efficient proof search.  The
2005 paper by Brotherston showed that the provability of
CLKID-omega
includes the provability of LKID, first order classical logic with inductive definitions in Martin-Löf's style,
and conjectured the
equivalence.  The equivalence has been left an open
question since 2011.
This paper shows that CLKID-omega and LKID are indeed
not equivalent.  This paper considers a statement called 2-Hydra in
these two systems with the first-order language formed by 0, the successor,
the natural number predicate, and a binary predicate symbol used to
express 2-Hydra.  This paper shows that the 2-Hydra statement is
provable in CLKID-omega, but the statement is not provable in
LKID, by constructing some Henkin model where the statement is
false.



[
    [
    December 30, 2023
=====================








§ INTRODUCTION



An inductive definition is a way to define a predicate by an expression which may contain the predicate itself.
The predicate is interpreted by the least fixed point of the defining equation on sets.
Inductive definitions are important in computer science, since they can define useful recursive data structures such as lists and trees.
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 <cit.> is
one of the most popular system of inductive definitions.
This system has production rules for an inductive predicate,
and the production rules determine the introduction rule and the elimination rule for the predicate.

Brotherston <cit.> and Simpson
<cit.> 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), 
or we found anywhere else in the proof-tree,
we can stop.
The induction rule is replaced by a case rule, for this purpose.
The soundness is guaranteed by
some additional condition, called the global trace condition,
which guarantees
that in any infinite path of the proof-tree there is some infinitely decreasing inductive definition.
In general, for proof search,
a cyclic proof system can find an induction formula in a more efficient way
than induction rules in Martin-Löf's style,
since a cyclic proof system does not have to choose a fixed induction formula
in advance.
A cyclic proof system enables efficient implementation of
theorem provers with inductive definitions <cit.>.
In particular, it works well for theorem provers of Separation Logic <cit.>.

Brotherston and Simpson <cit.>
investigated
the system  of inductive definitions in classical logic
for the first-order language,
and
the cyclic proof system  for the same language,
showed the provability of
 includes that of ,
and conjectured the equivalence.
 Since then, the equivalence has been left an open question.
In 2017, Simpson <cit.> proved a particular case
of the conjecture, for the theory of Peano Arithmetic.

 This paper (which is the journal version of <cit.>) shows  and  are indeed not equivalent.
To this aim, we will consider the first-order language L (with equality) formed by 0, the
successor , the natural number predicate , and a
binary predicate symbol p.  We introduce a statement we call
2-Hydra, which is a miniature version of the Hydra problem considered
by Kirby and Paris <cit.>: the proviso
“2” means that we only have two “heads”.
 H as Δ,N(x),N(y)  p(x,y)where Δ is the
set of assumptions for H, is not necessary here
We show that the 2-Hydra
statement is provable in  with language L,
but the statement is not provable in 
with language L. 2-Hydra is similar to the candidate for a counter-example proposed by Stratulat <cit.>. 

The unprovability is shown by constructing some Henkin
model  of  where 2-Hydra is false. 2-Hydra is true in all standard models of , but  is a non-standard model, in which both the universe of  and the interpretation of the predicate  are + Ζ, where  is the set of natural numbers and Ζ is the set of integers. Predicates of  are the equality relation and one “partial bijection”, i.e., a one-to-one correspondence between subsets of the universe of . The proof that  is a Henkin model of  immediately follows from a quantifier elimination result, which holds for all sets of partial bijections which are closed under composition and inverse.

Our quantifier elimination result  is new, to our best knowledge, and it may be of some independent interest. However, our interest is not the quantifier elimination result per se, but rather the identification of this result as a way of proving the unprovability of 2-Hydra in .

The model  also shows a side result, that  is not conservative when we add
inductive predicates. Namely, it is not the case that for any language
L, the system of  with language L and any additional
inductive predicate is conservative over the system of  with
L.

This is the plan of the paper. 
Section  <ref> describes inductive definitions, standard and Henkin models.
Section  <ref> defines the first order system  for inductive definitions,
the 2-Hydra statement, and proves 2-Hydra under two additional assumptions: the 0-axiom and the existence of an ordering ≤.
Section  <ref> defines the system  for cyclic proofs, gives a cyclic proof for the 2-Hydra statement and describes the Brotherston-Simpson conjecture. 
Section  <ref> defines the structure 
and the proof outline that  is a counter model.
Section  <ref> introduces a set of partial bijections in .
Section  <ref> proves a quantifier elimination theorem for any set of partial bijections closed under composition and inverse.
Section  <ref> disproves the Brotherston-Simpson conjecture, by proving that the 2-Hydra statement is not provable in . As a corollary, we have non-conservativity of  with additional inductive predicates.
We conclude in Section  <ref>.



§ INDUCTIVE DEFINITIONS, STANDARD MODELS AND HENKIN MODELS


In this section quickly recall the notion of first order inductive definition, standard model and Henkin model, taken from  <cit.>.  This introduction is only a sketch and we refer to <cit.> for motivations and examples. We fix a first order language Σ with equality that includes inductive predicate symbols P_1, …,P_n of arities k_1, …, k_n.

[Productions of Σ]

An inductive definition set Φ for Σ is a finite set of productions. A production is a rule

    P_i (t⃗)Q_1(u⃗_⃗1⃗)   … Q_h( u⃗_⃗h⃗ )    P_j_1  ( t⃗_⃗1⃗ )    …   P_ j_m (t⃗_⃗m⃗ )

whose premises are a finite sequence of atomic formulas, where 
Q_1, … ,Q_h are ordinary predicate symbols, j_1 , … , j_m ,i ∈{1, … ,n}, P_1, …, P_n are inductive predicate symbols,
and all vector of terms have the appropriate length to match the arities of the predicate symbols.


An example. Let Σ = {0, } be the language with 0 and the successor. Then a set of productions Φ_ describing the inductive predicate  for “being a natural number” is:  

    [      (0) ( x)( x) ]

We call the pair (Σ, Φ) an inductive definition system. The language for (Σ, Φ) is the first order language consisting of all constants, functions and predicates of Σ. The standard interpretation for (Σ, Φ)  is obtained by considering the smallest
prefixed point of a monotone operator ϕ_Φ defined below. From now on, we denote the powerset of a set X by (X). In the next definition we suppose that ρ is a valuation from finitely many variables to the universe, and that ρ is applied componentwise on a vector of terms.

[Monotone Operator ϕ_Φ]

Let   with domain  be a first-order structure for Σ, and for each i ∈{1, … ,n}, let k_i be the arity of
the inductive predicate symbol  P_i. 


  * Φ_i ={ϕ∈Φ|the conclusion of ϕ is P_i}.

  * Assume Φ_i has the form {Φ_i,r|  1 ≤ r ≤ |Φ_i|}. For each rule Φ_i,r of the form shown in
<ref>, we define 
Φ _i,r :  
(^k_j_1 ) ×…×(^k_j_n ) 
→(^k_i ) 
by:

    Φ_i,r (X_1  … ,X_n)
    = 
    {ρ(t⃗) |ρ,   ρ( t⃗_⃗1⃗ ) ∈ X_j_1 ,  … ,  ρ(t⃗_⃗m⃗ ) ∈ X_j_m,


    Q^_1 (ρ(u⃗_⃗1⃗)),  … ,  Q^_h (ρ( u⃗_⃗h⃗ )) }.


  * We define Φ_i for each
i ∈{1, … ,n} with the same domain and codomain, by:

    Φ_i(X_1, … ,X_n)
    =
    ⋃_1 ≤ r ≤ |Φ_i|Φ_i,r (X_1, … ,X_n).


  * We define ϕ _Φ, with domain and codomain
(^k_1 ) ×…×(^k_n ), by:
ϕ _Φ(X_1, … ,X_n)=(Φ_1(X_1, … ,X_n), … ,Φ_n(X_1, … ,X_n)).



We extend union and subset inclusion to the corresponding pointwise operations on n-tuples of sets: in this way (ϕ_Φ) becomes a complete lattice. A prefixed point of ϕ_Φ is X⃗∈(ϕ_Φ) such that X⃗⊆ϕ_Φ(X⃗). The map ϕ_Φ is monotone on a complete lattice. Thus,  ϕ_Φ has a unique smallest prefixed point by the Tarski Fixed Point Theorem. We define the standard model for (Σ, Φ) from such a prefixed point.

[Standard model]
A first-order structure  with universe   is said to be a standard model for (Σ, Φ) if the vector (P^_1, …, P^_n) of interpretations of P_1, …, P_n in  is the smallest prefixed point of ϕ_Φ.


The Henkin class for  is a family of subsets _k ⊆^k, indexed on k ∈, including all graphs of predicates of  and closed w.r.t. all first order connectives, as we make precise below.

[Henkin class for a first order structure ]

Le   with domain  be a structure for Σ. Assume k,h ∈, x⃗ = x_1, … ,x_k are variables, t_1, …, t_h are terms and d⃗ = d_1, … ,d_k ∈. A Henkin class for  is a family of sets 
= {_k  |  k  ∈} 
such that, for each k  ∈: _k ⊆(^k);


  * {(d,d)  | d  ∈}∈_2;

  * if Q ∈Σ is any predicate symbol of arity k then Q_∈_k ;

  * if R ∈_k +1 and d  ∈ then {(d⃗)  |  (d⃗,d) ∈ R}∈_k;

  * if R ∈_h  and  t_1[x⃗], … ,t_h[x⃗] are terms then
{ (d⃗)  |  ( t^_1 [ d⃗], … , t^_h [ d⃗]) ∈ R }∈ H_k;

  * if R ∈_k  then (^k ∖ R) ∈_k;

  * if R_1,R_2  ∈_k  then R_1 ∩ R_2  ∈_k;

  * if R ∈_k +1 then {(d⃗) |∃ d∈. (d⃗,d) ∈ R}∈_k.



The smallest Henkin family _ for a structure , and the only Henkin family we will consider later, is the set of definable sets in .

[The Henkin family _]
 
Assume  is a structure of language Σ. Let k ∈. We write u⃗, v⃗ for two vectors of elements in  of the same length as the vectors of variables x⃗, y⃗. Then the family of sets _ = {_k | k ∈} is defined by:

    _k = { {u⃗∈^k  | F[u⃗,v⃗/x⃗,y⃗] 
    }  |   
    (F∈ L(Σ))  ∧((F) ⊆x⃗, y⃗)  ∧(v⃗∈) }



In a Henkin Model for Σ, instead of requiring that (P^_1, …, P^_n) is the smallest prefixed points of ϕ_Φ w.r.t. all subsets of , we require that it is the smallest prefixed points w.r.t. all sets in some Henkin class _k for .

[Henkin model]
Let  be a first-order structure for (Σ, Φ) and  be a Henkin class for . Then (,) is a
Henkin model for (Σ, Φ) if (P^_1, …, P^_n) is the least prefixed point of ϕ_Φ⌈, where ϕ_Φ⌈ is ϕ_Φ with each argument in (^k) being restricted to _k.
We say  is a Henkin model when (, _) is a Henkin model.


In a Henkin model the interpretation of P_1, …, P_n may be larger than the smallest prefixed points of ϕ_Φ. Some Henkin models are not standard models, and this paper will discuss a Henkin model which is not a standard model.



§ THE SYSTEM  FOR INDUCTIVE DEFINITIONS AND THE 2-HYDRA STATEMENT


In this section we quickly introduce some definitions and results of <cit.>, in order to make the paper self-contained. We describe (Σ, Φ), formalizing the notion of inductive proof for a first order language Σ with equality, and for the the set of productions Φ (see section <ref>). We state that  is sound and complete with respect to Henkin models (again, see <cit.>). Then we formalize the 2-Hydra statement, which is our work. In later sections we will prove that 2-Hydra is false in some Henkin model, and we use 2-Hydra to distinguish between provability in  and cyclic proofs.



We write sequents of the form Γ⊢Δ where Γ, Δ are finite sets of formulas. We write Γ[θ ] for the application of substitution θ to all formulas in Γ.
For first-order logic with equality, we use the (standard) sequent calculus rules, with contraction implicitly given. (Σ, Φ) has a rule for 
substitution, and rules for equality. There are logical rules and rules for inductive predicates.

Structural and logical rules of  are the following.




Structural rules:


    [               [Γ∩Δ≠∅    ()]
    Γ⊢Δ [Γ⊆Γ'    Δ⊆Δ'     ()]
    Γ' ⊢Δ'Γ⊢Δ;                                ;        [()]
    Γ⊢ΔΓ⊢Δ, F     F,Γ⊢Δ             [()]
     Γ[θ] ⊢Δ[θ]Γ⊢Δ;                                 ]


  


Logical rules:


    [                                 [( L)]Γ,  F ⊢ΔΓ⊢ F, Δ                                   [( R)]Γ⊢ F, ΔΓ,F ⊢Δ;                                                      ;                   [(∨ L)]Γ, F ∨ G ⊢ΔΓ, F ⊢Δ   Γ, G ⊢Δ                          [(∨ R)]Γ⊢ F ∨ G, ΔΓ⊢ F, G, Δ;                                                      ;                          [(∧ L)]Γ, F ∧ G ⊢ΔΓ, F, G ⊢Δ                   [(∧ R)]Γ⊢ F ∧ G, ΔΓ⊢ F, Δ   Γ⊢ G, Δ;                                                      ;                   [(→ L)]Γ, F → G ⊢ΔΓ⊢ F, Δ   Γ, G ⊢Δ                         [(→ R)]Γ⊢ F → G, ΔΓ, F ⊢ G, Δ;                                                      ;             [(x ∉(Γ,Δ)     (∃ L)]
    Γ, ∃ x. F ⊢ΔΓ, F ⊢Δ                        [(∃ R)]
    Γ⊢∃ x.F, ΔΓ⊢ F[t/x], Δ;                                                      ;                      [(∀ L)]
    Γ, ∀ x. F ⊢ΔΓ, F[t/x] ⊢Δ              [(x ∉(Γ,Δ)      (∀ R)]
    Γ⊢∀ x.F, ΔΓ⊢ F, Δ;                                                      ; [(=L)]Γ[t/x,u/y], t=u⊢Δ[t/x,u/y]Γ[u/x,t/y]⊢Δ[u/x,t/y]                                       [(=R)]Γ⊢ t=t, Δ ]






We define left- and right-introduction rules for induction. For each production in Φ of the form:

    P_i (t⃗[x⃗])Q_1(u⃗_⃗1⃗[x⃗])  …  Q_h( u⃗_⃗h⃗[x⃗] ) P_j_1  ( t⃗_⃗1⃗[x⃗] )  …  P_j_m (t⃗_⃗m⃗ [x⃗])

we include the following right-introduction rule for  P_i in (Σ, Φ):

    Γ⊢Δ, P_i (t⃗[u⃗])Γ⊢Δ, Q_1(u⃗_⃗1⃗[u⃗])  …Γ⊢Δ,Q_h( u⃗_⃗h⃗[u⃗] )     Γ⊢Δ, P_j_1  ( t⃗_⃗1⃗[u⃗] )  …Γ⊢Δ, P_j_m (t⃗_⃗m⃗[u⃗] )

We assume that u⃗ is a vector of terms of the same length as x⃗.

We express left-introduction rules for inductive predicates in the form of induction rules for mutually depending predicates. We define mutual dependency first.

[Mutual dependency <cit.>]
Let P_i, P_j be inductive predicate symbols of Σ. 


  * P_j is a premise of P_i if P_i  occurs in the conclusion of some production in Φ, and P_j occurs among the premises
of that production. 

  * P_i  and P_j are mutually dependent if there is a chain for the “premise relation” from P_i to P_j, and conversely.



In order to define the left-introduction rule for any inductive predicate P_j, we first
associate with every inductive predicate  P_i  a tuple z⃗_i of k_i distinct variables (called induction variables), where k_i is the arity of  P_i, and a formula (called an induction hypothesis) F_i, possibly containing (some of) the induction variables z⃗_i. We define a formula G_i for each i ∈{1, … ,n} by:
G_i= F_i if  P_i  and P_j are mutually dependent
and  G_i= P_i (z⃗_i) otherwise.
We write G_it⃗ for G_i[t⃗/z⃗_i], and the same for F_i. Then the induction rule for P_j has the following form:

    Γ,P_ju⃗⊢Δ   Γ,F_ju⃗⊢Δ

The premise Γ,F_ju⃗⊢Δ is called the major premise of the rule, and for each production
of Φ having in its conclusion a predicate P_i  that is mutually dependent with P_j, say:

    P_i (t⃗[x⃗])Q_1(u⃗_⃗1⃗[x⃗])   …  Q_h( u⃗_⃗h⃗[x⃗] )    P_j_1  ( t⃗_⃗1⃗[x⃗] )   …  P_j_m (t⃗_⃗m⃗ [x⃗])

there is a corresponding minor premise:

    Γ,Q_1u⃗_⃗1⃗[y⃗],  …  ,Q_h u⃗_⃗h⃗ [y⃗],G_j_1   t_1 [y⃗],  …  ,G_ j_mt⃗_⃗m⃗ [y⃗] ⊢ F_it⃗[y⃗],Δ

where y⃗ is a vector of the same length as x⃗
for fresh variables.

An alternative formalization of induction is the induction schema. 

[Induction schema]

The induction schema  is the following set of axioms: 

    →∀y⃗.(P_it⃗(y⃗) → F_it⃗(y⃗)),     i∈{1, …, n}
 
 is defined to satisfy the induction schema if and only if all formulas of the induction schema are true in .


The axioms in the induction schema derive all instances of the induction rule and conversely. 
By definition unfolding we have the following. If a structure 
has 0,s,N and the inductive predicate symbol is only N,
then (,_) is
a Henkin model if and only if: if F[0/x] is true, and for all closed
terms t if F[t/x] is true then F[ t/x] is true, then we have
F[u/x] true, for all closed terms u. Thus, such a structure  is a Henkin
model if and only if  satisfies the induction
schema. The same remark applies to all inductive predicates.

We write A_1, …, A_n
 B for A_1 ∧…∧ A_n  C and ∀
x_1, …, x_n ∈.  A for ∀ x_1.  ….  ∀
x_n. ((x_1) ∧…∧(x_n) 
A). 
We abbreviate 1 and 2 for 0 and 0 respectively.

The case of the predicate . The induction rule for the `natural number' predicate  
(section  <ref>) is:

    [( N)]Γ,Nt⊢ΔΓ⊢ F0,Δ   Γ,Fx⊢ Fsx,Δ   Γ,Ft⊢Δ


where x is fresh and F is the induction formula associated with the predicate . The induction schema for  is the set of axioms 

    F0, (∀ x.Fx→ Fsx)  →∀ x.(Nx → Fx)
 
for any formula F.  satisfies the induction schema for  if and only if F0, (∀ x.Fx→ Fsx)  →∀ x.(Nx → Fx).

[Validity and Henkin Validity]
A sequent Γ⊢Δ is said to be valid if it is true in all standard models. Let (,) be a Henkin model for (Σ,Φ). A sequent Γ⊢Δ is said to be true in (,) if, for all valuations ρ for , whenever _ρ J for all J  ∈Γ  then _ρ K for some K  ∈Δ. A sequent is said to be Henkin valid if it is true in all Henkin models. 


A derivation tree is a tree of sequents in which each sequent is obtained as the
conclusion of an inference rule with its children as premises. A proof in  is a finite
derivation tree all of whose branches end in an axiom. The basic result about provability is:


Γ⊢Δ is a sequent provable in  if and only if Γ⊢Δ is Henkin valid.


We refer to <cit.> for a proof. Completeness does not hold for (standard) validity: there are valid sequents with no proof in . One example is the sequent ⊢ H, where H is the 2-Hydra statement, defined below.



 §.§ The Hydra Problem

The Hydra of Lerna was a mythological monster, popping two smaller heads whenever you cut one. It was a swamp creature (its name means “water”) and possibly was the swamp itself, whose heads are the swamp plants, with two smaller plants growing whenever you cut one. The original Hydra was defeated by fire, preventing heads from growing again. In the mathematical problem of Hydra, we ask whether it is possible to destroy an Hydra just by cutting heads.

Kirby and Paris <cit.> formulated the Hydra problem as a statement for mathematical trees. We are interested about making Hydra a problem for natural numbers, representing the length of a head, and restricting to the case when the number of heads is always 2. We call our statement 2-Hydra. It is a miniature version of the Kirby-Paris statement. 2-Hydra will give a counterexample to the Brotherston-Simpson conjecture.



 §.§ The 2-Hydra Statement


In this subsection we give the 2-Hydra statement,
which is a formula saying that any 2-Hydra eventually loses its two heads.

Let Σ_ be the signature {0, , p, N },
which are zero, the successor, an ordinary binary predicate symbol
p, and an inductive predicate  for natural numbers.
The logical system (Σ_,Φ_) is
defined as the system  with the signature Σ_N and the
production rules Φ_N for  (see section
<ref>). We define the (0, )-axioms in this
language as the axioms “0 is not successor” or ∀ x ∈.    x ≠ 0, and “successor is injective”, or
∀ x, y ∈.   x=  y  x = y.

We consider a formal statement H for 2-Hydra. H says that the number of heads
is always 2, and we can win a game having the following rules:


  * When both heads have positive length, we cut them off completely.
Then the first head shrinks to become 1 unit shorter than the previous head and the second head shrinks to become 2 units shorter than the previous head, if these shorter lengths exist.
Otherwise we win.

  * When there is a unique head of positive length, we cut it off completely.
Then the first head shrinks to become 1 unit shorter than the original head of
positive length and the second head shrinks to become 2 units shorter than the original head of positive length, if these shorter lengths exist.
Otherwise we win.

We express H by saying that some set of transformations eventually reaches a winning condition. The winning condition is the union of the winning conditions for the points 1 and 2 above. Let n, m ∈. The the winning conditions and the transformations  are:  


  * we win if we reach the cases: (0,0), (1,0) and (x,1) for any x ∈. 

  * if n ≥ 1 and m ≥ 2 then
(n,m) ↦ (n-1,m-2); 

  * if m ≥ 2 then (0,m) ↦ (m-1,m-2);

  * if n ≥ 2 then (n,0) ↦ (n-1,n-2); 

The four cases listed above are pairwise disjoint and cover all (n, m) ∈^2. For instance, case 4 is disjoint from cases 1, 2, 3. When we win, no transformation applies. Indeed, no transformation applies from (0,0) and (1,0), because if m=0 we require n ≥ 2. No transformation applies when m=1, because transformations 1 and 2 require m ≥ 2, and transformation 3 requires m=0. We define H by a formula in  the language Σ_. 

[2-Hydra Statement H]

We define
H = (H_a,H_b,H_c,H_d ∀ x,y ∈.  p(x,y)), where H_a,H_b,H_c,H_d are:


  * ∀ x ∈.   p(0,0) ∧ p(1,0) ∧ p(x,1),

  * ∀ x,y ∈.   p(x,y)  p( x,  y),

  * ∀ y ∈.   p( y,y)  p(0, y),

  * ∀ x ∈.   p( x,x)  p( x,0).



For a closed term of {0,},
its length is defined as the number of symbols  in it. Assume n, m are closed terms of {0,}. Then p(n,m) means that we win 
for the 2-Hydra game beginning with the first head being of length n
and the second head being of length m.
For all closed terms n,m of {0,}, there is a formula among H_a,H_b,H_c,H_d having some instance inferring p(n,m). The formula is unique if we assume the standard (0,)-axioms. 
H_a says that p(0,0), p(1,0) and p(n,1) for any closed term n are true, and expresses the winning condition of the game. Each instance of H_b,H_c,H_d is some implication 
p(n',m') → p(n,m) such that the maximum length of n',m' is smaller than 
the maximum length of n,m. Thus, for all closed terms n,m of {0,}, 
p(n,m) is true in all standard models of (Σ_N,Φ_N): it is shown by induction on the maximum length of n,m. An example: we derive p(1,4) by H_b and p(0,2), the latter by H_c and p(1,0), the latter by H_a. In a standard model, the interpretation of  is the set of interpretations of closed terms of {0,}: as a consequence, 2-Hydra is is true in all standard models of (Σ_, Φ_).

However, we will prove that (Σ_, Φ_) + (0,)-axioms does not prove 2-Hydra. Remark that the (0,)-axioms define a proper extension of (Σ_, Φ_). These axioms cannot be proved in (Σ_,
Φ_), because each of them fails in the following models.


  * the model with domain
= _ = {0}, 0=0; 

  * the model with domain = _ = {0,  0}, 0 ≠
0 and 0 =  0. 

Compared with Peano Arithmetic , in
(Σ_, Φ_) + (0,)-axioms we do
not have a sum or a product on ,
and we do not have inductive predicate symbols for addition, multiplication, 
or order.



 §.§ 2-Hydra is provable under additional assumptions

As an example of a formal proof in , we prove 2-Hydra under two additional assumptions: the inductive predicate ≤ and the 0-axiom, which will be defined.

The inductive predicate ≤ is defined from the following production rules:

    x ≤ x    x ≤ yx ≤ y

We call the set of these production rules Φ_≤.
The 0-axiom is: ∀ x ∈.   x ≠ 0.
In (Σ_N+{≤},Φ_N+Φ_≤), we can show
any number ≤ 0 is only 0.



, Nx,Ny, x ≤ y  y=0  x=0




The proof is by induction on the definition of x ≤ y. If y is
x then x=0  x=0, if y is (z) and the property holds
for x, z then we trivially have (z)=0  x=0 by
.


The next theorem shows 2-Hydra is provable in  with ≤.

H is provable in (Σ_N+{≤},Φ_N+Φ_≤).


  
Let Ĥ = H_a,H_b,H_c,H_d be the list of 2-Hydra axioms in Def. <ref>.
We will prove the equivalent sequent Ĥ, Nx,Ny  p(x,y).
We will first show ∀ n.   (n ≥ x  n ≥ y  p(x,y))
by induction on n.



  * Case 1: n=0. Then x=y=0 by Lemma <ref>, therefore p(x,y) by H_a.

  * Case 2: n= n'.



  * Sub-case 2.1: y=0.
  
  
  * Sub-sub-case 2.1.1. x=0 or x= 0. By H_a.
  
  * Sub-sub-case  2.1.2. x= x”. Then p( x”,x”) by induction hypothesis, hence p(x,0) by H_d.
  
  

  * Sub-case 2.2. y= 0. By H_a.


  * Sub-case 2.3. y= y”.
  
    
  * Sub-sub-case  2.3.1. x=0. Then p( y”,y”) by I.H., hence
      p(0,y) by H_c.
    
  * Sub-sub-case  2.3.2. x= x'. Then p(x',y”) by I.H., therefore p(x,y) by H_b.
    
   


By principal induction on x and secondary induction on y we prove that ∃ n. (n ≥ x) ∧ (n ≥ y). From this statement and the previous one we conclude our claim.




§ THE SYSTEM  AND THE BROTHERSTON-SIMPSON CONJECTURE


In this section we introduce more definitions and results of <cit.>, again in order to make the paper self-contained. We define an infinitary version of  called ^ω, then a subsystem  of the latter called the system of cyclic proofs in <cit.>. We give a cyclic proof of 2-Hydra, which is ours, and eventually we state the Brotherston-Simpson conjecture. 

The proof rules of the infinitary system ^ω  are the rules of , except the induction rules for each inductive predicate. The induction rule (P_i) of  is replaced by the case-split rule:

    [(P_i )]Γ,P_iu⃗⊢Δ

with case distinctions defined as follows. 
For each production having predicate P_i  in its conclusion:

    P_it⃗[x⃗⃗⃗]Q_1 u⃗ _1[x⃗ ]  … Q_h u⃗ _h [x⃗ ] P_j_1t⃗ _1 [x⃗ ]  … P_j_mt⃗ _m [x⃗ ]


there is a case distinction

    Γ, u⃗  = t⃗ [y⃗ ],Q_1u⃗_1[y⃗ ],  …  ,Q_h u⃗ _h [y⃗ ], 
    P_j_1t⃗ _1 [y⃗ ],  …  , P_j_mt⃗ _m [y⃗ ] ⊢Δ

where y⃗ is a vector of distinct variables of the same length as x⃗, and y⃗∩ V = ∅ for V = FV(Γ∪Δ∪{P_iu⃗|  i=1, …, n}).

The formulas P_j_1t⃗ _1 [y⃗ ],  …  , P_j_mt⃗ _m [y⃗ ] occurring in a case distinction are said to be case-descendants of the principal formula P_iu⃗.

The case-split rule for N is

    [x ∉(Γ∪Δ∪{Nt})   (N)]
    Γ,Nt ⊢ΔΓ,t=0⊢Δ   Γ,t=sx,Nx⊢Δ


The formula Nx occurring in the right hand premise is the only case-descendant of the formula Nt
occurring in the conclusion.

The system ^ω  is based upon infinite derivation trees. We
distinguish between `leaves' and `buds' in derivation trees. By a leaf we mean an axiom, i.e. the
conclusion of a 0-premise inference rule. By a bud we mean a sequent occurrence in the tree that
is not the conclusion of a proof rule. 

[^ω  Pre-proof]
An ^ω  pre-proof of a sequent Γ⊢Δ is a (possibly infinite) derivation tree Π, constructed
according to the proof rules of ^ω, such that Γ⊢Δ is the root of Π and Π has no buds.


^ω  pre-proofs are not sound in general: there are 
pre-proofs of any invalid sequent.
The global trace condition is a condition on pre-proofs which ensures their soundness.

A (finite or infinite) path π in a derivation tree Π is a sequence π = (S_i)_0≤ i<α,
for some α∈ N∪{∞}, of sequent occurrences in the tree such that S_i+1 is a child of S_i for all i+1<α.

[Trace]
Let Π be an ^ω  pre-proof and let π = (Γ_i ⊢Δ_i)_i≥ 0 be an infinite path in Π. 
A trace following π is
a sequence τ = (τ_i)_i∈ such that, for all i ∈:


  * τ_i=P_j_it⃗_i  ∈Γ_i, where j_i  ∈{1, … ,n};

  * if Γ_i ⊢Δ_i is the conclusion of () then τ_i=τ_i+1[θ ], where θ  is the substitution associated with the instance of ();

  * if Γ_i ⊢Δ_i is the conclusion of (=L) with principal formula t=u then there is a formula F and variables x,y such that τ_i=F[t/x,u/y] and τ_i+1=F[u/x,t/y];

  * if Γ_i ⊢Δ_i is the conclusion of a case-split rule then either (a) τ_i+1=τ_i or (b) τ_i is the principal formula of the rule instance and τ_i+1 is a case-descendant of τ_i. In the latter case, i is said to be a progress point of the trace;

  * if Γ_i ⊢Δ_i is the conclusion of any other rule then τ_i+1=τ_i.



An infinitely progressing trace is a trace having infinitely many progress points.

[^ω proof]
An ^ω  pre-proof Π is defined to be an ^ω  proof if it satisfies the following global trace condition: for every infinite path π = (Γ_i ⊢Δ_i)_i≥ 0 in Π, there is an infinitely progressing trace following some tail of
the path, π' = (Γ_i ⊢Δ_i)_i≥ k, for some k≥ 0.


Cyclic proofs are a subsystem  of ^ω, defined by
restricting ^ω  to proofs given by regular trees, i.e. those (possibly infinite) trees with only
finitely many distinct subtrees. 

Proofs of  are called cyclic proofs and are represented as finite graphs.

[Companion]
Let B be a bud of a finite derivation tree Π. A node C in Π which is conclusion of some rule is said to be a companion for B if C and B are the same sequent.


[Cyclic pre-proof]
A C^ω  pre-proof Π of Γ⊢Δ is a pair (Π,R), where Π is a finite derivation tree constructed according to the rules of ^ω  and whose root is Γ⊢Δ, and R is a function assigning a companion to every bud node in Π.


By unfolding a cyclic pre-proof to its associated (possibly infinite) tree, cyclic
pre-proofs generate exactly the class of ^ω  pre-proofs given by the regular derivation trees.

[Cyclic proof]
A   proof is defined as a   pre-proof such that its unfolding satisfies the global trace condition.




 §.§ Proof of 2-Hydra Statement in Cyclic-Proof System


The logical systems  (Σ_N,Φ_N) and (Σ_N,Φ_N) are
the systems  and  with the signature Σ_N and 
the set of production rules Φ_N.
In this subsection we give an example of a cyclic proof: a cyclic proof of the 2-Hydra statement in (Σ_N,Φ_N). 


The 2-Hydra statement H is provable in (Σ_, Φ_).



Let the 2-Hydra axioms Ĥ be H_a,H_b,H_c,H_d as in Definition <ref>.

For simplicity, we will write p(x,y) as pxy,
and we will write the use of 2-Hydra axioms 
by omitting (Cut), 
( R),
(∀ R),
(Axiom),
as in the following example.

    Ĥ,N y”,Ny” p0 y”Ĥ,N y”,Ny” p y”y”

Rule (=L) is left-introduction of equality: from Γ[a,b] ⊢Δ[a,b] prove a=b,Γ[b,a] ⊢Δ[b,a]. We will  write a combination of (Case) and (=L) 
as one rule in the following example.

    [Nx]Ĥ,Nx  px0Ĥ, N0  p00
    	   Ĥ,Nx'  p x'0


For saving space, we omit writing Ĥ in every sequent in the next proof figure.
For example, Nx,Ny  pxy actually denotes
Ĥ,Nx,Ny  pxy.

We define a cyclic proof Π of Nx,Ny  pxy, where the mark (a) denotes the bud-companion relation (there are three buds, the only companion is the root). Π is:



    [Ny]
      (a) Nx,Ny  pxyNx  px0Π_1… (a)…          Nx,Ny'  px y'Π_2… (a)… (a)…



where the left sub-proof Π_1 is:



    [Nx]
    Nx  px0N0  p00      -0.5cm 
    	  [Nx']Nx'  p x'0N0  p10   N x”,Nx” p x”0N x”,Nx” p x”x”  (a) Nx,Ny  pxy



and the right sub-proof Π_2 is:



    [Nx]
    Nx,Ny'  px y'N0,Nx  px1   [Nx]
    	 N y”,Nx,Ny” px y”N y”,Ny” p0 y”N y”,Ny” p y”y”  (a) Nx,Ny  pxy   N y”,Nx',Ny” p x' y”Nx',Ny” px'y”  (a) Nx,Ny  pxy




  
Π is a cyclic proof.
We only have to check: the global trace condition holds for any infinite path π in the cyclic proof Π above. We can explicitly describe an infinite trace in π, as follows. We have three possible choices for constructing the infinite path π in the proof: taking the bud in the left, middle, or right of the proof. For a given bud and z_1,z_2 ∈{x,y}, we write z_1  z_2 for a progressing
trace from z_1 in the companion to z_2 in the bud. We write z_1
 z_2,z_3 for z_1  z_2 and z_1  z_3.
For the left bud, there are x  x,y.
For the middle bud, there are y  x,y.
For the right bud, there are both x  x and y  y. We argue by cases.


  * Assume that from some point on the left bud does not appear in a path. Then from this point there is an infinitely progressing trace y  y  y ….

  * Assume that the middle bud from some point on does not appear in a path. Then from this point there is an infinitely progressing trace x  x  x …. 

  * Assume that the left and middle buds appear infinitely many times in a path. Start from x and the left bud if the left bud comes first, and from y and the middle bud if the middle bud comes first, then repeat infinitely one of following operations, according to the current bud.
Take x  x for all left buds, except for the last left bud before
the middle bud comes. Take x  y for this bud.
Take y  y for all middle buds, except for the last middle bud before
the left bud comes. Take y  x for this bud.

In both cases, take x  x or y  y for the right bud, depending if the previous trace was ending in x or in y. Also in this case we defined an infinitely progressing trace starting from some tail of the path, passing infinitely many times though x and though y.

Hence the global trace condition holds.




 §.§ The Brotherston-Simpson Conjecture


 has been often used for formalizing inductive definitions,
while  is another way for formalizing the same inductive definitions,
and moreover  is more suitable for proof search.
This raises the question of the relationship between  and
cyclic proofs: Brotherston and Simpson conjectured the equality for
each inductive definition. The left-to-right inclusion is proved in
<cit.>, Lemma 7.3.1 and in
<cit.>, Thm. 7.6. 
The Brotherston-Simpson conjecture (the conjecture 7.7 in <cit.>) says
that the provability  includes that of .
Simpson <cit.> proved the conjecture in the case of Peano Arithmetic.
The goal of this paper is to prove that the conjecture is false in general, by showing that there is no proof of 2-Hydra in (Σ_N,Φ_N).



§ THE STRUCTURE  FOR THE LANGUAGE Σ_



In this section we define a structure  for the language
Σ_, we prove that  falsifies the 2-Hydra
statement H, and we characterize the subsets of  which
satisfy the induction schema
(definition <ref>).  is not a standard
model of  (in any standard model 2-Hydra would be true). In
the next sections we will prove that (,_) is a Henkin
model of , where _ was defined as the set of definable
sets in  (definition <ref>).



 §.§ Outline for Proof of Non-Provability


In this section we define a counter model , whose predicates are the equality relation and a partial bijection relation (a one-to-one correspondence between some subsets of the universe for ).
We prove that (,_) 
is a Henkin model of (Σ_, Φ_) if we take _ as the set of definable sets of the theory of   (definition <ref>). In fact, we will prove that  satisfies the induction schema for   (definition <ref>). 

On one hand, we prove that in our structure  all definable sets of  (that is, all unary definable predicates of ) are all sets we obtain by adding/removing finitely many elements to: the set , the set of even numbers in , the set of multiples of four in , and so forth, together with their translations and their finite unions. All these sets have measure of a dyadic rational, which is a rational of the form z/2^m for some z ∈Ζ, m∈.
This claim about the measure of definable sets of  is derived as a particular case of a 
quantifier-elimination result (section <ref>), in
which we characterize the sets which are first order definable from a set of
partial bijections closed under composition and inverse (section
<ref>). This result is new, as far as we know. For an
introduction to quantifier-elimination we refer to <cit.>.

On the other hand, section <ref> shows
that a definable set of  with dyadic measure satisfies the induction schema for  (definition <ref>).
Combining them, finally we will show that
 satisfies the induction schema for  and therefore (,_) is 
a Henkin model of (Σ_, Φ_).



 §.§ Definition of the Structure 


Let Ζ be the set of integers. We first define the structure
 for 0,S,p and . 
Later we will define the interpretation of
the predicate p in . We denote the universe of  by
 and we set:

[The sets  and _]



  * = + Ζ = {(1,x) |  x ∈}∪{(2,x) |  x ∈Ζ} (the disjoint union of  and Ζ).

  * 0_ = (1,0) and _(x,y) = (x,y+1).

  * _ =. 


For all n ∈ we set: (x,y) + n = (x,y+n),
and = (2,0) (the element 0 in the component Ζ),
and - n = (2,-n) (the relative integer -n in the component Ζ).
We define the following subsets of :
= {0_ + n |  n ∈}
and
= { - (n+1) |  n ∈}
and
= { + n |  n ∈}.
The sets , ,  are a partition of .

By construction  satisfies the closedness of  under 0 and , and the (0,)-axioms.  is not a standard model of  because the intersection of all subsets of  closed under under 0 and  is ⊂, while _ =.

Even if  is not a standard model of , one can extend  to a Henkin model (,) of (Σ_N, Φ_N), provided that one can identify a suitable Henkin class  of sets in ()
that meets the Henkin closure conditions, and show that _ is the
least prefixed point of ϕ_Φ_N within
this class. We do it by adding to  the interpretation p_ of the binary predicate p, and taking  to be _, the set of all sets first order definable from 0, , =, , p  (definition <ref>). 
We first define a (non-empty) set of points in which the instances of 2-Hydra will be false in . Let r = {(n,2n) |  n ∈}. r is the set of points of the straight line y = 2x which are in ×. We imagine r starting from the infinity, moving at each step from some (a, b) to (a,b), and ending at (0,0).
Given (m_1, m_2) ∈× we define (m_1, m_2) + r = {(m_1 + a, m_2 + b) |  (a,b) ∈ r} and (m_1, m_2) - r = {(m_1 - a, m_2 - b) |  (a,b) ∈ r}. We define three paths in × by π_1 = (0_, ) + r and π_2 = (,0_) + r  and π_3 =(-1, -2) - r. Then π_1 ∪π_2 ∪π_3 is the set of points in which 2-Hydra will be false in the model.

Informally, the reason is that we can move forever along π_1 ∪π_2 ∪π_3 
while “cutting heads”, and we never reach a winning condition. Here is an example, where we write ↦ for a single move of the game, and we use the clause H_c for a head duplication. The infinite sequence of moves is: 


…↦ (0_+2,  +4) ↦ (0_+1, +2) ↦  (0_, ) ↦ (head duplication, by the clause H_c) ( -1,  - 2) ↦ ( - 2,  - 4) ↦…. In the next figure we represent π_1 ∪π_2 ∪π_3 in ×:






(3,3)




(2,2.1)(,)
(-1,2)(0_,)
(1.05,0.15)(,0_)

(-0.4,0.5)
(-0.4,1.5)Ζ^-
(-0.4,2.5)Ζ^+_0

(0.5,-0.3)
(1.5,-0.3)Ζ^-
(2.5,-0.3)Ζ^+_0


(1,0)(0,1)3
(2,0)(0,1)3
(0,1)(1,0)3
(0,2)(1,0)3

(0,0)(1,0)3
(0,0)(0,1)3


(0.5,3)(-1,-2)0.5
(2.5,1)(-1,-2)0.5
(1.9,1.8)(-1,-2)0.4


[160](0,2)(1,2.5)(1.9,1.8)
[160](2,0)(2.5,1)(1.9,1.8)


(0.35,2.5)π_1
(2.25,0.3)π_2
(1.40,1.4)π_3

(0.3,1.8)⇝ head dupl.


(0.4,-2.2)⇝ head dupl.










Eventually, we set 
    p_ = ^2 ∖ (π_1 ∪π_2 ∪π_3)
 We already defined the set _ as  (definition <ref>). We complete the definition of  by:

[The structure ]
= ⟨, 0_, _, _, p_⟩


In the following sections we will check that _ is the least prefixed point of ϕ_Φ_ restricted to the Henkin family _ (definition <ref>), and therefore that (,_) is a Henkin model. In this section we check that H is false in .



H



By Def. <ref>, H = (H_a,H_b,H_c,H_d ∀ x,y ∈.  p(x,y)). We have ∀ x,y ∈.  p(x,y) because _ = while p_⊂^2. In order to prove H, we have to prove that H_a,H_b,H_c,H_d. 



  * H_a. We have to prove that for all x ∈ we have: (0_, 0_), (0_ + 1, 0_), (x, 0_ + 1) ∈ p_, that is: (0_, 0_), (0_ + 1, 0_), (x, 0_ + 1) ∉π_1 ∪π_2 ∪π_3. For all n,m ∈, the sets π_2 ∪π_3 include no point of the form (0_ +n, 0_+m): this proves (0_, 0_), (0_ + 1, 0_) ∉π_1 ∪π_2 ∪π_3. We have (x, 0_ + 1) ∉π_1 ∪π_3 because all points in π_1, π_3 have the second coordinate of the form + z for some z ∈Ζ. We have (x, 0_ + 1) ∉π_2 because all points in π_2 have the second coordinate of the form 0_ + 2n for some n ∈. 


  * H_b. We have to prove that for all a, b ∈ if p_(a,b) then p_(_(a), __(b)), that is: (a,b) ∉π_1 ∪π_2 ∪π_3 implies (_(a), __(b)) ∉π_1 ∪π_2 ∪π_3. By taking the contrapositive, this is equivalent to show: (_(a), __(b)) ∈π_1 ∪π_2 ∪π_3 implies (a,b) ∈π_1 ∪π_2 ∪π_3. We argue by cases. 
Assume (_(a), __(b)) ∈π_1. Then (_(a), __(b)) = (0_ +n+1,  + 2n+2) for some n ∈, hence (a,b) = (0_ +n,  + 2n) ∈π_1. 
Assume (_(a), __(b)) ∈π_2. Then (_(a), __(b)) = ( -1 - n,  -2 - 2n)  for some n ∈, hence (a,b) = ( -1-1-n,  -2-2-n) ∈π_2. 
Assume (_(a), __(b)) ∈π_3. Then (_(a), __(b)) = ( +n+1, 0_ + 2n+2)  for some n ∈, hence (a,b) = ( +n, 0_ + 2n) ∈π_3. 


  * H_c. 
We have to prove that for all b ∈ if p_(_ (b), b) then p_(0_, __(b)), that is: (_ b, b) ∉π_1 ∪π_2 ∪π_3 implies (0_, __(b)) ∉π_1 ∪π_2 ∪π_3. 
By taking the contrapositive, this is equivalent to show:(0_, __(b)) ∈π_1 ∪π_2 ∪π_3 implies (_ (b), b) ∈π_1 ∪π_2 ∪π_3. 
We argue by cases. 
Assume (0_, __(b)) ∈π_1. Then  (0_, __(b)) = (0_, ), hence (_ (b), b) = (-1, -2) ∈π_2. 
Assume (0_, __(b)) ∈π_2 ∪π_3. This cannot be, because all points in π_2, π_3 have the first coordinate of the form + z for some z ∈Ζ.


  * H_d. 
It is similarly proved to the previous case.


_ was defined as the set of definable sets in
  (definition <ref>). 
We prove that (,_) is a Henkin model of .
We have to prove that _ is the
smallest pre-fixed point in _1 for ϕ_Φ_N (definition <ref>). An equivalent condition is to prove the induction schema for N: A[0/x],(∀ x.Nx, A → A[x+1/x]) →∀ x.(Nx → A) for any A ∈ L(). Since the interpretation of N is  itself, we have in fact to prove that all X ∈_1 which are closed under 0 and  are equal to .



 §.§ The Measure for the Subsets of  Closed Under 0 and 


In this subsection we define a sufficient condition for a subset of  to satisfy the induction schema for , by using a finitely additive measure μ(X), defined on
subsets X ⊆.
We will prove that
all definable subsets for  satisfy this condition.

[Measure for Subset of ]
For X ⊆ we set:

    μ(X) = lim_x →∞|  {0_ + n, -n, +n ∈|  n ∈ [0,x] ∩ N }∩ X  |/3(x+1)

whenever this limit exists.


For instance, μ() = 1/3 and if E = {0_, 0_ + 2, …,  -2, ,  + 2, …}, then μ(E) = 1/2.
A dyadic rational is any rational of the form z/2^n for some z ∈Ζ, n ∈. We prove that having a dyadic measure is a sufficient condition for a predicate A[x] to satisfy the induction schema for , namely: A[0], ∀ x. x,A[x] → A[ x]) →∀ x.( x → A[x]) (definition <ref>). Later, we will prove that all definable predicates of  have a dyadic measure, hence they satisfy the induction schema.



If μ(P) is a dyadic rational, then P satisfies the induction schema for .




In order to show the contraposition,
assume P does not satisfy the induction schema.
Then
P is closed under 0,  (hence P ⊇)
and there is some a ∈∖
P. From P ⊇ we deduce that a ∉, hence a =  + z for some z ∈Ζ. Let S_a =
{a, a-1,a-2,a-3, …}: by the contrapositive of closure under
, we deduce that S_a ⊆∖
P. Thus, ∖ P = ⋃{S_a | a ∈∖ P }. If there is a maximum a ∈∖ P we conclude that ∖ P = S_a = {…, a-3,a-2,a-1,a}, while if there is no
maximum for ∖ P then ∖ P = ∪. In the first case
we have μ(∖ P) = 1/3, in the second one
we have μ(∖ P) = 2/3. Thus, if P is a
counter-example to the induction schema for  then μ(P)
= 1/3, 2/3 and μ(P) is not a dyadic rational.


An example: if P = ∪Ζ^+_0, then P is closed under 0,  and -1 ∉P. P does not satisfy the induction schema and μ(P) = 2/3 is not dyadic.



§ THE SET  OF PARTIAL BIJECTIONS ON 



In this section we introduce some set  of partial bijections on
, whose domains have some dyadic rational measure. In
sections <ref>, <ref> we
will prove that all definable sets in  (definition
<ref>) are domains of bijections in
, therefore all these have dyadic rational measure, and by Lemma
<ref> they satisfy the induction schema for 
(definition <ref>). 
We will conclude that (,_) is a Henkin model of
(Σ_, Φ_).

For a set X and binary relations R, S we write: 𝕀_X = {(x,x) |  x ∈ X}, (R) = {x |∃ y.(x,y) ∈ R}, (R) = {y |∃ x.(x,y) ∈ R}, R^-1 = {(y,x)  |  (x,y) ∈ R}, R  S = {(x,z)  |∃ y. ((y,z) ∈ R) ∧ ((x,y) ∈ S) } and R ⌈ X = {(x,y) ∈ R  |  x ∈ X}. 
Note that we write a relation composition R  S in the same order as function composition.



 §.§ The set 



In this subsection we propose a candidate  for the definable
subsets of  (definition
<ref>).  will consist of
, the set including every other elements of 
, the set including every other elements of 
the previous set, and so
forth.  is closed under translations and finite unions and
adding/removing finitely many elements. We first define the
equivalence relation ∼, the subset M(2^r, z) of
, and a set  of subsets for
, then we will define .

For sets I, J we define I J as “(I ∖ J) is finite”: this means “I ⊆ J up to finitely many elements”. We define I ∼ J as I J ∧ J I: this means “I, J are equal up to finitely many elements”.  I ∼ J is equivalent to: (I ∖ J) ∪ (J ∖ I) is finite.
For r ∈, s ∈Ζ we define the following set of elements of :

    M(2^r,s) = 
    {0_ + (2^r*z + s)  |  2^r*z + s ≥ 0 ∧  z ∈Ζ}∪{ + (2^r*z + s)    |  z ∈Ζ}
  
If r=0, s=0 then M(2^r,s) =. We write
 for the set of all sets M(2^r,s), for some r ∈, s
∈Ζ. Since 2^r > 0, all sets M(2^r,s) are infinite.
We define  as the set of subsets which equal
finite unions of sets in  up to finitely many elements.

[The set  ]

D ∈ if and only if D ⊆ and D ∼ (B_1 ∪…∪ B_n) for some B_1, …, B_n ∈. 


We prove that
every set in  has some dyadic rational measure.



Let a_0, a ∈ and D ∈.


  * All finite subsets of  are in .

  * For all a ≥ a_0 there are 0 ≤ b_1 < … < b_i < 2^a such that M(2^a_0,b) = (M(2^a,b_1) ∪…∪ M(2^a,b_i)).

  * For any D there are some a and 0 ≤ b_1 < … < b_i < 2^a such that D ∼ (M(2^a,b_1) ∪…∪ M(2^a,b_i)).

  * μ(D) is some dyadic rational.

  * D satisfies the induction schema for .

  *  is closed under ∼, complement and finite union.






  * ∅ is a finite union, therefore  includes all D ∼∅: that is,  includes all finite subsets of .

  * By repeatedly applying the equation M(2^a,b) = M(2^a,b+2^a) we can assume that 0 ≤ b < 2^a. Then we repeatedly apply the equation M(2^a,b) = M(2^a+1,b) ∪ M(2^a+1,b+2^a).

  * Assume D ∼ (B_1 ∪…∪ B_n). By the point 2 above
there are a_1, …, a_n such that for all a ≥ a_1, …,
a_n and all i=1, …, n there are 0 ≤ b_i,1 < … <
b_i,n_i < 2^a such that B_i = (M(2^a,b_i,1) ∪…∪
M(2^a,b_i,n_i)). It follows our claim with a = max(a_1,
…, a_n).


  * From the point 3 above there are a and 0 ≤ b_1 < … < b_i < 2^a in  such that D ∼ (M(2^a,b_1) ∪…∪ M(2^a,b_i)). For any M(2^a,b) ⊆ we have μ(M(2^a,b) ∩) = 1/2^a. Since 0 ≤ b_1 < … < b_i < 2^a, 
the sets M(2^a,b_1), …, M(2^a,b_i) are pairwise disjoint. From μ(D) finite additive, we deduce that μ(D) = i/2^a.


  * By the point 4 above and Lemma <ref>, 
D satisfies the induction schema for .


  * 

By construction,  is closed under ∼ and finite
union. Thus, we have to prove that if D ∈ then
(∖ D) ∈. By the point 3 above
there are a and 0 ≤ b_1 < … < b_i < 2^a in  such
that D ∼ (M(2^a,b_1) ∪…∪ M(2^a,b_i)). Assume
that [0,2^a)∖{b_1, …, b_i}= {c_1, …, c_j}:
then (∖ D) ∼ (∖
M(2^a,b_1) ∪…∪ M(2^a,b_i)) = (M(2^a,c_1) ∪…∪
M(2^a,c_j)) ∈. By definition, we
conclude that (∖ D) ∈.




 §.§ The Set  of Partial Bijections on 


In this subsection we define a set  of partial bijections on  whose domains are in .

From now on, for n ∈ we call the relation R^n the n-th
power of the relation R. R^n is defined by iterating composition
n times: R^0 is the identity relation and R^n+1 is R^n 
R. We define a negative power of a relation by R^-n =
(R^-1)^n, where R^-1 denotes the inverse of R. Let R_0 =
^2 ∖ p_.  Graphically, R_0 is the
union of the three lines we see in the image in section
<ref>. We will define  as the set of
binary relations on  which include R_0^z for some z
∈Ζ, 
constant addition relation,
plus all relations we obtain from those by restricting the
domain to some D ∈.

We first define some set  of straight lines.  is the set of maps ϕ: →, defined by ϕ(x) =  2^z x + r for some z ∈Ζ and some r ∈.
 is closed under inverse: if ϕ(x) = 2^z x + r, then ϕ^-1(x) = 2^-z x -r/2^z.  is closed under composition: if ϕ_i(x) = 2^z_i x + r_i for i=1,2, then ϕ_2(ϕ_1(x)) = 2^z_1 + z_2 x + (2^z_2 r_1 + r_2).

Let +  = { (i,r)  |  i=1,2 ∧ r ∈}. We extend the notations 0_ + n and + z for n∈, z∈Ζ to the notations 0_ + r = (1,r) ∈ + and  + r = (2,r) ∈ + for r ∈. 

Let ϕ∈, ϕ(x) = 2^z x + r with z ∈Ζ and r
∈. We say that ϕ_ is even if z even,
and that ϕ is odd if z is odd.  For any ϕ∈
we define a map ϕ_:(ϕ) → +. We set ϕ_((i,r)) = (i,ϕ(r)) if ϕ is
even, and if ϕ is odd: ϕ_((1,r)) = (2,ϕ(r)),
ϕ_((2,r)) = (2,ϕ(r)) if r<0, ϕ_((2,r)) =
(1,ϕ(r)) if r ≥ 0. We say that ϕ is sign-preserving at
0_ + a ∈ if a ≥ 0 implies
ϕ(a) ≥ 0, it is sign-preserving at + b ∈ if b ≥ 0 ⇔ϕ(b) ≥ 0. ϕ
is sign-preserving on E ⊆ if ϕ is
sign-preserving on all e ∈ E.

Assume ϕ(x) is sign-preserving on E ⊆. We deduce: if ϕ is even, then ϕ_(∩ E) ⊆ and ϕ_(∩ E) ⊆ and ϕ_(∩ E) ⊆; if ϕ is odd, then ϕ_(∩ E) ⊆ and ϕ_(∩ E) ⊆ and ϕ_(∩ E) ⊆. As a consequence, if ϕ is sign-preserving on E ⊆, and ϕ(E) ⊆ F, and ψ is sign-preserving on F, then (ψϕ)_ and ψ_ϕ_ coincide when restricted to E.

A partial bijection on  is a one-to-one relation between two subsets of . A partial identity on  is the identity relation on some subset of . We now define a set  of partial bijections on  which are the restriction of ϕ_ to some D ∈, for some ϕ∈, and have range some E ∈. 
For instance, one bijection in  is defined by ϕ(x) = 2^2 x, with domain  and codomain M(2^2 ,0), mapping 0_ +n ↦ 0_ +4n and +z ↦ + 4z.

We define “even” and “odd” bijections. They will be restrictions of
an even or odd power of the relation R_0 = ^2 ∖ p_.

We write M for ||.

[The set of partial bijections ]

Let D, E ∈ and ϕ∈, ϕ(x) = 2^z*x + r. 



  * R is a (D,E,ϕ)-bijection if R is in .
and (R)=D, (R)=E and
∀ a ∈ D.∀ b ∈.R(a,b) ⇔
b=ϕ_(a) and ϕ is sign-preserving on E.


  * R is an even (odd) bijection if R is a (D,E,ϕ) bijection
and ϕ is even (odd).

  *  is the set of all (D,E,ϕ)-bijections for D, E ∈ and ϕ∈.



R_0, the complement of p_, is an example of an odd
bijection, shown as follows. R_0 is a partial bijection.
For all n ∈, R_0 maps 0_ + n
↦ + 2n and - (n+1) ↦ - 2(n+1) and
+ n ↦ 0_ + 2n. R_0 is 
the restriction of ϕ_ to , 
where ϕ is the odd map
ϕ(x) = 2^1x.

We will prove that the definable sets of  (definition
<ref>) can be expressed by the
propositional formulas whose predicates are equality and symbols for
predicates in .



Let ϕ(x) = 2^z_1x + r_1, z_1 ∈Ζ, r_1 ∈. 




  * Assume r ∈, z ∈Ζ and B = M(2^r,z) ∈ and B' = M(2^r+z_1,2^z_1z +
r_1).
If B' ∈ then ϕ_(B) ∼ B'.

  * If B ∈ and ϕ_(B), then ϕ_(B) ∼ B' for some B' ∈

  * If D ∈ and ϕ_(D) ⊆ then ϕ_(D) ∈





  * From B, B' ∈ we deduce B =(B ∩) ∪ (B ∩) ∪ (B ∩), and the same for B'.  If ϕ is even we have ϕ_(B ∩) ∼ B' ∩ and ϕ_(B ∩) ∼ B' ∩ and ϕ_(B ∩) ∼ B' ∩. If ϕ is odd we have ϕ_(B ∩) ∼ B' ∩ and ϕ_(B ∩) ∼ B' ∩ and ϕ_(B ∩) ∼ B' ∩. In both cases we conclude that ϕ_(B) ∼ B'.


  * Assume B = M(2^r,z) for some r ∈, z ∈Ζ and ϕ_(a) ∈ for all but finitely many a ∈ B. By definition, the set ϕ_(B) includes elements of  with second coordinate r_w = (2^r+z_1*w + (2^z_1z + r_1)) ∈Ζ, for all but finitely many w ∈Ζ. If we choose two consecutive values of w such that r_w ∈Ζ, we deduce that 2^r+z_1∈Ζ and 2^z_1z + r_1 ∈Ζ, hence that r+z_1 ∈. Thus, M(2^r+z_1,2^z_1z + r_1) is a set of . By the point 1 above we have ϕ_(B) ∼ M(2^r+z_1,2^z_1z + r_1). We conclude that ϕ_(B) ∼ B' for some B' ∈.


  * If D ∈ then by Lemma <ref>, point 3, we have D ∼
M(2^a_1,b_1) ∪…∪ M(2^a_i,b_i) for some a_1, …, a_i ∈ and some b_1, …, b_i ∈Ζ. From ϕ_(D) ⊆ we deduce ϕ_(a) ∈ for all but
finitely many a ∈ M(2^a_1,b_1) ∪…∪ M(2^a_i,b_i). By the
point 2 above we obtain ϕ_(M(2^a_1,b_1)) ∼ B'_1, …,
ϕ_(M(2^a_i,b_i)) ∼ B'_n for some B'_1, …, B'_n ∈.
Thus, ϕ_(D) ∈. 


 and  satisfy the following closure properties.



Assume that R, S ∈ and D ∈.



  * 𝕀_D ∈


  * If D ∈ then R(D) ∈


  * R  S ∈.


  * R^-1∈






  * 𝕀_D is an even (D,D,𝕀)-bijection.


  * 

If R is a (A,B,ϕ)-bijection, then by ϕ_(A ∩ D) = R(D)
⊆ B ⊆ we deduce ϕ_(A ∩ D)
⊆. By Lemma <ref>,
by A ∩ D ∈ and ϕ_(A ∩ D) ⊆ 
we deduce R(D) ∈.


  * 

S is some (A,B,ϕ)-bijection and R is some
(C,D,ψ)-bijection.  If R is an
even bijection, then R maps  in , and
 in , and  in
.  If R is an odd bijection, then R maps
 in , and  in ,
and  in .  The same holds for ψ
and S. Thus, R  S ∈ is even if both are even or both
are odd, and it is odd if one is odd and the other is even, and it is some
(ϕ^-1_(B∩ C), ψ_(B ∩ C), ψϕ)-bijection. Here we use the fact that B, C ∈ imply B
∩ C ∈ by closure of  under intersection, and that
ϕ^-1∈ and ϕ^-1_(B ∩ C) ⊆ A
⊆ imply ϕ^-1_(B∩ C) ∈
by Lemma <ref>, point 2. In the same way we prove that
ψ_(B∩ C) ∈.


  * 

Assume that R is a (D,E,ϕ)-bijection. Then R^-1 is even
or odd according to what is R, and is a (E,D,ϕ^-1)-bijection.




We write L() for the first-order language generated from 
binary predicate symbols for
relations in . Our goal is to prove that every first-order
definable set in  is in . Since the sets definable in
L() include those definable in , it is enough to prove
that any first-order definable set in L() is in . To
this aim, we need a quantifier-elimination result for a language
including L().



§ QUANTIFIER ELIMINATION RESULT FOR PARTIAL BIJECTIONS



In this section we prove a quantifier elimination result for some set of
partial bijections, which is an abstract counterpart of the set
 introduced in section <ref>. The
quantifier elimination result holds when  is closed under
composition and inverse. It is a simple, self-contained result
introducing a model-theoretical tool of some interest.  The only part
of this section which is used in the rest of the paper is the theorem
<ref>, which will be used to characterize
the sets which
are first order definable from the set . We take the definition
of quantifier elimination from <cit.>, section 3.1, section
3.2.


A set  of bijections on U is called 
closed under composition and inverse,
if R,S ∈ implies  R^-1, R ∘ S ∈.



Assume R_1,R_2 are in  that is closed under composition and inverse.



  * ∃ x_2R_1(x_1,x_2)  R_1^-1∘ R_1(x_1,x_1).

  * R_1(x_1,x_2)  R_2(x_2,x_3)  R_1(x_1,x_2)  R_2 ∘ R_1(x_1,x_3).




  
  * ← trivially holds. Since R_1 is a partial bijection,  holds.
  
  *  trivially holds. We will show ←.
    Assume R_1(x_1,x_2)  R_2 ∘ R_1(x_1,x_3).
    Then R_1^-1(x_2,x_1).
    Then R_2 ∘ R_1 ∘ R_1^-1(x_2,x_3).
    By definition of composition,
    R_2 ∘ R_1 ∘ R_1^-1(x_2,x_3)  ∃ x_1x_2'(R_1^-1(x_2,x_1)  R_1(x_1,x_2')  R_2(x_2',x_3)).
    Since R_1 is a partial bijection, x_2=x_2'.
    Hence
    R_2 ∘ R_1 ∘ R_1^-1(x_2,x_3)  R_2(x_2,x_3).
    Hence we have the left-hand side. 


For a set  of partial bijection on U 
we will consider the structure (U,) where
U is the universe and each partial bijection in  is a binary relation.
We will also consider the theory of the structure (U,) where
each element u in U is denoted by the constant u itself
and each partial bijection R in  is denoted by the predicate symbol R itself.


If  is a set of partial bijection on U that is closed under composition and inverse,
the theory of the structure (U,) admits quantifier elimination.



Let  be the structure (U,).



  * First we will show the following claim:

If  is a set of partial bijection on U that is closed under composition and inverse,
the theory of the structure (U,) without = admits quantifier elimination.

Assume a quantifier-free formula A of L() is given.
Let FV(A) = { x_1,…,x_n }.
We assume A is a disjunctive normal form.
We will find a quantifier-free formula B of L() that is equivalent to
∃ x_n A in .
Since ∃ x_n can be distributed over disjuncts,
we can assume A does not contain disjunction.

First we replace R(x_i,x_j) by R^-1(x_j,x_i) in A if i>j.
Then we can assume i ≤ j for every R(x_i,x_j) in A.



  * Case 1. There is some positive R_1(x_i,x_n) in A such that i<n.

We replace every positive or negative R_3(x_j,x_n), R_4(x_n,x_j),
and R_5(x_n,x_n) for j < n except the atom R_1(x_i,x_n) by
R_1^-1∘ R_3(x_j,x_i),
R_4 ∘ R_1(x_i,x_j),
and R_1^-1∘ R_5 ∘ R_1(x_i,x_i) respectively.
Then atoms that contain x_n is only the positive R_1(x_i,x_n).
Let the result be C  R_1(x_i,x_n).
Then ∃ x_n A  C ∃ x_n R_1(x_i,x_n).

Then ∃ x_n R_1(x_i,x_n)  R_1^-1∘ R_1(x_i,x_i).
Hence ∃ x_n A  C  R_1^-1∘ R_1(x_i,x_i).
Take B to be it.


  * Case 2. Positive atoms that contain x_n are only R_1(x_n,x_n),…,R_k(x_n,x_n).

Let A be A_1  R_1(x_n,x_n) … R_k(x_n,x_n)  R'_1(x_n,x_n) … R'_m(x_n,x_n)
A_2
where k,m ≥ 0, A_1 does not contain x_n and
each atom in A_2 is negative and contains both x_n and x_i for some i<n.

Let X be { x ∈ U  |  R_1(x,x), …, R_k(x,x),
 R'_1(x,x), …,  R'_m(x,x)  }.


  * Case 2.1. X is finite.

Let X be {u_1,…,u_m}.
Take B to be _u ∈ X A[x_n:=u].
Then ∃ x_n A  B.


  * Case 2.2. X is infinite.

By moving ∃ x_n inside, 
∃ x_n A  A_1 ∃ x_n(R_1(x_n,x_n) … R_k(x_n,x_n) 
 R'_1(x_n,x_n) … R'_m(x_n,x_n)
 A_2).
Take B to be A_1.
Then ∃ x_n A  B, since we can show
∃ x_n(R_1(x_n,x_n) … R_k(x_n,x_n) 
 R'_1(x_n,x_n) … R'_m(x_n,x_n)
 A_2) 
as follows.

Fix a negative atom R”(x_i,x_n) in A_2 where i<n.
Given x_1,…,x_n-1, we have |{ x_n ∈ U  | R”(x_i,x_n)}| ≤ 1 since
R” is a partial bijection.
Let Y be { x_n ∈ U  |  A_2 }.
Then Y is cofinite.
Since X is infinite, X ∩ Y ∅.
Hence
∃ x_n(R_1(x_n,x_n) … R_k(x_n,x_n) 
 R'_1(x_n,x_n) … R'_m(x_n,x_n)
 A_2) 
is true.



We have shown the claim.


  * Next we will show the theorem by using (1).

Assume a formula A is given.
Let ' be ∪{_U }.
Then ' is also closed under composition and inverse.
Let A' be the formula obtained from A
by replacing t_1=t_2 by _U(t_1,t_2).
Then A' is a formula in the theory of the structure (U,') without =.
By (1),
we have a quantifier-free formula B' equivalent to A' in 
the theory of the structure (U,').
Let B be the formula obtained from B'
by replacing _U(t_1,t_2) by t_1=t_2.
Then B is a quantifier-free formula in the theory of  and B  A.



If  is a set of partial bijection on U that is closed under composition and inverse,
and _{u}∈ for every u ∈ U,
then 
in the theory of the structure (U,),
for any given formula,
there is some quantifier-free constant-free formula that is equivalent to the formula.



Assume a formula A is given.
Choose any variable x.
By the theorem <ref>, 
there is a quantifier-free formula B that is equivalent to A.
In B, we replace R(u_1,u_2) with constants u_1,u_2 by
x=x if R(u_1,u_2) is true,
and replace it by x=x if it is false.

In B, we replace R(u,x) with constants u by
_{u_1}(x,x) if R(u,x) is equivalent to x=u_1,
and replace it by x=x if it is false.

In B, we replace R(x,u) with constants u in the same way as R(u,x).

Let C be the result.
Then A  C and C is a quantifier-free constant-free formula.


[Quantifier and constant elimination]
Our proof of the quantifier elimination results give an effective way
to transform any A ∈ L() into some equivalent quantifier-free
B ∈ L(). We explain how this method works by
two examples. Assume R_1, R_2, R_3 ∈.
We will eliminate quantifiers in ∃ x_4.A 
for a given quantifier-free formula A in the language L(),
by producing  some equivalent quantifier-free formula B ∈ L().



  * Example 1.
A = (R_1(x_1,x_4)  R_2(x_2,x_4)  R_3(x_3,x_4)). 
First we can use R_1(x_1,x_4) to eliminate x_4 in the other atoms,
since R_1 is a partial bijection.
Then ∃ x_4A is equivalent to

    ∃ x_4(R_1(x_1,x_4)  R_1^-1∘ R_2(x_2,x_1)  R_1^-1∘ R_3(x_3,x_1)).

Next we move ∃ x_4 inside and obtain an equivalent formula

    ∃ x_4(R_1(x_1,x_4))  R_1^-1∘ R_2(x_2,x_1)  R_1^-1∘ R_3(x_3,x_1).

Then we can replace ∃ x_4(R_1(x_1,x_4)) by
R_1^-1∘ R_1(x_1,x_1), since R_1 is a partial bijection,
to obtain an equivalent formula

    R_1^-1∘ R_1(x_1,x_1)  R_1^-1∘ R_2(x_2,x_1)  R_1^-1∘ R_3(x_3,x_1),

which we can take B to be.

  * Example 2.
A = (R_1(x_1,x_3)  R_2(x_4,x_4)  R_3(x_3,x_4)). 
First we move ∃ x_4 inside and obtain an equivalent formula

    R_1(x_1,x_3) ∃ x_4(R_2(x_4,x_4)  R_3(x_3,x_4)).

Let X be { x ∈ U  |  R_2(x,x) }.
We have two cases according to whether X is finite or not.


  
  * Case 1. X is finite.

For example, we assume X is { u_1, u_2 }.
By replacing existential quantification by disjunction we obtain an equivalent formula

    R_1(x_1,x_3)  ( R_3(x_3,u_1)  R_3(x_3,u_2)).

Since R_3 is a partial bijection,
R_3(x_3,u) is equivalent to false or x_3=u' for some u' ∈ U.
For example, we assume R_3(x_3,u_1) is equivalent to x_3=u_1'
and
R_3(x_3,u_2) is equivalent to x_3=u_2'.
Since x_3=u_i' is equivalent to _u_i'(x_3,x_3) for i=1,2,
we can take B to an equivalent formula

    R_1(x_1,x_3)  (_u_1'(x_3,x_3) _u_2'(x_3,x_3)).



  * Case 2. X is infinite.

For a given u_3 ∈ U,
|{ x_4 ∈ U  | R_3(u_3,x_4) }| is cofinite,
since R_3 is a partial bijection.
Since X is infinite, ∃ x_4(R_2(x_4,x_4)  R_3(x_3,x_4))
is true.
Hence we can take B to be an equivalent formula

    R_1(x_1,x_3).







§ MAIN THEOREM



In this section we prove that the statement 2-Hydra is a
counterexample to the Brotherston conjecture. Assume  is the
structure for the language Σ_N with universe 
defined in section <ref>. 
Recall that L() denoted the language having
a predicate symbol for each R ∈, where we identify R and
the symbol denoting R. We write L() for the language 
generated from 
Σ_N ∪. We consider the equality predicate = a part
of any first order language.

We write  for the
structure (||, 0_, s_, N_, p_, ).
We write L() for the first-order language generated from
||, 0, s, N, p,.




Let  be that introduced in section <ref>.
Then all
atomic formulas A ∈ L() are equivalent to some
formula B ∈ L() in .


 
Translation is defined to be homomorphic with logical connectives.


  * N(t) is translated into true.

  * x=y is translated into _M(x,y).

  * x = s^n(0) is translated into _{(1,n)}(x,x).

  * x = s^n((i,a)) for (i,a) ∈ M is translated into _{(i,a+n)}(x,x).

  * x=s^n(y) is translated into R(y,x) where
R = (||, || - {0,1,…,n-1}, ϕ) and ϕ(x)=x+n.

  * t_1=t_2 is first translated into 
∃ xy(x=t_1  y=t_2  x=y),
then translated into some formula by using above translation.

  * p(t_1,t_2) is first translated into 
∃ xy(x=t_1  y=t_2  p(x,y)),
then translated into some formula by using above translation.

  * R(t_1,t_2) is first translated into 
∃ xy(x=t_1  y=t_2  R(x,y)) for R ∈.
then translated into some formula by using above translation.



If X={ x ∈ M  | R(x,x) } for some R ∈,
then X ∈.


Let R be (A,B,ϕ) where ϕ(x)=2^ax+b.
If (a,b)=(0,0), then X=A and X ∈.
If (a,b)  (0,0), |X| ≤ 2 since
X is the intersection of the lines 
{ (x,y) ∈ M^2  | y=ϕ(x), x ∈ A }
and the line { (x,y) ∈ M^2  | x=y }.
Hence X ∈.




Let H be the formula defined in  Definition <ref>.
Then H has 
a proof in (Σ_, Φ_), and 
no proof in (Σ_, Φ_) + (0,)-axioms. 



The proof of H in  is shown in Theorem <ref>. The non-provability of H in (Σ_, Φ_) + (0,)-axioms is shown as follows. Let  be the structure defined in section <ref>:  falsifies H by Lemma <ref>.

We defined _ as the Henkin family of definable sets in
 (definition <ref>).  What is
left to be proved is: (, _) is a Henkin model of
(Σ_, Φ_). By definition of Henkin
model we have to prove that any prefixed point 
of the monotone operator ϕ_Φ_N 
with the restriction in _ 
includes the
interpretation of N. As we already pointed out, since the
interpretation of N is  itself, this is to say that any
set in _1 of _ which is closed under 0 and  is
equal to .

Let , be the set of relations and domains defined in
Def. <ref>, <ref>, and let =
(, ) be the partial bijection structure defined
by . By induction on the formula we prove that all formulas A
∈ L() are equivalent in  to some formula 
B ∈ L(): in the case A is an atomic formula we use Lemma
<ref>, in the cases A =  A_1, A_1 ∨ A_2,
∃ x. A_1 the induction hypothesis on A_1, A_2.

 includes all singletons and it is closed under complement and
finite union by Lemma <ref>.  is closed under
composition and inverse by Lemma <ref>,
points 3,4, By Theorem <ref>, each A
∈ L() having exactly one free variable x is equivalent in
 to some quantifier-free B ∈ L(). By replacing by x
each variable y ≠ x in B we obtain a formula B' equivalent
to A, which is a boolean combination of atoms of the form R(x, x)
for some R ∈, or the form x=x.  Assume an atom of the form
R(x,x).  Then D = {x ∈ ||^2 | R(x, x)} is in 
by Lemma <ref>.  Assume an atom of the form x=x. Then {x
∈ U | x=x} is U ∈. Thus, each atom R(x, x) in B'
is equivalent to x ∈ D for some D ∈. By the closure
properties for  we deduce that B' defines some set D' in
.  By Lemma <ref>, point 4, D' has
a dyadic measure, and by Lemma <ref> 
D' satisfies the induction schema.
Hence
(,_) is a Henkin
model of (Σ_, Φ_), as we wished
to show.




 §.§ Non-Conservativity of the Inductive Definition System 



This subsection shows a side result: non-conservativity of 
with respect to additional inductive predicates, by giving a counterexample.

In the standard model, the truth of formula does not change
when we extend the model with inductive predicates that do not appear in the formula.
On the other hand, this is not the case for provability in
the inductive definition system .
Namely, a system may change the provability of a formula
even when we add inductive predicates that do not appear in the formula.
Namely, for a given system,
the system with additional inductive predicates may not be
conservative over the original system.


There are Σ_1,Φ_1,Σ_2,Φ_2 such that
(Σ_2,Φ_2) is an extension of (Σ_1,Φ_1) and
(Σ_2,Φ_2) is not conservative over (Σ_1,Φ_1).


Take Σ_1 to be 0,s,N,p and Φ_1 to be Φ_N and
Σ_2 to be Σ_1 ∪{≤} and Φ_2 to be Φ_1 with
the production rules for ≤.
Then 
the sequent ⊢ H is in the language of
(Σ_1,Φ_1) but it is not provable in (Σ_1,Φ_1)
by Theorems <ref>,
while it is provable in (Σ_2,Φ_2)
by Theorem <ref>.




§ CONCLUSION


We have proved in Thm. <ref> that , the formal system
of cyclic proofs <cit.> proves strictly more than
, Martin-Löf's formal system of inductive definitions with
classical logic. This settles an open question given in <cit.>. 
In Theorem <ref>, by the same counterexample
we also shows that if we add more inductive predicates to
 we may obtain a non-conservative extension of .



 §.§ Acknowledgments

This is partially supported by Core-to-Core Program (A. Advanced
Research Networks) of the Japan Society for the Promotion of Science.

10

Berardi-Makoto-FOSSACS2017
Stefano Berardi, Makoto Tatsuta, The Classic Martin-Löf's System of Inductive Definitions is not Equivalent to Cyclic Proofs, FOSSACS 2017, 301–317.
 
Brotherston05
James Brotherston,
Cyclic Proofs for First-Order Logic with Inductive Definitions,
In: Proceedings of TABLEAUX 2005, 2005. 

Brotherston-phd
James Brotherston,
Sequent calculus proof systems
for inductive definitions,
phd. thesis, Laboratory for Foundations of Computer Science
School of Informatics
University of Edinburgh
2006.

Brotherston08
James Brotherston, Richard Bornat and Cristiano Calcagno,
Cyclic Proofs of Program Termination in Separation Logic,
In: Proceedings of POPL 2008, 2008. 

Brotherston11a
James Brotherston, Dino Distefano and Rasmus L. Petersen,
Automated Cyclic Entailment Proofs in Separation Logic,
In: Proceedings of CADE-23, 2011. 

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

Brotherston12
James Brotherston, Nikos Gorogiannis and Rasmus L. Petersen,
A Generic Cyclic Theorem Prover,
In: Proceedings of APLAS 2012, 2012.

Enderton00
H. B. Enderton,
A Mathematical Introduction to Logic, Second Edition,
Academic Press, 2000.

Kirby-1982
Laurence Kirby and Jeff Paris, Accessible Independence Results for Peano Arithmetic, Bulletin of London Mathematical Society, 1982; 14: 285-293.

Martin-Lof-1971
P. Martin-Löf. Hauptsatz for the intuitionistic theory of iterated inductive definitions. In Proceedings of the Second Scandinavian Logic Symposium, pp. 179–216. North-Holland,
1971.

Simpson-2017
Alex Simpson. Cyclic Arithmetic is Equivalent to Peano Arithmetic. Proceedings of Fossacs 2017.

Stratulat-2016
Sorin Stratulat, Structural vs. cyclic induction: a report on some experiments with Coq, 2016, SYNASC 2016: Proceedings of the 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, p. 27-34, IEEE Computer Society


