key: cord-0060957-7rrkkl6q
authors: Berghammer, Rudolf
title: A Relation-Algebraic Treatment of the Dedekind Recursion Theorem
date: 2020-04-01
journal: Relational and Algebraic Methods in Computer Science
DOI: 10.1007/978-3-030-43520-2_2
sha: df0193f8351d498c5df6d9ddc2d978b8ce13252b
doc_id: 60957
cord_uid: 7rrkkl6q

The recursion theorem of Richard Dedekind is fundamental for the recursive definition of mappings on natural numbers since it guarantees that the mapping in mind exists and is uniquely determined. Usual set-theoretic proofs are partly intricate and become lengthy when carried out in full detail. We present a simple new proof that is based on a relation-algebraic specification of the notions in question and combines relation-algebraic laws and equational reasoning with Scott induction. It is very formal and most parts of it consist of relation-algebraic calculations. This opens up the possibility for mechanised verification. As an application we prove a relation-algebraic version of the Dedekind isomorphism theorem. Finally, we consider two variants of the recursion theorem to deal with situations which frequently appear in practice but where the original recursion theorem is not applicable.

The so-called recursion theorem of Richard Dedekind, first formulated and proved in [6] , pertains to the method of recursively defining mappings f : N → A on the set of natural numbers N by first defining the value of f (0) (in [6] f (1), since there the natural numbers start with 1) and then defining the value of f (n + 1) (in [6] f (n ), with n as the successor of n) subject to the value of f (n), for an arbitrary natural number n ∈ N. It states that there exists precisely one such mapping and this guarantees the correctness of the method. Besides the Peano axioms, Dedekind's original proof (see [6] , Satz 126) decisively depends on the linear ordering of the natural numbers which, in contrast with modern approaches, is specified before addition is introduced. About fifty years later proofs have been published which do not use the order but are based only on the zero/one element and the successor mapping, that is, on the vocabulary of the Peano axioms. Two of them can be found in [9, 11] . The reader interested in the history of the Dedekind recursion theorem is referred to [7, 8] , for example.

Nowadays the Dedekind recursion theorem is frequently presented using Peano structures. These are algebraic structures (N, z, s) with a non-empty carrier set N , an element z ∈ N (the zero element) and a mapping s : N → N (the successor mapping) such that the following three axioms hold:

Then the recursion theorem states that, given a Peano structure (N, z, s), a nonempty set A, an element c ∈ A and a mapping F : A → A, there exists precisely one mapping f : N → A with the following two properties:

Modern proofs of the recursion theorem define the mapping f of (2) as a relation, viz. as the intersection of all relations R with source N and target A such that z R c and for all x ∈ N and y ∈ A from x R y it follows that s(x) R F (y). For example, in [3] , pages 346-348, the partly intricate proof that this intersection in fact is a univalent and total relation (that is, a mapping) and satisfies the two formulae of (2) is carried out in great detail.

Specifying the notions in question in the language of relation algebra and combining relation-algebraic calculations with Scott induction, in Sect. 3 of this paper we present a new proof of the Dedekind recursion theorem that is simpler than the purely set-theoretic proof of [3] or similar proofs. A further advantage of the new proof is that it is very formal and most parts of it consist of equational reasoning. This opens up the possibility for its mechanised verification by means of a theorem-proving tool. As an application of our relation-algebraic version of the recursion theorem we present in Sect. 4 a relation-algebraic version of the Dedekind isomorphism theorem, i.e., prove that all (relational) Peano structures are isomorphic. Finally, in Sect. 5 we consider two cases of recursive definitions of mappings which frequently appear in practice but where the original Dedekind recursion theorem is not applicable since either the mapping f to be defined is not unary or the result of f (s(x)) depends not only on the value of f (x) but also on x. For each case we give an example and prove a corresponding variant of the relation-algebraic recursion theorem.

We assume the reader to be familiar with the basic concepts of partially ordered sets and complete lattices, including monotone mappings on them, basic fixpoint theory (fixpoint calculus) and the construction of direct products. Otherwise we refer to standard textbooks on ordered sets and lattices, e.g., [4, 5] , and to [13] .

