Recursive Definitions

Summary. The text contains some schemes which allow elimination of defintions by recursion. MML Identifier: RECDEF 1. The papers [5], [1], [3], [2], and [4] provide the notation and terminology for this paper. We follow a convention: n, m, k will denote natural numbers and x, y, z, y1, y2 will be arbitrary. The arguments of the notions defined below are the following: D which is a non-empty set; p which is a function from into D; n which is an element of . Then p(n) is an element of D. The arguments of the notions defined below are the following: p which is a function from into ; n which is an element of . Then p(n) is a natural number. In the article we present several logical schemes. The scheme RecEx concerns a constant A and a ternary predicate P and states that: there exists f being a function such that domf = and f(0) = A and for every element n of holds P[n,f(n),f(n + 1)] provided the parameters satisfy the following conditions: • for every natural number n for arbitrary x there exists y being any such that P[n,x,y], • for every natural number n for arbitrary x, y1, y2 such that P[n,x,y1] and P[n,x,y2] holds y1 = y2. The scheme RecExD deals with a constant A that is a non-empty set, a constant B that is an element of A and a ternary predicate P and states that: there exists f being a function from into A such that f(0) = B and for every element n of holds P[n,f(n),f(n + 1)] provided the parameters satisfy the following conditions: • for every natural number n for every element x of A there exists y being an element of A such that P[n,x,y], • for every natural number n for all elements x, y1, y2 of A such that P[n,x,y1] and P[n,x,y2] holds y1 = y2