Given a partially ordered set (A, ≤) that is a complete lattice, we denote the least element of A by the symbol ⊥, the least upper bound of the subset B of A by B and the greatest lower bound of B by B. Alfred Tarski's well-known fixpoint theorem (see [16] ) states that each monotone mapping f : A → A has a least fixpoint, denoted as μ(f ), and μ(f ) = {x ∈ A | f (x) ≤ x} holds. For proving properties of μ(f ) we will apply the principle of Scott induction, sometimes also called computational induction or fixpoint induction. Usually the principle is formulated for complete partial orders (CPOs), that is, for partially ordered sets with a least element and the property that each chain possesses a least upper bound. See [10] , for example. Scott induction also works in the case of complete lattices, since complete lattices are CPOs.

Assume (A, ≤) to be a complete lattice. Then a predicate P on its carrier set A is called admissible (for Scott induction) if for every chain C in (A, ≤) the following implication is true: if for all x ∈ C it holds P (x), then P ( C) holds, too. Now, Scott induction states that for each monotone mapping f : A → A and each admissible predicate P on A from the two conditions

it follows that P (μ(f )). The left condition of (3) is called the induction base and the right one the induction step with induction hypothesis P (x). Besides the above version we will also apply a version which in [10] is called simultaneous.

We consider the case of two complete lattices (A, ≤ 1 ) and (B, ≤ 2 ) with least elements ⊥ 1 ∈ A and ⊥ 2 ∈ B and two monotone mappings f 1 : A → A and f 2 : B → B only. Then if P is an admissible predicate on the direct product A × B, which is ordered by the product order (that is, by (x 1 , x 2 ) ≤ (y 1 , y 2 ) iff x 1 ≤ 1 y 1 and x 2 ≤ 2 y 2 , for all x 1 , y 1 ∈ A and x 2 , y 2 ∈ B), then from the two conditions

it follows that P (μ(f 1 ), μ(f 2 )). This principle is obtained from the original one by taking in (3) the least element (⊥ 1 , ⊥ 2 ) of the product lattice (A × B, ≤) as ⊥ and the product of the two mappings f 1 : A → A and f 2 : B → B, defined by

as mapping f . Namely, from the monotonicity of f 1 with respect to ≤ 1 and of f 2 with respect to ≤ 2 and the definition of the product order ≤ it follows that f 1 ⊗ f 2 is monotone with respect to ≤ and μ(f 1 ⊗ f 2 ) = (μ(f 1 ), μ(f 2 )). Given complete lattices (A, ≤ 1 ) and (B, ≤ 2 ), a predicate P on the carrier set A × B of the product lattice (A × B, ≤) is admissible (for the simultaneous Scott induction described by (4)) if there exist -distributive mappings α :

for all x ∈ A and y ∈ B, or P (x, y) iff α(x) = β(y), for all x ∈ A and y ∈ B. See e.g., [10] for a proof of this property.

We assume the reader also to be familiar with the basic concepts of (axiomatic) relation algebra as introduced in [15] by Alfred Tarski. Otherwise we refer again to standard textbooks, e.g., to [12, 14] .

As in [14] we work with typed relations. For given sets (or objects in case of axiomatic relation algebra) A and B we denote the set of all relations with source A and target B by [A ↔ B] and write R :

As operations and predicates on relations we use transposition R T , complementation R , union R ∪ S, intersection R ∩ S, composition R ; S, inclusion R ⊆ S and equality R = S, and as special relations we use the empty relation O, the universal relation L and the identity relation I. As usual, in the latter cases we overload the symbols, i.e., avoid the binding of types to them, since all types can be derived from the context by means of the typing rules of the operations. All basic relation-algebraic laws we will apply in the remainder of the paper are well known for set-theoretic relations; their proofs from the axioms of an (axiomatic) relation algebra can be found in [14] , for example.

Many important properties of relations can be specified in a quantifierfree manner using (conjunctions of) inclusions and equations between relationalgebraic expressions only. In this paper we will use that a relation R : A ↔ B is univalent iff R T ; R ⊆ I, total iff R ; L = L or, equivalently, iff I ⊆ R ; R T , injective iff R ; R T ⊆ I and surjective iff R T ; L = L or, equivalently, iff I ⊆ R T ; R. For all R and S the following implication is shown in [14] as Proposition 4.2.2.iv:

Other results of [14] we will apply are Proposition 4.2.2.iii, stating that

for all Q, R and S, and Proposition 2.4.2.i, stating that

for all Q, R and S. We also need relational vectors, which are relations v : A ↔ B with v = v ; L, and relational points, which are injective and surjective relational vectors. In case of set-theoretic relations a little reflection shows that v : A ↔ B is a relational vector iff there exists a subset V of the set A such that v = V ×B, and it is a relational point iff additionally V is a singleton set. Hence, a set-theoretic relational vector models a subset of its source and a set-theoretic relational point models an element of its source. Therefore, the targets are irrelevant and in most applications, also of (axiomatic) relation algebra, relational vectors and points are from a set [A ↔ 1 1], where 1 1 is a singleton set (a specific object, respectively). In this case the demand v = v ; L can be dropped, since it holds because the identity relation and the universal relation from [1 1 ↔ 1 1] coincide.

To treat mappings with more than one argument relation-algebraically, we will use constructions related to direct products, viz. projection relations, products and pairings. Their formal introduction is postponed to Sect. 5.

In this section we formulate the recursion theorem of Dedekind in the language of relation algebra and present a proof that combines relation-algebraic calculations and Scott induction. We start with the following definition of a relational Peano structure. In a similar form its axioms can be found already in [2] . Since the Dedekind recursion theorem is a theorem on sets, in Definition 3.1 and all results we will prove in the remainder of the paper we consider relations as set-theoretic ones. But we will use only the operations of (axiomatic) relation algebra and its laws. As a consequence, our results remain true in this more general setting.

Compared with the notion of a Peano structure formulated in the introduction we see that the relational point z : N ↔ 1 1 models the zero element and the univalent, total and injective relation S : N ↔ N equals the injective successor mapping. The equation S ; z = O is the relation-algebraic version of the second formula of (1) and that for all relational vectors v :

follows v = L is the relation-algebraic version of the third formula of (1). To be able to prove totality of relations by means of Scott induction, in the next lemma (following [2] ) we specify the last axiom of a relational Peano structure as a least fixpoint equation. Notice, that in the remainder of the paper monotonicity of a mapping on relations always supposes inclusion as order.

Lemma 3.1. Assume z : N ↔ 1 1 to be a relational vector, S : N ↔ N to be a relation and the mapping g to be defined as follows:

Proof. The monotonicity of the mapping g follows from the monotonicity of union and composition. To show the second claim, we calculate as follows:

Having specified Peano structures in the language of relation algebra, we now consider the two formulae of the recursive definition of the mapping f : N → A via (2). If we model the element z ∈ N by the relational point z : N ↔ 1 1 of a relational Peano structure (N, z, S), use the univalent, total and injective relation S : N ↔ N instead of the injective successor mapping s : N → N , model the element c ∈ A by the relational point c : A ↔ 1 1, take the mapping F : A → A as univalent and total relation from [A ↔ A] and take the mapping f : N → A as univalent and total relation from [N ↔ A], then the two formulae of (2) are relation-algebraically specified as follows:

As next result we show how the two formulae of (9) can be specified by a single fixpoint equation. 

Then h is monotone and μ(h) : N ↔ A is total. Furthermore, for all univalent and total relations f : N ↔ A the two formulae of (9) 

Proof. The monotonicity of the mapping h follows again from the monotonicity of union and composition. With regard to the totality of the relation μ(h) we prove μ(g) ⊆ μ(h) ; L, with the mapping g defined by (8) . We apply Scott induction (of the form (4)) with the predicate P on the direct product 1 1] , respectively, the predicate P is admissible due to the criterion mentioned in Sect. 2.

A proof of the induction base P (O, O) is trivial. For a proof of the induction step, assume an arbitrary relational vector v : N ↔ 1 1 and an arbitrary relation X : N ↔ A such that P (v, X) holds. Then we get P (g(v), h(X)) by the following calculation: (10) Therefore, we have P (μ(g), μ(h)), i.e., μ(g) ⊆ μ(h) ; L. Now, L = μ(h) ; L follows from the last axiom of a relational Peano structure and Lemma 3.1. For a proof of the remaining claim, assume an arbitrary univalent and total relation f : N ↔ A to be given. To show implication "=⇒", suppose the two formulae of (9) to be true. We start with the following calculation: (9) In combination with Tarski's fixpoint theorem from (5) . With regard to implication "⇐=", assume f = h(f ). The following proof of the first formula of (9) uses definition (10) of the mapping h and f = h(f ):

The second formula of (9) is shown by the following calculation:

Notice, that in this proof only the univalence of the relation f is used. But from μ(h) ⊆ f and the totality of μ(h) the totality of f follows. For F only totality is applied. Now, we are able to prove the following relation-algebraic version of the recursion theorem of Dedekind. Here univalence of F is used, too. is also univalent, we use Scott induction (of the form (3)) with the predicate P on the set [N ↔ A] defined by P (X) iff X T ; X ⊆ I, for all relations X : N ↔ A.

To verify that P is admissible, assume the subset C of [N ↔ A] to be a chain of univalent relations. Then the following calculation shows that also the union (i.e., least upper bound) C is a univalent relation:

The last step uses {R T ; S | S ∈ C} ⊆ I, for all relations R ∈ C. This inclusion holds as, given any R ∈ C, it holds that R T ; S ⊆ I, for all relations S ∈ C. The latter, in turn, follows from the chain property of C and since all relations of C are univalent. Namely, given any S ∈ C, in case R ⊆ S we get R T ; S ⊆ S T ; S ⊆ I and in case S ⊆ R we get R T ; S ⊆ R T ; R ⊆ I. A proof of the induction base P (O) is obvious. To show the induction step, assume an arbitrary relation X : N ↔ A with P (X). Then P (h(X)) holds because of the following calculation:

Concerning Peano structure is applied. Also F T ; X T ; S ; z ; c T = O follows from this axiom. Finally, for F T ; X T ; S ; S T ; X ; F ⊆ F T ; X T ; X ; F ⊆ F T ; F ⊆ I we use that S is injective, X is univalent (due to the induction hypothesis P (X)) and F is univalent.

Because of μ(h) = h(μ(h)) and since μ(h) is univalent and total, from implication "⇐=" of Lemma 3.2 we get that the two formulae of (9) hold for the univalent and total relation μ(h), that is, we have z ; c T ⊆ μ(h) and S ; μ(h) = μ(h) ; F .

To show that μ(h) is the only univalent and total relation from [N ↔ A] that satisfies the two formulae of (9), let an arbitrary univalent and total relation f : N ↔ A be given such that z ; c T ⊆ f and S ; f = f ; F . Then implication "=⇒" of Lemma 3.2 shows f = h(f ), from which μ(h) ⊆ f follows. This inclusion, the univalence of f , the totality of μ(h) and implication (5) 

The proofs of Lemma 3.2 and Theorem 3.1 contain the decisive ideas which also will be used in Sect. 5 for proving the variants of Theorem 3.1 we have mentioned in the introduction.

Besides the recursion theorem a second important result of [6] is the nowadays called Dedekind isomorphism theorem (see [6] , Satz 132). In modern terminology it says that for each pair of Peano structures (N, z, s) and (N 1 , z 1 , s 1 ) there exists a bijective mapping Φ : N → N 1 with the following two properties:

When translated into the language of relation algebra with relational Peano structures (N, z, S) and (N 1 , z 1 , S 1 ), the bijective mapping Φ : N → N 1 becomes a univalent, total, injective and surjective relation Φ : N ↔ N 1 for which the following relation-algebraic versions of the two formulae of (11) hold:

To prove the existence of such a relation Φ, we consider the monotone mapping h of (10), where the set A is instantiated by N 1 , the relational point c is instantiated by z 1 : N 1 ↔ 1 1 and the relation F is instantiated by S 1 : N 1 ↔ N 1 . So, the mapping we consider is given as follows:

Furthermore, we define Φ as least fixpoint of h 1 , i.e. by Φ := μ(h 1 ) : N ↔ N 1 . Then from Theorem 3.1 we get that Φ is the only univalent and total relation from [N ↔ N 1 ] that satisfies the two formulae of (12). So, it remains to verify Φ as injective and surjective. To this end, we consider the following monotone mapping h 2 (that is again a specific instance of the mapping h of (10)):

It is easy to verify that the mapping t :

Hence, the μ-fusion theorem of the fixpoint calculus (see [13] ) yields

This equation and the univalence and totality of μ(h 2 ) (a consequence of Theorem 3.1) yield the injectivity and surjectivity of Φ. Altogether, we have shown the following relation-algebraic version of the Dedekind isomorphism theorem. 

When defining a mapping on natural numbers (or on a Peano structure) recursively, it frequently possesses, besides the argument that controls the recursion, additional arguments. An example is the following recursive definition of the addition-mapping add : N × N → N on a Peano structure (N, z, s) , where the first argument of add controls the recursion:

Since the original Dedekind recursion theorem only treats the recursive definition of unary mappings, it cannot immediately be applied to show that there exists precisely one mapping add : N × N → N for which the two formulae of (15) hold. Therefore, in the following we present a corresponding variant -in terms of sets as well as in terms of relation algebra. To simplify the presentation, we consider mappings of the kind f : N ×B → A only. Taking B as a direct product n i=1 B i , this also covers the case of mappings with more than two arguments. The set-theoretic variant of the Dedekind recursion theorem we have in mind is as follows: Let (N, z, s) be a Peano structure, A and B be non-empty sets and mappings d : B → A and G : A → A be given. Then there exists precisely one mapping f : N × B → A that satisfies the following two formulae:

If this statement is translated into the language of relation algebra, with a relational Peano structure (N, z, S) and the mappings d and G as univalent and total relations, then we obtain the following variant of Theorem 3.1. Up to isomorphism, the latter are specified relationalgebraically by the following four axioms (see also [2, 14] ): S ; π T ) T ; π ; S ; π T = π ; S T ; π T ; π ; S ; π T ⊆ π ; π T and its definition and the univalence of ρ imply

such that the third formula of (18) yields (S ⊗ I)

Similar calculations show that S ⊗ I is total and injective. After these preparations we are able to prove Theorem 5.1 with relationalgebraic means. The idea is the same as in case of Theorem 3.1. We define an appropriate monotone mapping on the set [N × B ↔ A] and verify that its least fixpoint satisfies the desired properties. Concretely, we consider the least fixpoint μ(h 3 ) : N × B ↔ A of the following monotone mapping:

The proof that μ(h 3 ) is the only univalent and total relation from [N × B ↔ A] that satisfies the two formulae of (17) is given by the following four lemmas.

Proof. Besides the mapping h 3 of (19) we additionally consider the mapping g of (8) and show π ; μ(g) ⊆ μ(h 3 ) ; L using Scott induction (of the form (4)). Then the totality of the projection relation π : N × B ↔ N and the last axiom of a Peano structure in combination with Lemma 3.1 yield L = π ; L = π ; μ(g) ⊆ μ(h 3 ) ; L.

For the Scott induction we use the admissible predicate P on the direct prod- P (v, X) . Then the following calculation shows P (g(v), h 3 (X)): 

and in combination with the above calculation we get P (h 3 (X)).

Proof. Using the definition of the mapping h 3 by (19) and that μ(h 3 ) is a fixpoint of h 3 we obtain

such that μ(h 3 ) satisfies the first formula of (17). The calculation

shows that μ(h 3 ) satisfies the second formula of (17), too. Proof. We start with the calculation 

Such a situation also requires a generalisation of the original Dedekind recursion theorem. The mapping F has to be binary and of type F : A × N → A and the recursive definition (2) of f : N → A changes to the following one:

When translated into the language of relation algebra, the statement that there exists precisely one mapping f : N → A that satisfies the two formulae of (21), leads to the following second variant of Theorem 3.1. 

is the only univalent and total relation from [N ↔ A] that satisfies the two formulae of (22). As in case of Theorem 5.1 this is obtained by four lemmas. To verify the induction step, let an arbitrary relational vector v : N ↔ 1 1 and an arbitrary relation X : N ↔ A be given such that P (v, X) holds. Then we have P (g(v), h 4 (X)) due to the following calculation:

last formula of (18) = z ∪ S T ; (X ; π T ∩ ρ T ) ; π ; L π univalent and (6) Proof. We use Scott induction (of the form (3)) with the admissible predicate P on the set [N ↔ A] defined by P (X) iff X T ; X ⊆ I, for all relations X : N ↔ A. The induction base P (O) holds trivially. To show the induction step, let an arbitrary relation X : N ↔ A with P (X) be given. For P (h 4 (X)) we then start with the following calculation that uses the definition of h 4 via (23): Proof. First, we calculate as follows: 

In this paper we have presented a simple new proof of the Dedekind recursion theorem that is based on a relation-algebraic specification of the notions in question and combines relation-algebraic laws and equational reasoning with Scott induction. As a simple application and using the same means, we also have shown the Dedekind isomorphism theorem. Finally, we have treated two cases where the original Dedekind recursion theorem is not applicable and have presented two variants of the relation-algebraic version of the recursion theorem. Their proofs are variations of that of the latter theorem. It is interesting to look at how Dedekind in [6] treats mappings with more than one argument. From his explanations to the definition of addition and multiplication (see [6] , Erklärung 135 and Erklärung 147) it becomes clear that he implicitly uses currying and uncurrying. For example, in case of addition he does not define a binary operation. Instead of that he fixes a natural number m and then uses Satz 126 to define recursively a unary mapping that yields for each natural number n the sum m + n. In Erklärung 147 he explicitly speaks of an infinite set of new mappings on N found in such a way. Also in the proof of Satz 4 of [9] , where again addition is recursively defined, implicitly currying and uncurrying are used. These approaches can be generalised as given below.

Consider the recursive definition

of a mapping g : N → A B , where (N, z, s) is a Peano structure and the mappings d : B → A and G : A → A are given. Since g is unary, the original Dedekind recursion theorem shows that (24) has a unique solution. We have to instantiate in (2) the set A by the set of mappings A B , the element c by the mapping d, the mapping F by the higher-order mapping F : A B → A B with F (h) = G • h, for all h ∈ A B , and the mapping f by the mapping g. From the unique solution g of (24) we then obtain the unique solution f of (16) via uncurrying, i.e., by defining f : N × B → A as f (x, y) = g(x)(y), for all x ∈ N and y ∈ B, or, shorter, by f := curry −1 (g), where curry −1 is the inverse of the well-known bijective currying-mapping curry. The definition of f and curry −1 and the formulae of (24) allow to show that f satisfies the two formulae of (16) . That it is the only mapping with this property can be shown by means of the definition of f and curry, the formulae of (24) and curry −1 (curry(h)) = h, for all h : N × B → A. All proofs of Sect. 3 to Sect. 5 are very formal and its decisive parts consist of equational reasoning using laws of relation algebra. These are ideal prerequisites for mechanised theorem proving. Concerning mathematical theorems, in the last years especially the proof assistant tools Coq and Isabelle/HOL have been used in this respect. A prominent example is the formal verification of Atle Selberg's elementary proof of the Prime Number Theorem in Isabelle/HOL; see [1] . For the future we also plan a mechanised verification of the proofs of this paper using Coq or Isabelle/HOL.

A formally verified proof of the prime number theorem

Relational algebraic semantics of deterministic and nondeterministic programs

Mathematik für die Informatik

Lattice Theory

Introduction to Lattices and Order

Was sind und was sollen die Zahlen?

Grundlagen der Analysis

The Foundations of Program Verification

Die Definition durch vollständige Induktion

Relation Algebras

Mathematics Program Construction Group: Fixed-point calculus

On the calculus of relations

A lattice-theoretical fixpoint theorem and its applications

Acknowledgement. I thank the referees for carefully reading the paper and for their very valuable suggestions.